Logic Web Tutor: Wrong Answer

Incorrect Answer.

if (x > y) {
      z = y + 1;
} else {
      z = x + 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 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 + 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.
If "x > y" evaluates to false in the initial store, then the program P executes the else-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.

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

_par

z = min(x,y)

is valid.

Back to Question.
Next Question.