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

Trace table verification example: the main

Each column in the table below tracks one state item. There are only three state items: the variable line; <stdin>, the standard input stream; and <stdout>, the standard output stream.

Because prime 1 tests whether <stdin> is empty or not, and because prime 2 also tests this, there are three cases: (1) <stdin> is empty; (2) <stdin> has exactly one line; and (3) <stdin> has more than one line.

The notation @(x) refers to whatever value state item x had before the execution of the prime. EOF means ``end of file.''


Case 1: <stdin> is empty

#-- 1 --
# [ if <stdin> is at end of file ->
#     line  :=  an empty string
#   else ->
#     line     :=  <stdin> through the end of the next line
#     <stdin>  :=  <stdin> advanced to next line or EOF,
#                  whichever comes first ]
line <stdin> <stdout>
"" at EOF @(<stdout>)
#-- 2 --
# [ if (line is "" and <stdin> is at EOF) or
#   (line is nonempty) ->
#     <stdout>  :=  <stdout> + line + (characters from <stdin>
#                   through end of file)
#     <stdin>   :=  <stdin> advanced to end of file
#     line      :=  "" ]
"" at EOF @(<stdout>)

Compare the final state above with the overall intended function:

#   [ <stdout>  :=  <stdout> + (contents of <stdin>)
#     <stdin>   :=  <stdin> advanced to end of file ]

Case 2: <stdin> contains exactly one line

#-- 1 --
# [ if <stdin> is at end of file ->
#     line  :=  an empty string
#   else ->
#     line     :=  <stdin> through the end of the next line
#     <stdin>  :=  <stdin> advanced to next line or EOF,
#                  whichever comes first ]
line <stdin> <stdout>
first line of <stdin> at EOF @(<stdout>)
#-- 1 --
# [ if <stdin> is at end of file ->
#     line  :=  an empty string
#   else ->
#     line     :=  <stdin> through the end of the next line
#     <stdin>  :=  <stdin> advanced to next line or EOF,
#                  whichever comes first ]
"" at EOF @(<stdout>) + (first line of <stdin>)
#-- 2 --
# [ if (line is "" and  is at EOF) or
#   (line is nonempty) ->
#       :=   + line + (characters from 
#                   through end of file)
#        :=   advanced to end of file
#     line      :=  "" ]
"" at EOF @(<stdout>) + (first line of <stdin>)

Compare this state to the overall intended function:

#   [ <stdout>  :=  <stdout> + (contents of <stdin>)
#     <stdin>   :=  <stdin> advanced to end of file ]

Case 3: <stdin> contains more than one line

#-- 1 --
# [ if <stdin> is at end of file ->
#     line  :=  an empty string
#   else ->
#     line     :=  <stdin> through the end of the next line
#     <stdin>  :=  <stdin> advanced to next line or EOF,
#                  whichever comes first ]
line <stdin> <stdout>
first line from <stdin> @(<stdin>) advanced to start of second line @(<stdout>)
#-- 2 --
# [ if (line is "" and <stdin> is at EOF) or
#   (line is nonempty) ->
#     <stdout>  :=  <stdout> + line + (characters from <stdin>
#                   through end of file)
#     <stdin>   :=  <stdin> advanced to end of file
#     line      :=  "" ]
"" at EOF @(<stdout>) + (first line from <stdin>) + (second through last lines from <stdin>)

Compare this with the overall intended function:

#   [ <stdout>  :=  <stdout> + (contents of <stdin>)
#     <stdin>   :=  <stdin> advanced to end of file ]

Next: Trace table verification example: the while loop
See also: Using trace tables for verification
Previous: Example of trace table verification: filter.py
Site map
John W. Shipman, john@nmt.edu
Last updated: 2002/10/26 02:26:01
URL: http://www.nmt.edu/~shipman/soft/clean/trace-main.html