indexing
description: "Array formatters"
library: "Gobo Eiffel Utility Library"
author: "Eric Bezault <ericb@gobo.demon.co.uk>"
copyright: "Copyright (c) 1998, Eric Bezault"
class interface
UT_ARRAY_FORMATTER
feature -- Access
output_stream_: KL_OUTPUT_STREAM_ROUTINES
-- Routines that ought to be in class OUTPUT_STREAM
-- (from KL_IMPORTED_OUTPUT_STREAM_ROUTINES)
ensure -- from KL_IMPORTED_OUTPUT_STREAM_ROUTINES
output_stream_routines_not_void: Result /= void
feature -- 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)
feature -- Type anchors
output_stream_type: IO_MEDIUM
-- (from KL_IMPORTED_OUTPUT_STREAM_ROUTINES)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
end -- class UT_ARRAY_FORMATTER