Design by contract
From Free net encyclopedia
←Older revision | Newer revision→
- DBC also stands for Direct Bonded Copper, a Power electronic substrate
- "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 types and the conceptual metaphor of a legal contract.
Contents |
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 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 input values or types (c.f. type bounds for Java 5 generics)), and their meanings
- Return values or types (c.f. type bounds for Java 5 generics), and their meanings
- Error and exception conditions values or types (c.f. type bounds for Java 5 generics), that can occur, and their meanings
- 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.
Languages implementing DBC
C
Recent efforts add support for Design by Contract to the C programming language using DBC for C, a preprocessor written in Ruby.
Other tools supporting DBC for C include:
C++
Tools supporting DBC for C++ include:
- C2.
C#
Tools supporting DBC for C# include:
- eXtensible C#, a commercial post-compiler that transforms "declarative assertions", in the form of .NET attributes attached to C# methods and properties, into actual pre- and post-conditions embedded in the compiled .NET IL code.
- Spec#, a Microsoft research extension of the C# language.
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:
- iContract2, a free Java source pre-processor/code-generator that uses Javadoc tags to specify preconditions, postconditions, and invariants
- Contract4J, a DBC tool where tests are defined using Java 5 annotations and aspects written in AspectJ evaluate the test expressions at runtime and handle failures.
- jContractor, which provides runtime contract checking by instrumenting the bytecode of classes that define contracts
- Jcontract, a proprietary DBC tool by Parasoft
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
Damian Conway's Class::Contract module, now maintained by C. Garrett Goebel, is available from CPAN, 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 external DesignbyContract modules avilable for Ruby. One of the better ones is DesignByContract
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
- Hoare logic
- D programming language
- Eiffel programming language
- SPARK programming language
- Test-driven development
External links
- An introduction to Design by Contract(TM)
- Isaac / Lisaac Project home
- C2 Wiki: Design by contract
- Damian Conway's Class::Contract Perl module from CPAN
- dlib C++ Library A C++ library that uses the DBC methodologyde:Design By Contract