If you know that A and B
are true, then you know, by the and
truth
table, that both A
and B
are true too.
and
elimination exploits this property by allowing you to conclude either
A
is true or B
is true if you know that A and B
is true.
For a co statement, you know that the precondition
{ P1 and P2 and ... and Pn }
is true at the time statement Si
begins execution. You can use
and
elimination to get rid of all the predicates S
j,
j != i (as a tactical matter, however, you may want to keep a few of
the other predicates in S
i's precondition, particularly if you
anticipate the need to weaken S
i's precondition to avoid
interference).
This page last modified on 11 June 2003.