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 $N+1$ , specfications are defined as $k$ copies of specfications of state $N$ .
- Example: $2$ ^N+1-bit multiplier implemented by combining four $2$ ^N bit multipliers.
General decomposition theorem:
- If |= A( $E$ ) and and_j=1ⁿ A( $M$ _j) $=>$ $E$ _i
  and |= A( $E$ _i)_+v and A( $M$ _i^l) $=>$ A( $M$ _i)
  and |= $E$ _i and $M$ _i^l $=>$ $M$ _i
  and $v$ is a tuple of variables including all free variables of $M$ _i
- Then |= A( $E$ )_+v and and_j=1ⁿ A( $M$ _j^l) $=>$ and_j=1ⁿ A( $M$ _j)
  and |= $E$ and and_j=1ⁿ $M$ _j^l $=>$ and_j=1ⁿ $M$ _j
Both decomposition theorems are equivalent.

Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine