A postcondition is a Boolean condition that must be true when a function returns or a use case finishes. In programming by contract, callers establish preconditions; the operation is responsible for meeting its postcondition before returning. section 6.3.3 section 3.7.2
Use postconditions to make successful completion explicit:
- For a CircularBuffer add(), a successful return means the value was added and the buffer is not empty; count must be greater than zero. section 6.3.3
- For remove(), a successful return means a value was removed and the buffer is not full; count must be less than capacity. section 6.3.3
- A failed postcondition may abort during an example, but an application can throw an exception; the contract then becomes success or exception. section 6.3.3
Shipping days
Shipment.calculate_days() promises days between 0 and 14. Expedited narrows that promise to 1 or 2 days, while International requires more than 12 days. Subclass postconditions must remain compatible with the superclass promise, or callers using Shipment can receive an invalid result. section 7.5
