Go backward to Verifying the Hypotheses
Go up to Top
Go forward to The General Theorem
GCD Example (Contd)
- Second and third hypotheses (GCD).
- Prove A() and A() A()
and and .
- Apply Propositions 4 and 5 to reduce first part to.
A() and A() A().
- Apply Proposition 2 to remove quantifiers from
A() and Proposition 1 to remove As.
- Prove and Init and always [A] Init and
always [A].
- Prove and Init and always [A] and WF(A)
WF(A)
- Apply Proposition 6 to rewrite lhs of both formulas to canonical form
and apply TLA implementation proof.
- Summary
- Applying propositions in standard sequence, use Decomposition Theorem to
reduce decompostional reasoning to ordinary TLA reasoning.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine