class interface FILE

creation
   make_open_read (a_file: STRING)
      require
         not_void: a_file /= Void

   make_open_write (a_file: STRING)
      require
         not_void: a_file /= Void

feature(s) from FILE
   --  Status

   is_closed: BOOLEAN
      --  Is file closed?


   end_of_file: BOOLEAN
      --  End of file?

      require
         not_closed: not is_closed

   last_string: STRING
      --  Last string.

      require
         not_closed: not is_closed

feature(s) from FILE
   --  Actions

   read_line
      --  Read a line.

      require
         not_closed: not is_closed

   put_string (s: STRING)
      --  Put string.

      require
         not_void: s /= Void;
         not_closed: not is_closed

   close
      --  Close file.

      require
         not_closed: not is_closed


end of FILE