Design by contract

It is based around the concept 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. The various modules are supposed to interact with each other according to these contracts. The conceptual metaphor of a legal contract is presumed by this terminology to be applicable to relationships internal to complex software designs.

In general, procedures have explicit preconditions, which must be satisfied for the procedure to work correctly, and explicit postconditions, which they guarantee will be true at the end of the procedure. Loops can also have loop invariant conditions, which must stay valid throughout the execution of the loop.

A contract takes the 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.

Where DBC is novel is making these contracts executable, so that they are defined by program code in the programming language itself, rather than by code in a meta-language. This is similar on the surface to the use of "assertion"s in the C programming language, but goes much deeper.

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:

• Accepted and nonaccepted 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 "fail hard" property paradoxically makes debugging for correct behavior much easier.

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.

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. They have also argued that without some common strong concept of what the argument data types are, a contract between higher-level entities is almost worthless. A regression approach is required, to ensure that lower level types behave as expected. Since this is very high overhead, it is unlikely to be carried out deeply, and therefore the risk that the overall system will 'fail hard' is thus increased.

Note: "Design by Contract" is a trademark of Interactive Software Engineering, the designers of Eiffel.

See also:

• Hoare logic