Permissible Cleanroom control structures

Only four branching constructs are allowed in Cleanroom code:

1. Sequence: do A, then do B.
2. Alternation: if condition C is true, then do A, else do B. Either A or B may be ``do nothing.''
3. While loop: while condition C is true, do A.
4. 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 verification).
• Each of the smaller units symbolized by A and B above is called a primary program refinement, or prime for short.
• There must be an intended function defining the semantics of each prime.
• If a prime calls another procedure, the semantics of that procedure are defined by that procedure's intended function.

Last updated: 1996/03/09 22:37:10
URL: http://www.nmt.edu/~shipman/soft/clean/con-structs.html