Incorrect Answer.
if (x > y) {
z = x + 1;
} 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 + 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 of the
expression x + 2.
- 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 of the
expression y + 2.
This case analysis reveals that, after program termination,
the value stored in z equals "the larger of the values stored in
x and y plus 2". Thus, we do not have the relationship claimed above.
Instead, we do have
parT P z =
max(x,y) + 2.
Back to Question.
Next Question.