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 mathematically-oriented specifications, the following two variants are well-known:
|
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 4-11 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 12-21 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 non-negative 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 object-oriented programming, in which methods can be specified with preconditions and postconditions.