Go backward to Decomposing a Complete Specification
Go up to Top
Go forward to Queue Component

Component Specification

Specification of M
- exists $x$ : Init and always [A_m or (< $m$ , $x$ >' = < $m$ , $x$ >)] _{<e, m, x>} and $L$ .
- exists $x$ : Init and always [A_m] _{<m, x>} and $L$ .
GCD: Specification M_a
- Init_a $<=>$ $a$ = 233344
- $M$ _a $<=>$ $(a > b)$ and $(a' = a-b)$ and $(b' = b)$
- A_a $<=>$ Init_a and always [A_a]_a and WF_a(A_a)
GCD: Specification M_a^l
- $M$ _a^l $<=>$ exists $ai$ , $pca$ : Init_a^l and always [A_a^l]_{<a, ai, pca>} and WF_{<a, ai, pca>}(A_a^l)

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