Design-By-Contract Foundations
Every function and method in a software system does something. Before it starts that something , the routine may have some expectation of the state of the world, and it may be able to make a statement about the state of the world when it concludes. Meyer describes these expec- tations and claims as follows:
- Preconditions: What must be true in order for the routine to be called; the routine’s requirements. A routine should never get called when its preconditions would be violated. It is the caller’s respon- sibility to pass good data (see the box on page 115).
- Postconditions: What the routine is guaranteed to do; the state of the world when the routine is done. The fact that the routine has a postcondition implies that it will conclude: infinite loops aren’t allowed.
- Class invariants: A class ensures that this condition is always true from the perspective of a caller. During internal processing of a routine, the invariant may not hold, but by the time the routine exits and control returns to the caller, the invariant must be true. (Note that a class cannot give unrestricted write-access to any data member that participates in the invariant.)