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
- Low-level system Pi of components Pi
- Prove that Pi implements Pi by proving that
Pi implements Pi
- Prove and and
- In general does not hold!
- Introduction of environments
- much simpler than and
- How to prove ?
- Again reasoning about whole low-level system!
- Suffices to prove and
- and simpler than and
- Only high-level specification required.
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine