PLP: Lecture 34
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