Trace table verification example: the while loop

The verification of a while loop has three parts: proving termination; the negative case (when the loop condition is initially false); and the positive or closure case.

Termination

Arguing termination is pretty straightforward in this case. The loop always advances the position of <stdin>:

while  line != "":
    #-- 2 body --
    # [ if <stdin> is at end of file ->
    #     <stdout>  :=  <stdout> + line
    #     line  :=  ""
    #   else ->
    #     <stdout>  :=  <stdout> + line
    #     <stdin>   :=  <stdin> advanced past the current line
    #     line      :=  rest of the current line of <stdin> ]
    ...

Assuming that <stdin> is finite, the program will terminate.

The negative case

In the negative case, the loop test (line != "") is false, so nothing changes. Here's the overall intended function of the loop:

#-- 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      :=  "" ]

As for <stdin>, we know that it is at end of file by the precondition (either line is nonempty, or <stdin> is at EOF).

As for <stdout>, line is empty by assumption, and since <stdin> is empty, the expression ``<stdout> + line + (characters from <stdin> through end of file)'' simplifies to ``<stdout>''.

So, not changing <stdin> or <stdout> satisfies the overall intended function.

The true (closure) case: case 1, <stdin> is at EOF

Recall that the proof rule for ``while a do b'' is: ``Does doing b, followed by doing the entire loop, do the overall intended function?''

So, to build the trace table for the closure case, we start with the I/F for the loop body, followed by the I/F for the entire loop (starting from the new state):

#-- 2 body -- # [ if <stdin> is at end of file -> # <stdout> := <stdout> + line # line := "" # else -> # <stdout> := <stdout> + line # <stdin> := <stdin> advanced past the current line # line := rest of the current line of <stdin> ]
line	<stdin>	<stdout>
""	At EOF	@(<stdout>) + line
#-- 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>) + line

Compare this with the overall I/F of the loop (above). Because <stdin> is empty, the expression <stdout> + line + (characters from <stdin>) simplifies to @(<stdout>) + line, which is what we have for <stdout>. And <stdin> is at EOF, and line is "".

The true (closure) case: case 2, <stdin> is not at EOF

#-- 2 body --
# [ if <stdin> is at end of file ->
#     <stdout>  :=  <stdout> + line
#     line  :=  ""
#   else ->
#     <stdout>  :=  <stdout> + line
#     <stdin>   :=  <stdin> advanced past the current line
#     line      :=  rest of the current line of <stdin> ]

#-- 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      :=  "" ]

Compare those three values with the loop's overall I/F (shown above under #-- 2 --): line is "" as it should be; <stdin> is at EOF; and <stdout> has had line and the rest of <stdin> appended to it. QED.

Last updated: 2002/10/26 02:56:26
URL: http://www.nmt.edu/~shipman/soft/clean/trace-while.html