Proof rules for Cleanroom control structures

In order to verify that a procedure's components correctly implement that procedure's intended function, four sets of proof rules are used, one for each of the four permissible branch constructs.

• The proof rule for sequences
• The proof rule for alternation
• The proof rules for the while loop
• The proof rule for definite iteration

Last updated: 1996/03/09 22:37:28
URL: http://www.nmt.edu/~shipman/soft/clean/proofrules.html