Go backward to Composed Specifications
Go up to Top
Go forward to Hierarchical Development

Decomposing Complete Systems

Complete System.
- Self-contained system that may be observed but does not interact with observer.
Example: GCD
- Program GCD
  var $a$ initially 233344, $B$ initially 233577899;
  cobegin
     loop < if $a>b$ then $a$ := $a-b$ > endloop
        ||
     loop < if $b>a$ then $b$ := $b-a$ > endloop
  coend
Correctness property:
- $a$ and $b$ eventually become and remain equal to gcd of initial values.
- Program $M$ _gcd, correctness property $P$ _gcd
- Verification $M$ _gcd $=>$ $P$ _gcd

Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine