Go backward to Reasoning about Composed Systems
Go up to Top
Go forward to Reasoning about Composed Systems

Reasoning about Composed Systems

Example:
- $M$ _c⁰ asserts $c$ always equals 0.
- $M$ _d⁰ asserts $d$ always equals 0.
- pi_c guarantees $M$ _c⁰ assuming $M$ _d⁰ and pi_d guarantees $M$ _d⁰ assuming $M$ _c⁰.
- Composition leaves $c$ and $d$ unchanged, so it implements $M$ _c⁰ and $M$ _d⁰.
Example:
- $M$ _c¹ asserts $c$ eventually equals 1.
- $M$ _d¹ asserts $d$ eventually equals 1.
- pi_c guarantees $M$ _c⁰ assuming $M$ _d⁰ and pi_d guarantees $M$ _d⁰ assuming $M$ _c⁰.
- Composition leaves $c$ and $d$ unchanged, so it does not implement $M$ _c¹ and $M$ _d¹!

Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine