class interface KL_STANDARD_FILES 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_IMPORTED_OUTPUT_STREAM_ROUTINES -- Access OUTPUT_STREAM_: KL_OUTPUT_STREAM_ROUTINES -- Routines that ought to be in class OUTPUT_STREAM ensure output_stream_routines_not_void: Result /= Void feature(s) from KL_IMPORTED_OUTPUT_STREAM_ROUTINES -- Type anchors OUTPUT_STREAM_TYPE: OUTPUT_STREAM feature(s) from KL_STANDARD_FILES -- Access input: STD_INPUT -- Standard input file ensure file_not_void: Result /= Void; file_open_read: INPUT_STREAM_.is_open_read(Result) output: STD_OUTPUT -- Standard output file ensure file_not_void: Result /= Void; file_open_write: OUTPUT_STREAM_.is_open_write(Result) error: STD_ERROR -- Standard error file ensure file_not_void: Result /= Void; file_open_write: OUTPUT_STREAM_.is_open_write(Result) end of KL_STANDARD_FILES