Logic Web Tutor: Wrong Answer

Incorrect Answer.

For the relation

_par

x = 1; x = 2;

x = 1

x = 2

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 "x = 1 x = 2". Observe that this formula is inconsistent, it cannot be made true. Thus, the relationship above can only hold if the program never terminates! But this program always terminates and, after termination, the value stored in x equals 2. Thus, we do not have partial correctness for the Hoare triple above.

Back to Question.
Next Question.