|
Design by Contract is a design technique developed by Bertrand Meyer [Meyer]. The technique is a central feature of the Eiffel language he developed. Design by Contract is not specific to Eiffel, however; it is a valuable technique that can be used with any programming language.
At the heart of Design by Contract is the assertion. An assertion is a Boolean statement that should never be false and, therefore, will be false only because of a bug. Typically, assertions are checked only during debug and are not checked during production execution. Indeed, a program should never assume that assertions are being checked.
Design by Contract uses three particular kinds of assertions: post-conditions, pre-conditions, and invariants. Pre-conditions and post-conditions apply to operations. A post-condition is a statement of what the world should look like after execution of an operation. For instance, if we define the operation "square root" on a number, the post-condition would take the form input = result * result, where result is the output and input is the input value. The post-condition is a useful way of saying what we do without saying how we do it梚n other words, of separating interface from implementation.
A pre-condition is a statement of how we expect the world to be before we execute an operation. We might define a pre-condition for the "square root" operation of input > = 0. Such a pre-condition says that it is an error to invoke "square root" on a negative number and that the consequences of doing so are undefined.
On first glance, this seems a bad idea, because we should put some check somewhere to ensure that "square root" 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. Without this explicit statement of responsibilities, we can get either too little checking梑ecause both parties assume that the other is responsible梠r too much梑oth parties check. Too much checking is a bad thing because it leads to a lot of duplicate checking code, which can significantly increase the complexity of a program. Being explicit about who is responsible helps to reduce this complexity. The danger that the caller forgets to check is reduced by the fact that assertions are usually checked during debugging and testing.
From these definitions of pre-condition and post-condition, we can see a strong definition of the term 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 an assertion about a class. For instance, an Account class may have an invariant that says that balance == sum(entries.amount()). The invariant is "always" true for all instances of the class. Here, "always" means "whenever the object is available to have an operation invoked on it."
In essence, this means that the invariant is added to pre-conditions and post-conditions associated with all public operations of the given class. The invariant may become false during execution of a method, but it should be restored to true by the time any other object can do anything to the receiver.
Assertions can play a unique role in subclassing. One of the dangers of inheritance is that you could redefine a subclass's operations to be inconsistent with the superclass's operations. Assertions reduce the chances of this. The invariants and post-conditions of a class must apply to all subclasses. The subclasses can choose to strengthen these assertions but 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, per the principle of substitutability. If a subclass strengthened its pre-condition, a superclass operation could fail when applied to the subclass.
| 
