while loops is more involved
than the other three proof rules. Such loops are treacherous
because they can become infinite loops. Hardly ever is that
the desired functioning of your program.
The general form:
C: # [
There are three parts to the proof rule for
You must prove that the loop terminates.
When the condition
false, you must prove that doing nothing accomplishes the
When the condition
C is true,
you must prove that doing intended function
X, followed by doing intended function
A, accomplishes the overall
Here is an example that implements the same function as the
joiner function in Section 6.3, “The definite iteration rule”. Note that we use the
Python slice operator “
make a copy of the
pieceList argument. If we
pieceList instead of the copy inside the
while loop, the overall intended function for
joiner() would have to specify that the value
pieceList becomes empty.
def joiner2(connector, pieceList): '''Join the pieces of pieceList with the connector. [ (connector is a string) and (pieceList is a list of strings) -> return a string containing the elements of (pieceList) separate by (connector) ] ''' #-- 1 # [ prefix := an empty string # result := an empty string # L := a copy of pieceList ] prefix = '' result = '' L = pieceList[:] #-- 2 # [ if L is empty -> # I # else -> # result := result + prefix + (elements of L separated # by copies of connector) # prefix := connector # L := empty ] while len(L) > 0: #-- 2 body # [ result := result + prefix + (first element of L) # prefix := connector # L := L minus its first element ] #-- 2.1 # [ result := result + prefix + (first element of L) ] result += prefix + L #-- 2.2 # [ prefix := connector # L := L minus its first element ] prefix = connector del L #-- 3 return result
To prove that the
while loop implements the
correct semantics, we first prove that the loop terminates.
Because each pass through the loop deletes one element of
L, and because the loop runs until
L is empty, it is clear that the loop cannot run
The next step is to prove that the
does the right thing when
L is empty. This
also is quite clear: if
L is empty, then
len(L) is not greater than zero, so the loop never
executes. This satisfies the special identity intended
The final step is to prove the true case, when
L is not empty.
First we execute the intended function for the body of the loop. This accomplishes the following state changes:
Then we execute the intended function for the entire
while loop. Assuming there is at least one more
element remaining in L, the new states of the three
L contained only one element initially,
the value of
result in the above table
which is the desired final state in that case.
Generally you may find yourself preferring definite
iterations to indefinite (
iterations, because they are easier to prove correct.