According to the Assignment Rule, given the statement x = x + 1 and the
postcondition { x = 1 }, the proper precondition is
{ x = 1 }[ x <- x + 1 ] | = | { x + 1 = 1 } |
= | { x = 0 } |
However, the actual precondition { x = 0 or x = 1 } is weaker than the
required precondition { x = 0 }. The Rule of Consequence is only valid when
replacing a weaker precondition by a stronger one. We're stuck with the
(valid) triple
{ x = 0 } x = x + 1 { x = 1 }
with no way to get the necessary triple
{ x = 0 or x = 1 } x = x + 1 { x = 1 }
The predicate x = 1 cannot be the correct postcondition for the
statement x = x + 1 when the precondition is { x = 0 or x = 1 }.
This page last modified on 11 June 2003.