/ Shipman's Home Sweet Homepage
/ Site map
Permissible Cleanroom control structures
Only four branching constructs are allowed in Cleanroom code:
- Sequence: do A, then do B.
- Alternation: if condition C is true, then do A,
else do B. Either A or B may be ``do nothing.''
- While loop: while condition C is true, do A.
- Definite iteration: do A to every component of some
composite or container.
- Each branch construct has an associated proof rule that is
discussed later (see
- Each of the smaller units symbolized by A and B above
is called a primary program refinement, or prime for
- There must be an intended function defining the semantics of
- If a prime calls another procedure, the semantics of that
procedure are defined by that procedure's intended function.
Next: Verifying a Cleanroom procedure
See also: Overview of the Cleanroom software methodology
Previous: Writing Cleanroom intended functions
John W. Shipman,
Last updated: 1996/03/09 22:37:10