What is Verified Design-by-Contract?

Verified Design-by-Contract is the natural evolution of Design-by-Contract, which was a new name (introduced with the Eiffel programming language) for some well-established but under-used principles. It is a correct by construction approach to developing software.

The basic principles of Design-by-Contract are:

• For each class method, a precondition and a postcondition are specified;
• Whenever a class method is called, the client and the method are bound by a contract. The client guarantees to satisfy the precondition at the point of call; in return the method guarantees to satisfy the postcondition at the point of return;
• To assist in ensuring that contracts are honoured, additional elements such as class invariants and assertions may be included in the specification.

While the basic Design-By-Contract principle is a powerful addition to software development techniques, it is hard to ensure that all contracts are honoured. When applied to software developed in traditional programming languages and enhanced by notation for contracts, then typically only limited verification of contracts is possible, because:

• The specified contracts are frequently incomplete (often because the notation used is not expressive enough);
• Even with class invariants and assertions, insufficient information is available to prove that contracts are honoured;
• Contracts are most naturally and simply expressed in terms of a simple abstract data model of a class, whereas the programming language only allows the implementation model to be described;
• The presence of unconstrained polymorphism and reference aliasing introduce too many unknowns;
• The contracts may be incorrectly specified and not meet the requirements.

Verified Design-by-Contract, as supported by Perfect Developer and the Escher C Verifier, avoids these issues.

In Perfect Developer:

• Contracts are completely specified (without unnecessarily constraining the implementation);
• Contracts are expressed in terms of an abstract data model, which has a specified relationship to the implementation model (if different);
• Additional information such as ghost methods, recursion variants and post-assertions completes the information needed to make manual or automatic verification of contracts possible;
• Polymorphism and aliasing occur only on demand instead of by default;
• Required or expected behaviour of classes and methods may be described in addition to the basic contracts.

By extending the Design-by-Contract principle in this way and using advanced Automated Reasoning technology, Perfect Developer provides verification from requirements right through to code - hence Verified Design-by-Contract.

More information is available in this paper.