Design by Contract
Correctness of programs
e.g. European Space Agency (ESA) Arianne 5 Crash
- $500 million loss
- Code ok, for16-bit Ariane 4,
but failed for Ariane 5.
- Cause of failure:
A conversion from a 64-bit floating-point number (the mission’s "horizontal bias") to a 16-bit signed integer produced an exception because the number was not representable with 16 bits.
Preconditions and Postconditions and other class assertions.
In Eiffel, The Precondition of a routine is the assertion designated by 'require'
The postcondition is designated by 'ensure'
Example:
Square_root(x:REAL):REAL is
require: x >= 0
<function body>
ensure: Result*Result = x
The class invariant is an assertion 'global' to all routines in the class.
By giving a precise precondition and postcondition of a routine we are in effect specifying what the routine is supposed to do.
From B. Meyer
quote:
Specification and debugging
To improve software reliability, the first and perhaps most difficult problem is to define as precisely as possible, for each software element, what it is supposed to do. The immediate objection is that specifying a module's purpose will not ensure that it will achieve that specification; this is obviously true, but:
- One may reverse this proposition and note that it we don't state what a module should do, there is little likelihood that it will do it. (The law of excluded miracles.)
- In practice, it is amazing to see how far just stating what a module should do goes towards helping to ensure that it does it.
... the presence of a specification, even if it does not fully guarantee the module's correctness, is a good basis for systematic testing and debugging.
end quote
Design by Contract
- A method for building reliable software
- Based on metaphor of business contracts
- Basic ideas applicable to all languages
- Built-in into Eiffel language and tools
Writing a program is a like a contract between the supplier and the client.
The supplier routine will deliver the result specified by the postcondition, as long as the client (calling) routine fulfills the requirements of the precondition.
- The precondition binds the client: it defines the conditions under which a call to the routine is legitimate. It is an
obligation for the client and a benefit for the supplier.
- The postcondition binds the class: it defines the conditions that must be ensured by the routine on return. It is a benefit for the client and an obligation for the supplier.
See page 342 OOSC 2nd Ed
Example:
A client routine of the square_root program must supply an value >= 0, otherwise the supplier routine will not provide the proper result.
Defensive Programming is Bad
In the case of the square_root program, defensive programming could use instead of a precondition, a defensive 'if -then' e.g.
Square_root(x:REAL):REAL is
if x < 0 then
<output error message>
else
<function body>
end
Problems with Defensive Programming:
- Complexity:
By adding possibly redundant checks, you add more software; more software means more complexity, and in particular more sources of conditions that could go wrong; hence the need for more checks, meaning more software; and so on ad infinitum.
- Costs:
Redundant checks imply a performance penalty — often enough in practice to make developers wary of defensive programming regardless of what the textbooks say.
Example of Class with Assertions
see pg 11-12 Invitation to Eiffel (.pdf version)