Design By Contract

Design By Contract is a design technique developed by Bertrand Meyer and a central feature of the Eiffel language that he developed. Design By Contract is not specific to Eiffel, however, and is a valuable technique for any programming language.

At the heart of design by contract is the assertion. An assertion is a Boolean statement. An assertion should never be false, and will only be false due to a bug. Typically assertions are only checked during debug and are not checked during production execution, indeed the program should never assume that assertions are being checked. Design By Contract uses three kinds of assertions: pre-conditions, post-conditions, and invariants.

Pre and post conditions are applied to operations. The post condition (it is easier to describe this first) is a statement of what the world should look like after an operation. For instance if we define the operation square on a number the post-condition would be of the form result = this * this (where result is the output and this is the object on which the operation was invoked). The post condition is a useful way of saying what we do, without saying how we do it, separating interface from implementation.

The pre-condition is a statement of how we expect the world to be before we execute the operation. Thus we might define a pre-condition for square of this >= 0. Such a pre-condition is saying that it is an error to invoke square on a negative number, and the consequences of doing so are undefined. On first glance this seems a bad idea, for we should put some check somewhere to ensure that square is invoked properly. The important question is who is responsible for doing so. The pre-condition makes it explicit that the caller is responsible for checking. Now without this explicit statement of responsibilities we can either get too little checking (because both assume the other is responsible) or too much (both check). Too much checking is a bad thing for it leads to lots of duplicate checking code which can significantly increase the complexity of a program. Being explicit about who is responsible helps to reduce this complexity. This danger that the caller forgets to check is reduced by the fact that assertions are usually checked during debugging and testing.

Out of this definition of pre and post condition we see a strong definition of an exception. An exception occurs when an operation is invoked with its pre condition satisfied, yet cannot return with its post-condition satisfied.

An invariant is a statement about a class. For instance a account class may have an invariant that says that balance == sum(entries.amount()). The invariant is 'always' true for all instances of the class. 'Always' means whenever the object is available to have an operation invoked upon it. In essence this means that the invariant is added to pre and post conditions of all public operations of the class. The invariant may become false during execution of a method, but should be restored by the time any other object can do anything to the receiver.

Assertions have a particular role in subclassing. One of the dangers of polymorphism is that you could redefine the subclass's operation in such a way as to be inconsistent with the superclass operation. The assertions stop you from doing this. The invariants and post-conditions of a class must apply to all subclasses. The subclasses can choose to strengthen these assertions but they cannot weaken them. The pre-condition on the other hand cannot be strengthened but may be weakened. This looks odd at first, but it is important to allow dynamic binding. You should always be able to treat a subclass object as if it were an instance of the superclass. If a subclass strengthened its pre-condition then a superclass operation could fail when applied to subclass. Essentially assertions can only increase the responsibilities of the subclass. Pre-conditions are a statement of passing a responsibility on to the caller, you increase the responsibilities of a class by weakening a pre-condition. In practice all this allows much better control of subclassing, and helps you to ensure that subclasses behave properly.

Ideally assertions should be included in the code as part of the interface definition. Compilers should be able to turn assertion checking on for debugging and remove it for production use. Various stages of assertion checking can be used. Pre-conditions often give you the best chances of catching errors for the least amount of processing overhead.

When to Use Them

Design by Contract is a very valuable technique that you should use whenever you program. It is a great technique for helping you build clear interfaces. Only Eiffel supports assertions as part of its language, and Eiffel is (sadly) not a widely used language. It is possible to add mechanisms to C++ and Smalltalk to support some assertions. Java is rather more problematic.

Where to Find Out More

[Meyer] is a classic book on OO design that talks a lot about assertions. [Waldén and Nerson] and [Cook and Daniels] use Design by Contract extensively in their books. You can also get more information from ISE (Bertrand Meyer's company).