A postcondition is a Boolean condition that must be true when a function or operation returns. When its precondition was satisfied, the function is responsible for establishing the postcondition before returning. section 6.3.3
Use postconditions to make successful behavior explicit:
- After add() succeeds on a non-full circular buffer, the buffer contains the new value and is not empty: self._count > 0. section 6.3.3
- After remove() succeeds on a non-empty circular buffer, it returns a value and the buffer is not full: self._count < self._capacity. section 6.3.3
- If the operation cannot establish its promised result, raising an exception changes the contract to successful completion or an exception. section 6.3.3
A contract for a circular buffer
A caller first confirms that add() or remove() can legally run. The method then performs its operation and checks the resulting state before returning. A failed check may abort in a demonstration; an application can instead raise an exception. This separates the caller’s precondition responsibility from the function’s postcondition responsibility. section 6.3 section 6.3.3
Postconditions make method behavior predictable. Together with preconditions and a class invariant, they form a programming-by-contract description that helps prevent objects from being left in invalid states. section 6.3 section 6.4
