- $p$
`unless`$q$ in $F$ [] $G$ $<=>$

($p$`unless`$q$ in $F$*and*$p$`unless`$q$ in $G$)- If $p$ is true and $q$ is not, $p$ remains true or $q$ becomes true.

- $p$
`ensures`$q$ in $F$ [] $G$ $<=>$

[$p$`ensures`$q$ in $F$*and*$p$`unless`$q$ in $G$]*or*

[$p$`ensures`$q$ in $G$*and*$p$`unless`$q$ in $F$]- If $p$ is true, $p$ remains true as long as $q$ is false and eventually $q$ becomes true.

- (
`FP`of $F$ [] $G$) $<=>$

(`FP`of $F$)*and*(`FP`of $G$)- State does not change any more.

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine $$