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