Design by contract

from Wikipedia, the free encyclopedia

Design by contract (short DbC , English for draft according to contract ) or Programming by Contract ('contract-based programming') is a concept from the field of software development . The aim is the smooth interaction of individual program modules through the definition of formal contracts for the use of interfaces that go beyond their static definition. It was developed and introduced by Bertrand Meyer with the development of the Eiffel programming language .

Basic principle

The smooth interaction of the program modules is achieved by means of a "contract" which, for example, must be adhered to when using a method . This consists of

  • Preconditions (English precondition ), that the assurances must comply with the caller
  • Postconditions (English postcondition ), that the assurances will comply with the callee, and the
  • Invariants (English class invariants ), basic assumptions that apply across all instances of a class.

The contract can refer to all available information, i.e. to variable and parameter contents as well as to object states of the object concerned or other accessible objects. As long as the caller adheres to the preconditions and invariants, no errors can occur and the method guarantees no unexpected results.

A weakened form of contracts is achieved in typed languages ​​by typing the input and output parameters. The type defines value ranges that can be interpreted as pre- and post-conditions. However, a type system is not able to capture the relationships between several parameters or relationships between input and output values. It therefore represents a significantly weakened form of protection compared to design by contract, but usually takes effect at translation time, while the assurances made in contracts only take effect if they are breached during runtime.

By defining class invariants, preconditions and postconditions, a module can be exchanged for any other module if it fulfills the same “contract”. For this, however, any identifiers and syntactic details used must be understood as pre- and post-conditions.

Invariants

Invariants are logical statements that apply to all instances of a class over the entire object life cycle. They usually appear in the form of class invariants , which are also allowed to access private properties of the class concerned. One therefore speaks of implementation invariants . Since invariants in current systems can only be checked before and after a method call, invariants within methods may well be violated temporarily . In this respect, they represent implicit preconditions and postconditions of every method call. An alternative to this approach would be to intercept any variable access using metaprogramming methods and thus also prohibit temporary violations of the invariants. However, this approach has not yet been pursued in current design by contract implementations.

Pre- and post-conditions

Each subprogram are preconditions ( preconditions ), and postconditions ( post conditions associated). The preconditions define the circumstances under which the subroutine should be callable. For example, a subroutine for reading from a file may only be called if the file has been successfully opened beforehand. The postconditions define the conditions that must be met after the subroutine call has been completed.

Pre- and post-conditions are formulated as Boolean expressions. If a precondition is not met (that is, its evaluation results in false , ie "not applicable"), there is an error in the calling code: It should have been ensured that the precondition is met. If a postcondition is not met, there is an error in the subprogram itself: The subprogram should have ensured that the postcondition is met.

Therefore, pre- and post-condition form a kind of contract (English contract ): If the calling code satisfies the precondition, then the subroutine is obliged to fulfill the postcondition.

Subclassing and contracts

Liskov's principle of substitution

Applying Liskov's principle of substitution to pre- and post-conditions, one obtains the following statement:

If the preconditions of the superclass are met before a method of the subclass is called, the method must meet the postconditions of the superclass.

This means that a method of a subclass is not free to design its pre- and post-conditions: It must at least fulfill the “contract” formulated by the pre- and post-conditions. That is, it must not tighten the preconditions (it must not demand more from the calling code than is required in the superclass), and it must not relax the postconditions (it must guarantee at least as much as the superclass).

Summary of the contractual terms of subclasses

In Design by Contract, subclasses must adhere to the following rules regarding the superclasses :

Formally, the relationship between the superclass and the subclass can be expressed as follows with regard to the preconditions and postconditions: 

 Vorbedingungsuper  →  Vorbedingungsub  
 Nachbedingungsub   →  Nachbedingungsuper

Review of the contractual terms of subclasses

The fulfillment of the logical implications described in the previous paragraph can only be checked algorithmically with great effort ( fulfillment problem ). A trick is therefore used in current implementations:

  • The preconditions are linked disjunctive (with logical OR). This can only weaken the precondition for the superclass, but not tighten it.
  • The postconditions are linked conjunctively (logical AND). As a result, the postcondition can only be tightened, but not weakened.
  • Invariants are also linked conjunctively.

Limitations of the procedure

Design by Contract can only be applied to software properties that can also be formulated as pre- and post-conditions. Conditions such as “Routine B must have been called before routine A” can be mapped using status variables. This means, on the one hand, increased effort for the programming of the class, on the other hand, users can dispense with keeping such an equipped object permanently under their control, but can pass it on to other functions and react to any status changes afterwards. Similarly, conditions such as “Routine A always calls routine B” (especially important in the object-oriented area) can be defined using postconditions and module invariants.

If an invariant is based on auxiliary objects, the invariant can be destroyed by aliasing . If invariants are also checked at the beginning of each subroutine, the destruction of the invariant can be reliably diagnosed before the program makes wrong decisions based on such an invariant violation, but the programmer does not receive any information about where the alias was created and when the auxiliary object was modified was actually destroyed.

If the semantics of a subroutine are completely summarized in preconditions, postconditions, and module invariants, a functional specification of the subroutine is obtained from which the actual subroutine could in principle be generated by means of the assurances. Such generators can be created from the compiler techniques for functional programming languages; in this respect, an approach driven to perfection according to Design By Contract indicates a step towards the next more abstract programming methodology.

Language support

Some less common programming languages ​​such as D and Eiffel support Design by Contract at least partially natively, including Ada since Ada 2012. From Version 4.0, the .NET Framework contains a class library (especially in the namespace System.Diagnostics.Contracts), which is also known as code contracts , for implementing Design by contract. The bean validation concept offers the same possibility in Java , and since Java Bean Validation 1.1 it has also been possible to implement pre- and post-conditions directly in method headers using annotations. This was previously possible using the OVal framework or the Java Modeling Language (JML for short) in Java. Other implementations such as GContracts for Groovy used APIs for compiler extensions to add appropriate language elements.

See also

Web links

Individual evidence

  1. ↑ msdn.microsoft.com
  2. ↑ Parameter constraints using Java Bean Validation 1.1
  3. ↑ Return value constraints using Java Bean Validation 1.1
  4. ↑ http://www.eecs.ucf.edu/~leavens/JML//index.shtml Accessed February 6, 2015
  5. ↑ github.com
Principles of object-oriented design


SOLID principles

Single Responsibility  • Open Closed  • Liskov Substitution Principle  • Interface Segregation  • Dependency Inversion

Further principles

Demeter's law  • Design by contract  • Data encapsulation  • Linguistic Modular Units  • Self-Documentation  • Uniform Access  • Single Choice  • Persistence Closure  • Command Query Separation  • Principle of Least Surprise

Packaging principles

Reuse Release Equivalence  • Common Closure  • Common Reuse  • Acyclic Dependencies  • Stable Dependencies  • Stable Abstractions