Determine the post-condition given the precondition?
This question is so simple, one gets the impression that you don’t know what a post condition is. A pre-condition says what you know about the state of the world before the statement is executed. A post-condition says what you know about the state of the world after the statement is executed and is based on the nature of the statement and the precondition. For example: { x != 0 } x := x^2 gives { x > 0 } because whether x is positive or negative, its square is not negative, and is 0 if and only if x started out 0. Or: { x < 5 } x := x + 3 gives { x < 8 } because if x starts out less than 5 and we add 3 to x, then x has to end up less than 8.
