class interface UT_ARRAY_FORMATTER

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 UT_ARRAY_FORMATTER
   --  File handling

   put_integer_array (a_file: like OUTPUT_STREAM_TYPE; an_array: ARRAY[INTEGER]; start_pos, end_pos: INTEGER)
      --  Write code for an_array's items within bounds
      --  start_pos and end_pos to a_file.

      require
         an_array_not_void: an_array /= Void;
         start_pos_large_enough: start_pos >= an_array.lower;
         end_pos_small_enough: end_pos <= an_array.upper;
         valid_bounds: start_pos <= end_pos + 1;
         a_file_not_void: a_file /= Void;
         a_file_open_write: OUTPUT_STREAM_.is_open_write(a_file)


end of UT_ARRAY_FORMATTER