Here is the general form of a while
construct:
# [A
] whileC
: # [X
] ...
The trace table work you use to verify while
loops is quite similar to the method described in Section 8.3, “Trace table for definite iteration”. Reviewing the proof rule
discussed in Section 6.4, “The while
loop rule”, recall there are
three parts. There is no need for trace tables in proving
termination, or in proving the trivial case where the
condition is initially false.
For the third part, where you prove that doing the loop body's
intended function
followed by doing X
achieves the state changes in C
, constructing a trace table can help
you reason about the correctness of the loop.
C
For example, we'll use the joiner2
function
defined in Section 6.4, “The while
loop rule”.
In this trace table, there are three columns. The first
column shows the state after prime [1]. The second column
shows the state after executing intended function [2 body]
once. The third column shows the state after executing [2].
The correctness test is that the final values of the state
items must match the overall intended function for joiner2
.
State item  [1]  [2 body]  [2] 

prefix

''

connector

connector

result

''

pieceList[0]

pieceList[0]+connector+(elements of
pieceList[1:] separated by connector)

L

copy of pieceList

copy of pieceList[1:]

empty

The correctness test is to compare the returned value,
“pieceList[0]+connector+(elements of
pieceList[1:] separated by connector)
”, with
the desired function value, “elements of
(pieceList) separated by (connector)
”: they
match.