Here is the general form of a definite iteration.
# [A
] fore
inS
: # [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
when sequence A
is empty. This is a straightforward
application of reasoning.
S
For the second step, a twocolumn trace table can help you
reason that the code is correct. We can assume that sequence
is nonempty.
S
The first column shows the value of all the state items
affected after intended function
is executed for the first
element of B
.
S
The second column shows the value of all state items
affected after intended function
is executed for the remaining
elements of A
.
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.