class interface KL_INPUT_STREAM_ROUTINES feature(s) from KL_IMPORTED_INPUT_STREAM_ROUTINES -- Access INPUT_STREAM_: KL_INPUT_STREAM_ROUTINES -- Routines that ought to be in class INPUT_STREAM ensure input_stream_routines_not_void: Result /= Void feature(s) from KL_IMPORTED_INPUT_STREAM_ROUTINES -- Type anchors INPUT_STREAM_TYPE: INPUT_STREAM feature(s) from KL_INPUT_STREAM_ROUTINES -- Initialization make_file_open_read (a_filename: STRING): like INPUT_STREAM_TYPE -- Create a new file object with a_filename as -- file name and try to open it in read-only mode. -- is_open_read (Result) is set to True -- if operation was successful. require a_filename_not_void: a_filename /= Void; a_filename_not_empty: a_filename.count > 0 ensure file_not_void: Result /= Void feature(s) from KL_INPUT_STREAM_ROUTINES -- Access name (a_stream: like INPUT_STREAM_TYPE): STRING -- Name of a_stream require a_stream_void: a_stream /= Void ensure name_not_void: Result /= Void feature(s) from KL_INPUT_STREAM_ROUTINES -- Status report is_open_read (a_stream: like INPUT_STREAM_TYPE): BOOLEAN -- Is a_stream open in read mode? require a_stream_void: a_stream /= Void is_closed (a_stream: like INPUT_STREAM_TYPE): BOOLEAN -- Is a_stream closed? require a_stream_void: a_stream /= Void end_of_input (a_stream: like INPUT_STREAM_TYPE): BOOLEAN -- Has an EOF been detected? require a_stream_void: a_stream /= Void; a_stream_is_open_read: is_open_read(a_stream) feature(s) from KL_INPUT_STREAM_ROUTINES -- Status setting close (a_stream: like INPUT_STREAM_TYPE) -- Close a_stream if it is closable, -- let it open otherwise. require a_stream_not_void: a_stream /= Void; not_closed: not is_closed(a_stream) feature(s) from KL_INPUT_STREAM_ROUTINES -- Input operations read_string (a_stream: like INPUT_STREAM_TYPE; nb_char: INTEGER): STRING -- Read at most nb_char characters read from a_stream. -- Return the characters that have actually been read. require a_stream_not_void: a_stream /= Void; a_stream_open_read: is_open_read(a_stream); nb_char_large_enough: nb_char >= 0 ensure string_not_void: Result /= Void; string_count_small_enough: Result.count <= nb_char read_stream (a_stream: like INPUT_STREAM_TYPE; a_buffer: STRING; pos, nb_char: INTEGER): INTEGER -- Fill a_buffer, starting at position pos with -- at most nb_char characters read from a_stream. -- Return the number of characters actually read. require a_stream_not_void: a_stream /= Void; a_stream_open_read: is_open_read(a_stream); a_buffer_not_void: a_buffer /= Void; valid_position: a_buffer.valid_index(pos); nb_char_large_enough: nb_char >= 0; nb_char_small_enough: nb_char <= a_buffer.count - pos + 1 ensure nb_char_read_large_enough: Result >= 0; nb_char_read_small_enough: Result <= nb_char end of KL_INPUT_STREAM_ROUTINES