Incorrect Answer.
if (x > y) {
z = x;
} else {
z = y + 1;
}
z = z - 1;
For the relation 
par
T
P z =
max(x,y) to hold, it has to be the
case that at any state satisfying T ("true"), if the program
in question terminates, then the resulting store satisfies "z =
max(x,y)". This is not the case for the P above. For
consider any terminating run of the program:
- If "x > y" evaluates to true in the initial store, then the program P
executes the first branch of its if-statement, "z = x;", and then passes
control to the assignment statement "z = z - 1;". The "final net effect" of these two assignments is that the value stored in z equals the value of the
expression x - 1.
- If "x > y" evaluates to false in the initial store, then the program P
executes the else-branch of its if-statement, "z = y + 1;", and then passes
control to the assignment statement "z = z - 1;". The "final net effect" of these
two assignments is that the value stored in z equals the value in y.
This case analysis reveals that, after program termination,
the value stored in z equals the larger of the values stored in
x and y in case that y is larger than x. Otherwise, the program is
"off" by one as it returns the value of x - 1 and not the value of x,
as desired.
Back to Question.
Next Question.