Here is the general form of a
C: # [
The trace table work you use to verify
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
followed by doing
achieves the state changes in
, constructing a trace table can help
you reason about the correctness of the loop.
For example, we'll use the
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 . The second column
shows the state after executing intended function [2 body]
once. The third column shows the state after executing .
The correctness test is that the final values of the state
items must match the overall intended function for
|State item||||[2 body]|||
The correctness test is to compare the returned value,
pieceList[1:] separated by connector)”, with
the desired function value, “
(pieceList) separated by (connector)”: they