Go backward to An Example
Go up to Top
Go forward to Invariant Proof
Proofs
- Invariant I
- and and and .
- Fixed point condition FP
- ( or ( and )) and
( or ( and )) and
( or ( and ))
- I and FP imply
- and .
- true FP (see later).
Program meets its specification!
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity2.tex,v 1.1 1996/04/15 14:38:10 schreine Exp schreine