Determine the post-condition given the precondition?

Question

{x<5-y} x := x+y

Answer 1

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.

In your case, the pre-condition is equivalent to { x+y < 5 }