Next / Previous / Shipman's Home Sweet Homepage / Site map

Using trace tables for verification

If you keep your modules small, many of them can be verified by inspection. In more complex cases, though, it is necessary to use trace tables to verify the code.

A trace table is just a list of the values of all the state-items (the left sides of the intended function lines) at each step of the procedure.

For example, suppose a procedure affects variables a, b, and x, and the procedure is a sequence of two primes. The trace table can be conceptualized as a 3x2 matrix, with rows for each variable. The first column shows the value of each variable after the first prime, and the second column shows the value of each variable after the second prime.

If the expressions given in the overall I/F for the procedure match the values of the corresponding state-items in the last column of the trace table, then the procedure is likely to be correct.

If a given state item s is not local to the procedure, I use the notation @(s) to signify the value it had on entry. For example, if the first I/F says

    <stdout>  :=  <stdout> + "Arr.\n"
then the trace table item for <stdout> after that prime would be ``@(<stdout>) + "Arr.\n"''.

If there are conditions in the overall intended functions, it is necessary to crank through a trace table for every possible condition.

If there are multiple conditions at a given point in the code, it is necessary to crank a trace table for the Cartesian product of all the possible conditions. This is another reason to keep modules small, one level of branch construct or two at the outside.

Proceed on to see an example of trace table verification.


Next: Using the Cleanroom methodology with objects
See also: Overview of the Cleanroom software methodology
Previous: Proof rules for Cleanroom control structures
Site map
John W. Shipman, john@nmt.edu
Last updated: 2002/10/26 01:15:24
URL: http://www.nmt.edu/~shipman/soft/clean/trace.html