Go backward to Composing Assumption/Guarantee Specifications
Go up to Top
Go forward to Corollary
The Composition Theorem
- a/g specifications -|>+ .
- Composition implements -|>+ .
- Prove and ( -|>+ )
-|>+
- Composition Theorem
- If |= A()
and and A()
and |= A() and A()
A()
and |= and and
- then |= and ( -|>+ )
( -|>+ ).
- Hypotheses
- Proved similar to Decomposition Theorem.
- Each structured |= and and .
- Each form of specification of complete system.
- Reasoning about a/g specifications reduced to reasoning about
complete systems.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine