Table of Contents

About

A Design By Contract (DBC) model is based on the fact that a computation, given correct input, must terminated with a correct output. This assertion notion is central in a DBC design. If any assertion evaluates to false, the software system is considered as invalid.

Bertrand Meyer developed DBC as part of his Eiffel programming language.

This is also known as:

  • contract-driven
  • contract-first

Three roles collectively defines what is called the design-by-contract model of programming

  • Precondition: A condition that the caller of an operation agrees to satisfy. The user invoking the computation has the responsibility of providing the correct input.
  • Post-condition: A condition that the method itself promises to achieve. If the computation is successful, the computation has satisfied the post-condition.
  • Invariant: A condition that should always be true at a specified point of a program

Documentation / Reference