The proof rules for the while loop

For a construct of the form

    while C do
      A;

there are three proof rules you must deal with:

Termination: You must prove that the loop terminates.
False case: You must prove that if C is false, doing nothing does the overall I/F of the loop.
True case: You must prove that if C is true, doing the intended function for A, and then doing the intended function for the entire loop (after the state changes caused by A), does the overall intended function.

(This page needs a good example. If you get here and agree, send me e-mail and I'll put one up.)

Next: The proof rule for definite iteration
See also: Proof rules for Cleanroom control structures
Previous: The proof rule for alternation
Site map