Design by contract
|
|
Design by contract or DBC is a methodology for designing computer software. It prescribes that software designers should define precise checkable interface specifications for software components based upon the theory of abstract data types and the conceptual metaphor of a legal contract.
The central idea of DBC is that software entities have obligations to other entities based upon formalized rules between them. A functional specification, or 'contract', is created for each module in the system before it is coded. Program execution is then viewed as the interaction between the various modules as bound by these contracts.
In general, routines have explicit preconditions that the caller must satisfy before calling the routine, and explicit postconditions that describe the conditions that the routine will guarantee to be true after the routine finishes. Thus, a contract takes the following general form: "If you, the caller, set up certain preconditions, then I will establish certain other results when I return to you. If you violate the preconditions, then I promise nothing." Each module's implementation can then be written assuming the correctness of the modules it uses (its subcontractors), as long as it satisfies their preconditions.
Many languages have facilities to make assertions like these. However, DBC is novel in recognizing that these contracts are so crucial to software correctness that they should be part of the design process. In effect, DBC advocates writing the assertions first.
The notion of a contract extends down to the method/procedure level; the contract for each method will normally contain the following pieces of information:
- Acceptable and unacceptable inputs
- Return values, and their meanings
- Error and exception conditions that can occur
- Side-effects
- Preconditions
- Postconditions
- invariants
- (Rarer) Performance guarantees, e.g., for time or space used
Using the DBC methodology, the program code itself must never try to verify the contract conditions; the whole idea is that code should "fail hard", with the contract verification being the safety net. (This stands in stark contrast to the defensive programming methodology.) DBC's "fail hard" property makes debugging for-contract behavior much easier because the intended behaviour of each routine is clearly specified.
The contract conditions should never be violated in program execution: thus, they can be either left in as debugging code, or removed from the code altogether for performance reasons.
All class relationships are between Client classes and Supplier classes. A Client class is obligated to make calls to Supplier features where the resulting state of the Supplier is not violated by the Client call. Subsequently, the Supplier is obligated to provide a return state and data that does not violate the state requirements of the Client. For instance, a Supplier data buffer may require that data is present in the buffer when a delete feature is called. Subsequently, the Supplier guarantees to the client that when a delete feature finishes its work, the data item will, indeed, be deleted from the buffer. Other Design Contracts are concepts of "Class Invariant". The Class Invariant guarantees (for the local class) that the state of the class will be maintained within specified tolerances at the end of each feature execution.
Unit testing tests a module in isolation, to check that it meets its contract assuming its subcontractors meet theirs. Integration testing checks whether the various modules are working properly together. Design by contract also fosters code reuse, since the contract for each piece of code is fully documented. The contracts for a module can also be regarded as a form of software documentation for the behavior of that module.
| Contents |
Languages implementing DBC
Eiffel
The object oriented Eiffel programming language was created to implement Design by Contract. However, the ideas behind DBC are applicable to many programming languages, both object-oriented and otherwise.
Critics of DBC, and Eiffel, have argued that to 'fail hard' in real life situations is sometimes literally dangerous. In an attempt to address this, Eiffel treats contract breaches as exceptions that can be caught, allowing a system to recover from its own defects. The degree to which this approach succeeds is arguable.
D
D implements Design by Contract as a major feature.
Lisaac
Lisaac implements Design by Contract as a major feature.
SPARK
The SPARK programming language implements Design by Contract by static analysis of Ada programs. By using static analysis SPARK ensures that no contract is ever broken at run-time. This means that Eiffel's problematic 'fail hard' situation will never occur on SPARK.
See also
- Hoare logic
- D programming language
- Eiffel programming language
- SPARK programming language
- Lisaac Présentation générale du langage lisaac
- Test-driven development
External links
- Isaac / Lisaac Project home (http://www.isaacos.com)
- C2 Wiki: Design by contract (http://c2.com/cgi/wiki?DesignByContract)
Note: "Design by Contract" is a trademark of Eiffel Software, Inc. (formerly Interactive Software Engineering), the designers of Eiffel.