Contract Programming

Contract programming ( design by contract (DbC), programming by contract , contract-based programming ) is a software design method. He suggests that the designer should define formal, accurate, and verifiable interface specifications for system components. In addition to the usual definition of abstract data types, preconditions , postconditions and invariants are also used. These specifications are called "contracts" in accordance with the conceptual metaphor of conditions and liability in civil law contracts.

Story

The term suggested by Bertrand Meyer in connection with the development of the Eiffel language. Contract programming has grown out of formal verification, formal specification and Hoare logic. Contract programming is not only a simple metaphor that indicates a design method. Conditions facilitating the use of contract programming:

• the presence of inheritance and the possibility of dynamic binding,
• the ability to handle exceptions,
• possibility of automatic software documentation.

Description

rice contract module design

The main idea of ​​contract programming is a model of interaction of elements of a software system based on the idea of ​​mutual obligations and benefits . As in business, the customer and the supplier act in accordance with a specific contract . A contract of a certain method or function may include:

• specific obligations that any client module must fulfill before calling the method — preconditions that give an advantage to the supplier — it may not check whether the preconditions are fulfilled;
• specific properties that must be present after the implementation of the method - postconditions that are included in the obligations of the supplier;
• obligations for the implementation of specific properties - invariants that must be fulfilled when the supplier receives the message, as well as when leaving the method.

Many programming languages ​​allow for such commitments. Contract programming implies these requirements are critical to the correctness of programs, so they must be approved during design. Thus, contract programming prescribes starting to write code with writing formal assertions of correctness (assertions).

In object-oriented programming, a method contract usually includes the following information:

• possible types of input data and their meaning;
• return types and their meanings;
• conditions for exceptions, their types and values;
• the presence of a side effect of the method;
• preconditions that can be relaxed (but not strengthened) in subclasses;
• postconditions that can be strengthened (but not weakened) in subclasses;
• invariants that can be strengthened (but not weakened) in subclasses;
• (sometimes) performance guarantees, such as temporary complexity or memory complexity.

When using contracts, the code itself is not obliged to verify their implementation. Usually in such cases, the code makes a hard drop [ clarify ] (“ fail-fast ”), thus facilitating the debugging of the execution of contracts. In many languages, such as C, C ++, Delphi, PHP, this behavior is implemented by the assert operator. In the release version of the code, this behavior can be saved, or checks can be removed to improve performance.

Unit tests check the module in isolation from others, checking that the module meets the assumptions of the contract, and also the modules used by it fulfill their contracts. Integration tests verify that the modules work correctly together.

Contract programming can increase code reuse as the module’s commitments are clearly documented. In general, a module contract can also be viewed as a software documentation method.

Implementation in programming languages

DbC language support

Languages ​​that initially support tools for contract programming:

• Ada 2012
• Clojure
• Cobra
• D [1]
• Eiffel
• Fortress
• Lisaac
• Nice
• Oxygene (formerly Chrome)
• Racket
• Sather
• Scala
• SPARK through static analysis programs in Ada
• Spec #
• SeC (C language extension)
• J @ va (Java language extension)
• C # (with .NET Framework 4.0)

DbC support with third-party libraries

• C and C ++ via CTESK, the Contract ++ library, the DBC for C preprocessor, GNU Nana, or the C ++ compiler from Digital Mars.
• C # via Code Contracts
• Java via JavaTESK, iContract2, Contract4J, jContractor, Jcontract, C4J, CodePro Analytix, STclass, Jass preprocessor, OVal with AspectJ, Java Modeling Language (JML), SpringContracts for Spring Framework, or Modern Jass, Custos using AspectJ, JavaDbC using AspectJ, cofoja (developed by Google).
• JavaScript via Cerny.js or ecmaDebug.
• Lisp
  • Common Lisp using macros or the CLOS metaobject protocol.
  • Scheme through the expansion of PLT, namely the fact that any breach of contract should indicate the culprit and have an accurate explanation. [1]
• Nemerle with macros.
• Perl using CPAN modules Class :: Contract (Damian Conway) or Carp :: Datum (Raphael Manfredi).
• Php using phpDeal
• Python using the zope.interface package, PyDBC or Contracts for Python.
• Ruby using DesignByContract (by Brian McCallister), Ruby DBC, or ruby-contract.

Common tools

• Perfect Developer, using the Perfect specification language, can verify a contract using static code analysis and generating programs in languages ​​like C ++ and Java.