Go backward to Decomposition Theorem
Go up to Top
Go forward to Verifying the Hypotheses
Verifying the Hypotheses
- How to prove hypotheses of theorem?
- Simplify by Propositions 1 and 2.
- |= and (Init and always [A]) .
- Apply Proposition 5 to rewrite Init and always [A] in canonical form.
- First hypothesis (GCD example)
- A() and A() .
- Apply Proposition 1 to construct C() (strip fairness
condition).
- Since A implies and ,
A() implies .
- Second hypothesis (general).
- Apply Propositions and to eliminate .
- Use Proposition 2 to eliminate quantifiers.
- Use Proposition 1 to compute closures.
- Perform implementation proof with refinement mapping.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine