The relation between liveness and saftey properties is based on their
definitions as forall
and foreach
predicates. The foreach
predicate
foreach x : P(x) : Q(x)
is identical to the forsome
predicate
not (forsome x : P(x) : not Q(x))
In the other direction, the forsome
predicate
forsome x : P(x) : Q(x)
is identical to the foreach
predicate
not (forall x : P(x) : not Q(x))
The slippery bit in these identities is the double negative.
This page last modified on 25 June 2003.