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