Source listing for filter.py

#!/usr/local/bin/python
#--
# Classic filter example for Cleanroom class: just copies
# stdin to stdout.
#--
# 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 ]
import sys

line  =  sys.stdin.readline()

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

    #-- 2.1 --
    # [ <stdout>  :=  <stdout> + line ]
    sys.stdout.write ( line )

    #-- 2.2 --
    # [ if <stdin> is at end of file ->
    #     line  :=  empty string
    #   else ->
    #     line     :=  characters from current line of <stdin>
    #     <stdin>  :=  <stdin> advanced past the current line ]
    line  =  sys.stdin.readline()