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

• `result` is the first element of `pieceList`, followed by the value of `prefix` (which is now a copy of `connector`), followed by the remaining elements of `pieceList` separated by `connector`.

• `prefix` is set to a copy of `connector`.

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.