Verified Design By Contract

If Design-by-Contract is new to you, then by all means have a quick glance through this section now, but there's no need to try to take in everything. It will become clearer by the end of this set of tutorials.

Design By Contract

If you have been brought up on Design By Contract (e.g. as supported by Eiffel), then you have already taken a step towards Verified Design By Contract provided by Perfect. But there are some important differences between DBC and VDBC.

First of all, in VDBC contracts are expressed in terms of an abstract data model, which may be very different from the eventual implementation model. The abstract data model is the simplest possible way of describing the essence of the data that is stored, avoiding any kind of redundancy or over-specification.

Second, in VDBC contracts are complete. In other words, the contract provides everything the client needs to know about what the method does.

A corollary to this is that in Perfect, postconditions are complete; that is, they specify precisely what variables are changed and how they are changed. In contrast, an Eiffel postcondition merely specifies something that must be true when the method returns.

In order to provide for partial method specifications that are inherited even when a method is overridden, Perfect provides an additional construct: the postassertion. A postassertion specifies everything the client can assume even in the presence of polymorphism.

To summarize: in Perfect:

• A method postcondition is a construct that says precisely which variables have changed and the conditions satisfied by the final values of those variables. It is not a Boolean expression - the syntax for postconditions is quite separate from the syntax for expressions. A Perfect postcondition has no equivalent in Eiffel (because, in Eiffel, to determine precisely what the method does, you have to look at the statements making up the method body). If you redefine (i.e. override) the method in a derived class, the Perfect postcondition is not inherited - you always supply a new one (just as, in Eiffel, you would supply a new method body).
• A method postassertion is a Boolean expression stating something that must be true when the method finishes. It must be a provable consequence of the postcondition. When you redefine the method in a derived class, the postassertion is inherited (and must be respected by the new postcondition). You can override the postassertion if you like, but the new postassertion must respect (i.e. imply) the old one. A Perfect postassertion performs a similar role to an Eiffel postcondition.

Next:  a Java example