Go backward to The Decomposition Theorem
Go up to Top
Go forward to Verifying the Hypotheses
Decomposition Theorem
- The Basic Theorem
- If |= and A()
and |= A() and A()
A()
and |= and
- then |= and
and
- GCD Example
- always [ and ()]
- and
- is only implied by safety properties
- can only contain safety properties.
- are safety properties.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine