Next / Previous / Contents / Shipman's homepage

8.3. Trace table for definite iteration

Here is the general form of a definite iteration.

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

Recalling the proof rule in Section 6.3, “The definite iteration rule”, the proof proceeds in two steps. The first step is to determine whether doing nothing accomplishes intended function A when sequence S is empty. This is a straightforward application of reasoning.

For the second step, a two-column trace table can help you reason that the code is correct. We can assume that sequence S is nonempty.

  1. The first column shows the value of all the state items affected after intended function B is executed for the first element of S.

  2. The second column shows the value of all state items affected after intended function A is executed for the remaining elements of S.

For our example, we will use the joiner function defined in Section 6.3, “The definite iteration rule”. We'll need to build two trace tables: one for the case where the pieceList argument is an empty sequence, and one for the general case.

Here's the trace table for the empty case.

State item[1][2][3]
prefix '' '' ''
result '' '' ''
Result    ''

The function result is the empty string, which is the correct result when pieceList is empty.

Now for the general case. Here we can assume that pieceList has at least one element. The first column shows the state after prime [1]. The second column shows the state after executing the [2 body] intended function with piece set to the first element of pieceList. The third column shows the state after executing the [2] intended function on the rest of pieceList.

State item[1][2 body][2]
prefix '' connector connector
result '' pieceList[0] pieceList[0]+connector+(elements of pieceList[1:] separated by connector)

Our test for correctness is to compare “elements of (pieceList) separated by (connector)” against “pieceList[0]+connector+(elements of pieceList[1:] separated by connector)”: they agree.