- Decomposition:
- Environment of each component are the other components.
- Assumption about environment must be stated.
- Assumption must be satisfied by other components.
- Decomposition theorem for system verification by proving property of high-level specification and properties of each low-level component.

- Composition:
- Environment is unknown.
- Component satisfies guarantee $M$ only under assumption $E$.
- Assumption/guarantuee property $M$ -|>+ $E$.
- Composition theorem for reasoning about assumption/guarantee specifications.

Wolfgang.Schreiner@risc.uni-linz.ac.at

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