Developing Loops

Start by expressing the postcondition Q, obtain an invariant I and guard B so that $I and ~B \supset Q$.

Design by Contract

Bertrand Meyer developed Eiffel in 1980’s to have more advanced assertions. In DbC, the specification given by preconditions and postconditions forms a contract. Satisfying the precondition is the responsibility of the caller. Satisfying the postcondition is the responsibility of the supplier.

Non-redundancy principle: under no circumstances shall the body of a routine ever test for the routine’s precondition (Avoid defensive programming)

Reasonable precondition principle:

  • Every routine precondition must be specified in the official documentation
  • Makes sense in terms of the specification only

Precondition availability rule

  • All the information needed for a client to check the precondition must be available to the client