Given the required precondition { x = 0 or x = 1 } for the statement x =
x + 1, what's the proper postcondition?
Because we know the precondition but not the postcondition, this is a case where it makes more sense to work the Assignment Rule forward (from precondition to postcondition) rather than backward. The given precondition
{ x = 0 or x = 1 }
is still true when we add 1 to each side of the equality.
{ x + 1 = 1 or x + 1 = 2 }
This is just the predicate x = 1 or x = 2 with all occurrences of x
replaced by x + 1.
{ x = 1 or x = 2 }[ x <- x + 1 ]
The Assignment Rule now tells us that the proper postcondition is { x = 1 or
x = 2 } and the valid triple is
{ x = 0 or x = 1 } x = x + 1 { x = 1 or x = 2 }
This page last modified on 11 June 2003.