CS656/556 Notes on Assertions

Assertions have been a part of prgramming since the time of Von Neuman. This document discribes the various types.

At first assertions appeared as annotations or comments added to the design for a program. These designs where expressed as flowcharts. The annotaions where statements that would be true any time the program went through them. In 1967 Robert W Floyd named them invariants and showed how they could provide semantics to a flowchart ( "Assigning Meaning to Programs", pp19-32 of Proceedings of Symposia in Applied Mathematics Vol XIX ). Donald Knuth used them in his monumental "Art of Computer Programming". These assertions were logical statements attached to a point in a program. They were used by programmers trying to write and/or understand the code. We used them to check that the code worked. Typically, there was one for each branch and loop in a program. I used theme for key parts of my Ph. D. work. They made sure that no bugs were ever found in the key parts of the program (bugs appeared where I didn't use assertions).

With the development of modular programs and high level languages we learned to document pre-conditions and post-conditions for each subprogram. A pre-condition is written at the start of a subprogram. It states the conditions that can be assumed by the subprogram when it starts. Pre-conditions are to be set up by the clients of the subprogram. For example the pre-condition for a square root routine is that the argument is not negative. A post-condition states what is going to be true when the subprogram exits. Conceptually they belong at the end the code.

Programmers also got into the habit of coding executable assertions. An executable assertion does nothing if the condition was true. If it is false, the program halts and an error message is displayed -- this must state which subprogram has the problem and the condition that is broken. I used this style in a successful team project in the early 1970s. Pre and post conditions are now a part of object-oriented programming and the UML. They can be used to document functions so that they can be used without studying the code inside. In the following "i0" stands for the value of i when the function is called. This allows the value of i to change as the function is executed.

int isqrt(int i);

// pre: i == i0 and i0 >=0

// post: n is returned where n*n <= i0 <(n+1)*(n+1)

When C was created, a special library <assert.h> was developed that supported executable assertions. See the manual on the other side of this piece of paper. Here is an executable C/C++ pre-condition:

int isqrt(int i)

{ assert( i >=0 ));

A pre+post-condition pair is now called a contract. They are the heart of a programming method and language developed by Bertrand Meyer (Object-Oriented software construction, Prentice Hall QA76.6 M4845 1988, pages 111..128). He also reintroduced the idea of an invariant at the class level. A class invariant is a property of objects of a given class. Whenever no function is executing the invariant is true. Proving it true is not difficult: just show that every constructor and every method guarantees that the invariant is still true. Then, the code in each method can assume that the invariant is true.

Recently, executable assertions have been given a new use in extreme programming. This is as unit tests. A unit test tests to see if a module is working correctly. They are written outside the code being tested. In extreme programming you always write a set of test cases first and then start working to make the code pass the tests.

for ( i = 0; i<30; i++)

{ n = isqrt(i);

assert( (n*n <= i) && (i < (n+1)*(n+1)));

}