- $p$ is stable in $F$ [] $G$ $<=>$

($p$ is stable in $F$*and*$p$ is stable in $G$) -
$p$ `unless`$q$ in $F$$p$ is stable in $G$ $p$ `unless`$q$ in $F$ [] $G$ -
$p$ is invariant $q$ in $F$ $p$ is stable in $G$ $p$ is invariant $q$ in $F$ [] $G$ -
$p$ `ensures`$q$ in $F$$p$ is stable in $G$ $p$ `ensures`$q$ in $F$ [] $G$ - Locality:
- $p$ is a local predicate of $F$, if it only mentions variables that can be modified by $F$ alone.
- If $p$ is a local predicate of $F$, then the following properties hold
in $F$ [] $G$, for any $G$: $p$
`unless`$q$, $p$`ensures`$q$, $p$ is invariant.

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

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