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 49.3 Specifications 49.2 Correctness

 

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.

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

The programmers own, immediate comprehension Not formulated - not documented - volatile - easily forgotten Sometimes incomplete A program specification Formulated - written Well-considered and agreed upon Formal or informal Part of the program

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:

Algebraic specifications Equations that define how certain operations work on constructor expressions Axiomatic specifications Logical expressions - assertions - associated with classes and operations Often divided into invariants, preconditions, and postconditions

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.