Next / Previous / Contents / Shipman's homepage

6.3. The definite iteration rule

This rule is for performing some operation on every element of a Python iterable (sequence value), typically in a for statement with this general form.

# [ A ]
for e in S:
    # [ B ]

The proof rule is in two parts.

  1. If S is empty, does doing nothing have the same net effect as intended function A?

  2. If S is nonempty, does doing intended function B to the first element of S, followed by doing intended function A to the remaining elements of S, have the same net effect as intended function A on the entire sequence S?

Here's an example. This function implements the logic of Python's str.join() method, the equivalent of “connector.join(pieceList)”.

def joiner(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 = ''
    result = ''

    #-- 2
    # [ if pieceList is empty ->
    #     I
    #   else ->
    #     result  :=  result + prefix + (elements of (pieceList),
    #                 separated by (connector)
    #     prefix  :=  connector ]
    for piece in pieceList:
        #-- 2 body
        # [ result  :=  result + prefix + piece
        #   prefix  :=  connector ]
        result = result + prefix + piece
        prefix = connector

    #-- 3
    return result

Let's apply the two proof rules to this example.

Firstly, suppose pieceList is an empty sequence. In that case, the for loop never executes, so the return value is the value of result set in prime #1, the empty string. The overall intended function specifies that the connector is inserted only between elements; since there are no elements, the empty string is the correct result value.

In the case that pieceList is not empty, we apply the second proof rule. After applying the #2 body intended function, result is set to the first element of pieceList and prefix is set to the value of connector.

We then apply the intended function for the entirety of prime #2. After that, the states of our two variables are:

So in the case that pieceList is nonempty, the net changes are exactly what the intended function for the joiner function specifies.

Note that primes #1 and #3 have no intended functions. In these cases, the code itself serves as the intended function. This is acceptable only when the meaning is quite clear. For example, the intended function for prime #1 would be:

    #-- 1
    # [ prefix  :=  an empty string
    #   result  :=  an empty string ]
    prefix = ''
    result = ''

Assuming that the reader knows that '' is the empty string in Python, the comment becomes pretty much redundant.