Go backward to GCD Example (Contd)
Go up to Top
Go forward to Composing Assumption/Guarantee Specifications
The General Theorem
- Correctness of systems defined inductively:
- At stage , specfications are defined as copies of specfications
of state .
- Example: -bit multiplier implemented by combining four
bit multipliers.
- General decomposition theorem:
- If |= A()
and and A()
and |= A() and A()
A()
and |= and
and is a tuple of variables including all free variables of
- Then |= A()
and and A()
and A()
and |= and and
and
- Both decomposition theorems are equivalent.
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine