Next / Previous / Contents / Shipman's homepage

8.4. Trace table for while loops

Here is the general form of a while construct:

    # [ A ]
    while C:
        # [ 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 X followed by doing C achieves the state changes in C, constructing a trace table can help you reason about the correctness of the loop.

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.