| Design By Contract |
Article Index for Design |
Website Links For Design |
Information AboutDesign By Contract |
| CATEGORIES ABOUT DESIGN BY CONTRACT | |
| programming language topics | |
"Design by Contract" is also the name of a trademark of Eiffel Software, Inc. (formerly Interactive Software Engineering), the designers of Eiffel. Design by contract, '''DBC''' or '''Programming by contract''' 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 Type s and the Conceptual Metaphor of a legal Contract . DESCRIPTION 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 and during its implementation. Program execution is then viewed as the interaction between the various modules as bound by these contracts. For a description of DBC that attempts to depict the original model more closely, see wikibooks . In general, routines have explicit '' Precondition s'' that the caller must satisfy before calling the routine, and explicit '' Postcondition s'' 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 Assertion s 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:
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. LANGUAGES IMPLEMENTING DBC C Recent efforts add support for Design by Contract to the written in Ruby . Other tools supporting DBC for C include: C++ Tools supporting DBC for C++ include:
C# Tools supporting DBC for C# include:
Chrome The Chrome Programming Language is an Object Pascal implementation that has "class contracts", which are similar to DBC. D D implements Design by Contract as a major feature. 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. Java Tools supporting DBC for Java include:
JML The Java Modeling Language (JML) provides specifications, including contracts, to describe Java programs. Lisaac Lisaac implements Design by Contract as a major feature. Perl , and implements design-by-contract in Perl. Although the module is not widely used, it enjoys some popularity among Perl users involved in larger projects. Class::Agreement is a newer, less mature alternative. PHP PHP can implement design by contract via its assert() function and a callback function defined using assert_options() . PLT Scheme PLT Scheme , an extension of the Scheme Programming Language , implements a sound variant of Eiffel's DbC for modules, higher-order functions, and objects. The design of this system emphasizes that each contract violation must blame the guilty party and must do so with an accurate explanations. As Findler and Felleisen's papers carefully explain, this is ''not'' the case for Eiffel's system. Python Python supports DBC through tools like PyDBC and Contracts for Python . Ruby There are several external Design by Contract modules avilable for Ruby, including DesignByContract , Ruby DbC , and ruby-contract . Sather The Sather programming language implements Design by Contract. 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
EXTERNAL LINKS
|
|
|