A Brief History of Preconditions and Postconditions

Preconditions and postconditions were a relatively recent addition to what Alistair Cockburn, in his article "Use Cases, Ten Years Later," calls the fully dressed use case. They weren't a part of Jacobson's original use cases, or OMT's scenarios. But though a newcomer to use cases, the history of pre- and postconditions goes back to at least the late 1960s with the work of researchers like Floyd, Hoare, and Dijkstra.^[6]

^[6] A paper by Cliff Jones (2003) even traces roots going back to work by pioneers such as Von Neuman and Turing in the late 1940s.

Preconditions and postconditions played a key role in reasoning about programs (Does this program meet its specification?) and later with formal specification languages like VDM (Vienna Development Method) and Z (pronounced "Zed") as a way to specify the behavior of Abstract Data Types. Much of what we today ascribe to being "object-oriented" is rooted in the concept of Abstract Data Types (ADT). This is particularly true of the matter of specifying the expected behavior of an object, which is an issue of great interest to testing. In 1971, David Parnas introduced "Information Hiding," which wrapped each "design decision" in a module with a defined interface eliminating the need for details of how the module was programmed. But if you are going to hide the details of the implementation of your new widget from your fellow programmers, you need some way of communicating to them what the widget does. By the mid-to-late 1970s, two approaches to tackling the problem were underway: the algebraic specification approach and the model-based specification approach. VDM and Z were outgrowths of the work on the latter.^[7] These formal specification languages and techniques in turn influenced the object-oriented community e.g., Bertrand Meyer's Eiffel (1998) with its Design by Contract, pre-UML "unified" object-oriented methodologies such as Fusion (Coleman et al. 1994), and more recently UML's Object Constraint Language (OCL) (Warmer and Kleppe 1994).

^[7] For an overview of algebraic and model-based specification, see Sommerville (2000).

Fast forwarding to today, though preconditions and postconditions are now a part of the fully dressed use case, a key facet in their history, one central to their use in reasoning about programs and specifications, has been overlooked a tad. Preconditions can be calculated from postconditions. In fact, that was pretty much the point originally. You can calculate preconditions from postconditions as opposed to intuitively making them up. And in the early days, there was even discussion as to whether it was better to generate the precondition from the postcondition, or vice versa; the former eventually won out and has been the norm since.

This technique is usually described in terms of Hoare triples or predicate transformer for calculating the weakest precondition (i.e., a technique that transforms one predicate, the postcondition, into another, the precondition). The version of the technique we'll see in this book is basically that used by Z, and in that literature it is often just called "calculating the precondition."

The intent here is not to say that calculating the precondition is the only, or even the right way you get preconditions for use cases; even in writing specifications in formal languages like Z, one usually comes up with preconditions in an intuitive sort of way. But that connection between precondition and postcondition is always there to leverage (e.g., as a way to demonstrate the validity of an intuitively derived precondition or to tell if there are additional preconditions that have been overlooked). And it turns out to be a handy tool for failure analysis of and test design from use cases.