Logic Web Tutor: Right Answer

Correct Answer.

if (x > y) {
      z = x + 1;
} else {
      z = y + 1;
}
z = z - 1;

For the relation

_par

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 indeed 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 in x.
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. (What happens if the values stored in x and y are equal?)

Back to Question.
Next Question.