Next / Previous / Contents / Shipman's homepage

6.4. The while loop rule

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:

# [ A ]
while C:
    # [ X ]
    ...

There are three parts to the proof rule for while loops.

  1. You must prove that the loop terminates.

  2. When the condition C is false, you must prove that doing nothing accomplishes the intended function A.

  3. When the condition C is true, you must prove that doing intended function X, followed by doing intended function A, accomplishes the overall intended function 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.

  1. 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
    LL[1:]
  2. 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)
    prefixconnector
    Lempty

    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.