- $p$ is stable $<=>$ $p$
`unless`false.- Stable predicates remain true once it becomes true (but it may never become true).

- $q$ is invariant $<=>$ (initial condition $=>$ $q$)
*and*$q$ is stable.- Invariant is always true from the beginning.

**constant**$p$- $p$ and
*not*$p$ are stable.

- $p$ and

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

$$Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine $$