In software engineering, a explicit logical statement that must evaluate to true
on completion of a method or component. (Compare with precondition and invariant).
In the design by contract paradigm, pioneered by the Eiffel language, postconditions
are embodied as formal assertions that are tested on method exit.
Failure of a postcondition usually denotes an error in the component itself,
termed the "supplier".
Postconditions are often relegated to documentation of a method (if, of course,
there is any documentation at all), and are unfortunately considered trivial and,
as such, remain implicit. However, a full set of postconditions determines the
precise behavior of a component and as such is important validation that a
software component correctly implements the software design. It is perhaps
surprising that precisely describing what a component does is such a difficult task,
but it requires considerable attention to detail. For example, the postcondition
for a simple method such as adding an object to a collection data structure
would explicitly state what happens if the object is already in the collection,
and that the resulting collection still contains any previous items, the new object,
and no others.
Postconditions tested at runtime can detect a component failure but may be
considered computationally expensive. In addition, a suitably robust application
would have to specify suitable behavior in the event of a component failure. It is
evidently beneficial to validate postconditions before deployment in a
production environment. Unit testing is a convenient best practice to do so.