The predicate { x1 = 0 } is true because it's the precondition
of the statement
x1 = x1 + 1
that we're testing for interference. If the statement's being executed, its precondition must be true (in a correctly annotated computation).
This page last modified on 11 June 2003.