Incorrect Answer.
if (x > y) {
z = y;
} else {
z = x;
}
z = z;
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 = y;", and then passes
control to the assignment statement "z = z;". The "final net effect" of these two assignments is that the value stored in z equals the value in y.
- If "x > y" evaluates to false in the initial store, then the program P
executes the else-branch of its if-statement, "z = x;", and then passes
control to the assignment statement "z = z;". The "final net effect" of these
two assignments is that the value stored in z equals the value in x.
This case analysis reveals that, after program termination,
the value stored in z equals the smaller of the values stored in
x and y. (What happens if the values stored in x and y are equal?)
Thus, the claimed relationship does not hold. But our analysis demonstrated
that
parT P z =
min(x,y)
is valid.
Back to Question.
Next Question.