We'll look at a trace table verification of a program containing a sequence of two primes, of which the second one is a while loop.
The program is the classic ``Unix filter,'' which reads lines from the standard input stream and writes the same lines to the standard output stream. This example will be written in Python (refer to the Python help page for documentation describing how Python features work).
When I'm verifying code with trace tables, I generally use an ASCII-only format of my own invention. I bring up emacs in two-window mode, put the code in the top window, and develop the trace table in the bottom window. First I set up the case structure, using the character sequence "####" to set off the different cases. Then I use copy and paste to lift copies of the intended functions out of the code, following each intended function with lines describing the current values of each state item after that intended function operates. After reaching the final state, I paste in a copy of the overall intended function to compare it with, preceded by the comment #-- TARGET --.
Here are some examples of this style of trace table verification: