unless <forall : in ::
and not or >
- If is true at some point in program execution, then
in the next step
- either remains true,
- or becomes true.
- If holds at any point during execution of , then
- either never holds and continues to hold forever,
- or holds eventually and continues to hold at least
until holds.
- Program execution model:
- ( and not )[] ( or )[].
- []
<forall : :: ( andnot )[])>
or [<exists : :: []
and <forall : :: (
and not )[])>]