Next
/
Previous
/ Shipman's Home Sweet Homepage
/ Site map

## 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

John W. Shipman,
`john@nmt.edu`
##### Last updated: 1996/03/09 22:39:11

URL: http://www.nmt.edu/~shipman/soft/clean/proofwhile.html