Incorrect Answer.
Assume that the program " x = y; y = x;" runs in any store in which
the values stored in x and y are 5 and 3, respectively. If the program
run terminates (in our tiny core language, this will be the case), then
both x and y have 3 as their stored value:
- Since y equals 5 initially,
the first assignment "x = y;" stores 3 in location x.
- Then, the second
assignment "y = x;" stores the current value of x,
which is 3, into y.
- But then the formula
x = 3 
y =5
is false.
- Thus, the relation
parx = 5 y = 3 x = y; y = x; x = 3 y = 5
does not hold.
Back to Question.
Next Question.