Design by Contract

A full tutorial on Design by Contract is beyond the scope of this chapter. The following section gives a brief introduction to the basic concepts and the purpose of contracts. Readers who are familiar with those concepts may want to skip them.

Pre- and Postconditions

The basic components of Design by Contract are preconditions and postconditions. Both are sets of logical (Boolean) expressions, with no side effects, that are attached to individual methods.^[2] They describe semantic properties that are required to hold when the respective method is executed.

^[2] As a recent discussion in some newsgroups showed, the concept of side effect freeness is somewhat hard to define. We do not discuss it in this chapter but only give an intuitive definition: Pre- and postconditions must not alter the state of the system they describe.

Preconditions describe the required conditions for the method to return a reasonable result. They are checked before the actual method is executed. Postconditions describe to some extent the expected result of the method, provided the preconditions were kept. Postconditions are checked after method execution but before returning to the calling context.

Invariants

Class invariants are contracts attached to a class that are to be checked as both preconditions and postconditions and that are checked for every public method of a class. Therefore, most of what is said about either of the other two kinds of contracts is also valid for class invariants.

The rest of the chapter therefore in most cases addresses only preconditions and postconditions. Class invariants are discussed only where they differ from the other two.

Inheritance

Contracts are, by definition, inheritance-aware: The methods of a subclass must obey the rules given by its superclass [Meyer1997; Liskov1998]. When method m of class A is overwritten in subclass B, the contracts for A.m must also automatically be checked for B.m.

Furthermore, subclasses must require no more than their superclass that is, they can only weaken preconditions. Conversely, they must promise at least what their superclass does. So they can only strengthen postconditions. This is usually implemented by combining all preconditions for a method in an inheritance chain with a logical or and all postconditions with a logical and.

Implementing Contracts

A detailed discussion of different implementations is beyond the scope of this chapter. Instead, we point the reader to existing products such as iContract for Java or the Eiffel language.^[3]

^[3] See http://www.reliable-systems.com and http://www.eiffel.com.

An implementation of Design by Contract should provide some tools for formulating contracts, either in a repository or inlined in the method and class code. It should enable switching on and off contract checking for performance. It should offer additional constructs beyond the standard logical operators, such as the following.

• old in postconditions provides access to the state of a variable at the time of the method call that is, when the precondition was checked. This is necessary to compare the old versus the new state of the variable.

• forall in pre- and postconditions checks a condition against all elements of a collection.

• exists in pre- and postconditions checks whether at least one element of a collection satisfies a condition.

Why Contracts?

In their article [Jézéquel+1999], Jean-Marc Jézéquel and Bertrand Meyer comment on the Ariane 5 disaster, in which a $500 million rocket exploded about 40 seconds after takeoff because of a software failure. They cite the official analysis of that incident, stating that a piece of software reused from the predecessor Ariane 4 was called in a situation that violated its implicit preconditions, crashing the system. They claim that having the routine's contract stated explicitly would have made finding this violation much easier and would probably have prevented the system crash.

Although not all software defects cause such spectacular crashes, contracts do provide a means to tell a developer about the constraints and promises of a piece of code. Particularly when reusing existing code that has been around for a while or that was developed by third parties, this can give quality assurance teams a hint of what to look out for. Sometimes, contracts may even help discover defects nobody was expecting, simply because they are enforced automatically.

Contracts Versus Assertions

The logical expressions that constitute pre- and postconditions are frequently referred to as assertions. For this reason, they are sometimes mistaken as the assertions known in C and similar programming languages. However, they are both more and less powerful than those. They are more powerful in that they are aware of inheritance and polymorphism. They are also less powerful because they can only be attached to method invocations and returns, while assertions can be interspersed in a method's code. We have therefore mostly avoided the term "assertion" in this chapter.

Contracts can be implemented using assertions, but it takes additional effort besides writing down the plain assertions themselves. The additional operators have to be provided, and more important their behavior with respect to inheritance has to be simulated.