Contracts and Assertions 
A complete PDF version of the text book is now available. The PDF version is an almost complete subset of the HTML version (where only a few, long program listings have been removed). See here. 
This is the first chapter in the lecture about contracts and assertions. We all want to write correct programs. But what is correctness? Program correctness is always relative to something else. In this lecture we will discuss program correctness relative to a program specification. In Chapter 50, (the next chapter) we will take a closer look at a particular approach to program specification, on which the rest of this lecture will be based.

49.1. Software Qualities
Contents Up Previous Next Slide Annotated slide Aggregated slides Subject index Program index Exercise index
Program correctness is one of several program qualities. A software quality is a positive property of program. There are many different software qualities that may be considered and promoted. In Table 49.1 we list a number of important program qualities.
Quality  Description  Contrast 
Correct  Satisfies expectations, intentions, or requirements  Erroneous 
Robust  Can resist unexpected events  Fragile 
Reusable  Can be used in several contexts  Application specific 
Simple  Avoids complicated solutions  Complex 
Testable  Constructed to ease revelation of errors   
Understandable  Mental manageability  Cryptic 
Table 49.1 Different program qualities listed by name, description, and (for selected qualities) a contrasting, opposite quality 
Of all software qualities, correctness play a particular important role. Program correctness is in a league of its own. Who would care about robustness, reusability, and simplicity of an incorrect program?
49.2. Correctness
Contents Up Previous Next Slide Annotated slide Aggregated slides Subject index Program index Exercise index
Software correctness is only rarely an absolute concept. Correctness should be seen relative to something else. We will distinguish between program correctness relative to

At the time the program is written, it may be tempting to rely on the comprehension and specification in the mind of the programmer. It is not difficult to understand, however, that such a specification is volatile. The specification may slide away from the original understanding, or it may totally fade away. In a software house it may also easily be the case that the programmer is replaced. Of these reasons it is attractive to base correctness on written and formal specifications.
In the following section we will discuss written and formal specifications that are based on mathematical grounds.
49.3. Specifications
Contents Up Previous Next Slide Annotated slide Aggregated slides Subject index Program index Exercise index
We will introduce the following straightforward definition of a specification:

Notice that specifications answer what questions, not how questions.
In the area of formal mathematicallyoriented specifications, the following two variants are wellknown:

We will first study an algebraic specification of a stack, see Program 49.1. We have already encountered this specification earlier in the material, namely in the context of our discussion of abstract data types in Section 1.5. From line 411 we declare the syntax of the operations that work on stacks. The operations are categorized as constructors, destructors, and selectors. As the name suggests, constructors are operations that constructs a stack. Both push and pop are functions that return a stack. This is different from the imperative stack procedures we experienced in Program 30.1, which mutate the stack without returning any value.
An arbitrary stack can be constructed in terms of one or more constructors. Destructors are operations that work on stacks. (The term "destructor" may be slightly misleading). Any stack can be constructed without use of destructors. As an example, the expression pop(push(5, pop (push (6, push (7, new ()))))) is equivalent with push(7, new ()). The selectors extract information about the stack.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22  Type stack [int] declare constructors new () > stack; push (int, stack) > stack; destructors pop (stack) > stack; selectors top (stack) > int; isnew (stack) > bool; for all i in int; s in stack; let pop (new()) = error; pop (push (i,s)) = s; top (new()) = error; top (push (i,s)) = i; isnew (new()) = true; isnew (push(i,s)) = false; end end stack.  

The lines 1221 define the meaning (also known as the semantics) of the stack. It tells us what the concept of a stack is all about. The idea is to define equations that express how each destructor and each selector work on expressions formulated in terms of constructors. The equation in line 16 specifies that it is an error to pop the empty stack. The equation in line 17 specifies that pop applied on stack s on which we have just pushed the integer i is equivalent with s. Please consider the remaining equations and make sure that you understand their meaning relative to your intuition of the stack concept.
The specification in Program 49.1 tells us what a stack is. It is noteworthy that the specification in Program 49.1 defines the stack concept without any binding to a concrete representation of a stack. The specification gives very little input to the programmer about how to implement a stack with use of a list or an array, for instance. A good specification answers what questions, not how questions.
If you wish to see other similar specifications of abstract datatypes, you may review our specifications of natural numbers and booleans in Program 1.9 and Program 1.10 respectively.
Below, in Program 49.2 we show an axiomatic specification of a single function, namely the square root function. An axiomatic specification is formulated in terms of a precondition and a postcondition. The precondition specifies the prerequisite for activation of the square root function. It states that it is only possible to calculate the square root of nonnegative numbers. The precondition constrains the output of the function. In case of the square root function, the square of the result should be very close to the input.
1 2 3 4 5  sqrt(x: Real) > Real precondition: x >= 0; postcondition: abs(result * result  x) <= 0.000001  

In the rest of this lecture we will study objectoriented programming, in which methods can be specified with preconditions and postconditions.