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