Go backward to Decomposing a Complete Specification
Go up to Top
Go forward to Queue Component
Component Specification
- Specification of
- exists : Init and always [A
or (<, >' = <, >)]
and .
- exists : Init and always [A]
and .
- GCD: Specification
- Init = 233344
- and
and
- A Init
and always [A] and WF(A)
- GCD: Specification
- exists , : Init
and always [A] and WF(A)
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec2.tex,v 1.1 1996/05/24 15:01:43 schreine Exp schreine