Designing with `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:

# [] while`A`

: # [`C`

] ...`X`

There are three parts to the proof rule for `while`

loops.

You must prove that the loop terminates.

When the condition

is false, you must prove that doing nothing accomplishes the intended function`C`

.`A`

When the condition

is true, you must prove that doing intended function`C`

, followed by doing intended function`X`

, accomplishes the overall intended function`A`

.`A`

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 “`[:]`

” to
make a copy of the `pieceList`

argument. If we
used `pieceList`

instead of the copy inside the
`while`

loop, the overall intended function for
`joiner()`

would have to specify that the value
of `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[0] #-- 2.2 # [ prefix := connector # L := L minus its first element ] prefix = connector del L[0] #-- 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
forever.

The next step is to prove that the `while`

loop
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
function “`I`

”.

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:

`result`

`result+prefix+L[0]`

`prefix`

`connector`

`L`

`L[1:]`

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 variables are:`result`

`result+prefix+L[0]+connector+(elements of L[1:] separated by connector)`

`prefix`

`connector`

`L`

empty If

`L`

contained only one element initially, the value of`result`

in the above table becomes “`result+prefix+L[0]`

”, which is the desired final state in that case.Generally you may find yourself preferring definite iterations to indefinite (

`while`

) iterations, because they are easier to prove correct.