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