In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification.
Often, postconditions are simply included in the documentation of the affected section of code.
In some software design approaches, postconditions, along with preconditions and class invariants, are components of the software construction method design by contract.
[1] As it relates to the routine's contract, the postcondition offers assurance to potential callers that in cases in which the routine is called in a state in which its precondition holds, the properties declared by the postcondition are assured.
The following example written in Eiffel sets the value of a class attribute hour based on a caller-provided argument a_hour.