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