(of a statement S in some program) An assertion that characterizes the state of the program immediately after execution of S. The postcondition is expressed in terms of properties of certain program variables and relationships between them. Where a program text is annotated by attaching assertions, a postcondition is attached immediately after the statement to which it relates. See also precondition.