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
- 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
- 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.