postcondition (condition + post-; after)
A condition that must be met immediately after execution of some piece of code