Go backward to Examples
Go up to Top
Go forward to Summary
Properties
- invariant count = number of statement executions in
underlying program.
- invariant claim (count 10)
- claim detects (number of statement executions in the
underlying program exceeds 10).
- detects ( ) and (
)
- holds within a finite time of holding, and if holds, then so
does .
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: unity3.tex,v 1.1 1996/04/19 12:29:22 schreine Exp schreine