Incorrect Answer.
The program P:
x = y;
if (x < z) { x = z; }
satisfies the Hoare triple
x < y 
P x = y
with respect to the partial correctness relation 
par, if
at any state satisfying "x < y", if the program
P terminates, then the resulting store satisfies "x = y".
- Case 1:
Assume that "x < z" evaluates to true when the flow of control passes on to
the if-statement. Then x gets assigned
the current value of z and terminates. Thus, "x = y" can only be true after
termination, if the current value of z equals the current value of y.
But as neither y nor z are ever updated in the program, this can only happen
if "z = y" holds in the initial state.
- Case 1:
Assume that "x < z" evaluates to false when the flow of control passes on to
the if-statement. Then the only effect of
executing P is the one of the assignment "x = y;" and, clearly, this formula
holds after program termination.
After this static analysis, we can easily construct
a to the claim of partial correctness above.
For case 1, consider the initial store in which the values of
x, y, and z are 2, 3, and 4, respectively. Notice that y and z have
different values and that the value of y is less than the one for z,
causing the if-statement to execute its first branch.
After P terminates, the values of x and y are 4 and 3, respectively.
Back to Question.
Next Question.