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