Incorrect Answer.
The program P:
x = y;
if (x < z) { x = z; }
satisfies the Hoare triple
y = z 
P x < y
with respect to the partial correctness relation 
par, if
at any state satisfying "y = z", 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 is less than 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, making "x < y" false.
After this static analysis, we can easily construct
a to the claim of partial correctness above.
We saw that any terminating instance of case 2 renders a
counterexample. Consider the initial store in which
x, y, and z have values 2, 3, and 2, respectively.
Verify that this is indeed an terminating instance of case 2.
Back to Question.
Next Question.