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.''
#-- 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 ]
#-- 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 | ||
| "" | 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 ]
#-- 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 ]