"Oh really?" you may be saying to yourself, "doesn't the
consumer statement empty = true interfere with the producer predicate
{ empty }?" Let's see.
The consumer statement empty = true has some precondition, call it
{ P }. We need to determine if the triple
{ P and empty } emtpy = true { empty }
is valid. Working backward in the Assignment Rule, the expected precondition is
{ empty }[ empty <- true ]
or just true. true is the weakest possible predicate, and can be
replaced as a precondition by any stronger predicate; in particular, it can be
replaced by the predicate { P and empty }. The Consequence Rule lets us
conclude that the triple
{ P and empty } emtpy = true { empty }
is valid and there's no interference. A somewhat quicker way to reach the same
conclusion is to note that the statement assigns true to empty, which cannot
falsify the predicate { empty }.
A similar argument and conclusion can be made about the producer statement
empty = false and its ability to intefere with the consumer predicate
{ not empty }.
This page last modified on 11 June 2003.