Incorrect Answer.
We consider the program P
y = x - y - 1;
x = x + 1;
y = 2*x + y;
This answer claims that the precondition
y = y + 3
guarantees that, after the program has run and terminated, x = y.
In order to determine whether this is true or not, we can compute
the weakest precondition for the program
which quarantees the postcondition x = y.
To obtain that, we push x = y upwards through the assignments in the program
and simplify if need be:
y = 2x Weakest Precondition
(x + 1) = 2(x + 1) + (x - y - 1) Implied
y = x - y - 1;
(x + 1) = 2(x + 1) + y Assignment
x = x + 1;
x = 2x + y Assignment
y = 2x + y;
x = y Assignment
- The instance of the proof rule "Implied" above is not only legitimate.
We merely simplified the equation x + 1 = 2(x + 1) + x - y - 1 to the
equivalent one, y = 2x. Thus, the latter is the weakest precondition that
guarantees the given postcondition x = y .
- Since y = 2x is the weakest precondition that
guarantees x = y
for the given program, we can only have
par
y = y + 3 P
x = y
if, and only if, y = y + 3 implies y = 2x. But this is not the case in
general.
(For which combinations of x and y values is this an
implication nonetheless?)
Back to Question.
Next Question.