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( $E$ _a)_{+ <a, b>} and A( $M$ _a^l) $=>$ A( $M$ _a) and $E$ _a and $M$ _a^l $=>$ $M$ _a.
- Apply Propositions 4 and 5 to reduce first part to. A( $E$ _a) and A( $M$ _a^l) $=>$ A( $M$ _a).
- Apply Proposition 2 to remove quantifiers from A( $M$ _a^l) and Proposition 1 to remove As.
- Prove $E$ _a and Init_a^l and always [A_a^l]_{+ <a, ai, pca>} $=>$ Init_a and always [A_a^l]_a.
- Prove $E$ _a and Init_a^l and always [A_a^l]_{+ <a, ai, pca>} and WF_{+ <a, ai, pca>}(A_a^l) $=>$ WF_a(A_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.

Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine