Go backward to Two Queues in Series
Go up to Top
Go forward to Decomposition Theorem

The Decomposition Theorem

Complete system Pi of components Pi_i
- Low-level system Pi^l of components Pi_i^l
- Prove that Pi^l implements Pi by proving that Pi_i^l implements Pi_i
Proof:
- Prove and_i=1^l $M$ _i^l $=>$ and_i=1^l $M$ _i
- In general $M$ _i^l $=>$ $M$ _i does not hold!
Introduction of environments E_i
- $E$ _i and $M$ _i^l $=>$ $M$ _i
- $E$ _i much simpler than and_i $M$ _i^l
How to prove E_i?
- and_i=1^l $M$ _i^l $=>$ $E$ _i
- Again reasoning about whole low-level system!
Suffices to prove and_i=1^l M_i => E_i
- and_i=1^l $M$ _i simpler than and_i=1 $M$ _i
- Only high-level specification required.

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