Design by contract

contractscontractdesign contractdesign-by-contractprogramming by contractsoftware contractsCodeContractscontract systemscontractually obligedstatically checked contracts
Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software.wikipedia
133 Related Articles

Bertrand Meyer

Bertrand Meyer English Wikipedia HoaxBertrand Meyer § Wikipedia hoaxMeyer, Bertrand
The term was coined by Bertrand Meyer in connection with his design of the Eiffel programming language and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction.
He created the Eiffel programming language and the idea of design by contract.

Eiffel (programming language)

EiffelEiffel programming languageEiffel language
The term was coined by Bertrand Meyer in connection with his design of the Eiffel programming language and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction.
Both are based on a set of principles, including design by contract, command–query separation, the uniform-access principle, the single-choice principle, the open–closed principle, and option–operand separation.

Abstract data type

abstract data typesabstract data structureabstract
It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.
However, various language features correspond to certain aspects of ADTs, and are easily confused with ADTs proper; these include abstract types, opaque data types, protocols, and design by contract.

Precondition

pre-preconditionspre-condition
It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.
Preconditions in object-oriented software development are an essential part of design by contract.

Unit testing

unit testunit testsunit
Design by contract does not replace regular testing strategies, such as unit testing, integration testing and system testing.
A unit test provides a strict, written contract that the piece of code must satisfy.

Inheritance (object-oriented programming)

inheritancesuperclasssubclass
Subclasses in an inheritance hierarchy are allowed to weaken preconditions (but not strengthen them) and strengthen postconditions and invariants (but not weaken them).
For example, in Eiffel, contracts that define the specification of a class are also inherited by heirs.

Object-Oriented Software Construction

Object Oriented Software Construction
The term was coined by Bertrand Meyer in connection with his design of the Eiffel programming language and first described in various articles starting in 1986 and the two successive editions (1988, 1997) of his book Object-Oriented Software Construction.
It starts with an examination of the issues of software quality, then introduces abstract data types as the theoretical basis for object technology and proceeds with the main object-oriented techniques: classes, objects, genericity, inheritance, Design by Contract, concurrency, and persistence.

Assertion (software development)

assertionsassertionassert
Many programming languages have facilities to make assertions like these.
This forms an important part of the method of design by contract.

Object-oriented programming

object-orientedobject orientedobject-oriented programming language
Similarly, if the method of a class in object-oriented programming provides a certain functionality, it may:
Essential to the quality focus of Eiffel is Meyer's reliability mechanism, Design by Contract, which is an integral part of both the method and language.

Postcondition

postconditionspost-conditions
It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.
In some software design approaches, postconditions, along with preconditions and class invariants, are components of the software construction method design by contract.

Liskov substitution principle

Inheritance semanticssubstitutabilitybehavioral subtyping
These rules approximate behavioural subtyping.
In the same paper, Liskov and Wing detailed their notion of behavioral subtyping in an extension of Hoare logic, which bears a certain resemblance to Bertrand Meyer's design by contract in that it considers the interaction of subtyping with preconditions, postconditions and invariants.

D (programming language)

DD programming languageD language
Type inference, automatic memory management and syntactic sugar for common types allow faster development, while bounds checking, design by contract features and a concurrency-aware type system help reduce the occurrence of bugs.

Ada (programming language)

AdaAda programming languageAda 83
It has built-in language support for design-by-contract, extremely strong typing, explicit concurrency, tasks, synchronous message passing, protected objects, and non-determinism.

Software documentation

documentationonline documentationuser documentation
The contracts for a module can be regarded as a form of software documentation for the behavior of that module.
Often, tools such as Doxygen, NDoc, Visual Expert, Javadoc, EiffelStudio, Sandcastle, ROBODoc, POD, TwinText, or Universal Report can be used to auto-generate the code documents—that is, they extract the comments and software contracts, where available, from the source code and create reference manuals in such forms as text or HTML files.

Invariant (mathematics)

invariantinvariantsinvariance
It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.
The theory of optimizing compilers, the methodology of design by contract, and formal methods for determining program correctness, all rely heavily on invariants.

Formal methods

formal methodformalformal analysis
It prescribes that software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.

SPARK (programming language)

SPARKSPARK programming languageSPARK/Ada
The SPARK language consists of a well-defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification.

Test oracle

oracle
The use of assertions can be considered to be a form of test oracle, a way of testing the design by contract implementation.
However, method postconditions are part of the system under test, as automated oracles in design by contract models.

Class invariant

class invariantsinvariantinvariant of the class
Other design contracts are concepts of class invariant.
The class invariant is an essential component of design by contract.

Comment (computer programming)

commentcommentsREM
Contracts can be written by code comments, enforced by a test suite, or both, even if there is no special language support for contracts.
Comments are sometimes used to document contracts in the design by contract approach to programming.

Spec Sharp

Spec#Sing#Spec# language
Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions.

Offensive programming

When using contracts, a supplier should not try to verify that the contract conditions are satisfied—a practice known as offensive programming—the general idea being that code should "fail hard", with contract verification being the safety net.

Sather

Sather programming language
Sather also takes inspiration from other programming languages and paradigms: iterators, design by contract, abstract classes, multiple inheritance, anonymous functions, operator overloading, contravariant type system.

Nice (programming language)

Nice
Nice aims to be feature-rich, and as such, in addition to the common features of modern object-oriented programming languages, it implements contracts in the style of Eiffel, class extensibility through multimethods, and many concepts drawn from functional programming such as anonymous functions, tuples, pattern matching (“value dispatch”), and parametric polymorphism.