class interface KL_STRING_BUFFER_ROUTINES
feature(s) from KL_IMPORTED_STRING_BUFFER_ROUTINES
-- Access
STRING_BUFFER_: KL_STRING_BUFFER_ROUTINES
-- Routines that ought to be in class STRING_BUFFER
ensure
string_buffer_routines_not_void: Result /= Void
feature(s) from KL_IMPORTED_STRING_BUFFER_ROUTINES
-- Type anchors
STRING_BUFFER_TYPE: STRING
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_STRING_BUFFER_ROUTINES
-- Initialization
make (n: INTEGER): like STRING_BUFFER_TYPE
-- Create a new string buffer being able
-- to contain n characters.
require
non_negative_n: n >= 0
ensure
string_buffer_not_void: Result /= Void;
count_set: Result.count = n
make_from_string (a_string: STRING): like STRING_BUFFER_TYPE
-- Create a new string buffer with characters from a_string.
require
a_string_not_void: a_string /= Void
ensure
string_buffer_not_void: Result /= Void;
count_set: Result.count = a_string.count;
charaters_set: equal(substring(Result,lower,a_string.count + lower - 1),a_string)
feature(s) from KL_STRING_BUFFER_ROUTINES
-- Conversion
to_string_buffer (a_string: STRING): like STRING_BUFFER_TYPE
-- String buffer filled with characters from a_string.
-- The string buffer and a_string may share internal
-- data. Use make_from_string if this is a concern.
require
a_string_not_void: a_string /= Void
ensure
string_buffer_not_void: Result /= Void;
count_set: Result.count >= a_string.count;
charaters_set: equal(substring(Result,lower,a_string.count + lower - 1),a_string)
feature(s) from KL_STRING_BUFFER_ROUTINES
-- Access
substring (a_buffer: like STRING_BUFFER_TYPE; s, e: INTEGER): STRING
-- New string made up of characters held in
-- a_buffer between indexes s and e
require
a_buffer_not_void: a_buffer /= Void;
s_large_enough: s >= lower;
e_small_enough: e <= upper(a_buffer);
valid_interval: s <= e + 1
ensure
substring_not_void: Result /= Void;
count_set: Result.count = e - s + 1
feature(s) from KL_STRING_BUFFER_ROUTINES
-- Measurement
lower: INTEGER
-- Lower index
upper (a_buffer: like STRING_BUFFER_TYPE): INTEGER
-- Upper index
require
a_buffer_not_void: a_buffer /= Void
ensure
definition: a_buffer.count = Result - lower + 1
feature(s) from KL_STRING_BUFFER_ROUTINES
-- Element change
append_substring_to_string (a_buffer: like STRING_BUFFER_TYPE; s, e: INTEGER; a_string: STRING)
-- Append string made up of characters held in a_buffer
-- between indexes s and e to a_string.
require
a_buffer_not_void: a_buffer /= Void;
a_string_not_void: a_string /= Void;
not_same: to_string_buffer(a_string) /= a_buffer;
s_large_enough: s >= lower;
e_small_enough: e <= upper(a_buffer);
valid_interval: s <= e + 1
ensure
count_set: a_string.count = old a_string.count + e - s + 1;
characters_set: s <= e implies equal(a_string.substring(old a_string.count + 1,a_string.count),substring(a_buffer,s,e))
copy_from_string (a_buffer: like STRING_BUFFER_TYPE; pos: INTEGER; a_string: STRING)
-- Copy characters of a_string to a_buffer
-- starting at position pos.
require
a_buffer_not_void: a_buffer /= Void;
a_string_not_void: a_string /= Void;
not_same: to_string_buffer(a_string) /= a_buffer;
pos_large_enough: pos >= lower;
enough_space: pos + a_string.count - 1 <= upper(a_buffer)
ensure
charaters_set: equal(substring(a_buffer,pos,a_string.count + pos - 1),a_string)
copy_from_stream (a_buffer: like STRING_BUFFER_TYPE; pos: INTEGER; a_stream: like INPUT_STREAM_TYPE; nb_char: INTEGER): INTEGER
-- Fill a_buffer, starting at position pos with
-- at most nb_char characters read from a_stream.
-- Return the number of characters actually read.
require
a_buffer_not_void: a_buffer /= Void;
pos_large_enough: pos >= lower;
a_stream_not_void: a_stream /= Void;
a_stream_open_read: INPUT_STREAM_.is_open_read(a_stream);
nb_char_large_enough: nb_char >= 0;
enough_space: pos + nb_char - 1 <= upper(a_buffer)
ensure
nb_char_read_large_enough: Result >= 0;
nb_char_read_small_enough: Result <= nb_char
move_left (a_buffer: like STRING_BUFFER_TYPE; old_pos, new_pos: INTEGER; nb: INTEGER)
-- Copy nb characters from old_pos to
-- new_pos in a_buffer.
require
a_buffer_not_void: a_buffer /= Void;
nb_positive: nb >= 0;
old_pos_large_enough: old_pos >= lower;
enough_characters: old_pos + nb - 1 <= upper(a_buffer);
new_pos_large_enough: new_pos >= lower;
enough_space: new_pos + nb - 1 <= upper(a_buffer);
move_left: old_pos > new_pos
move_right (a_buffer: like STRING_BUFFER_TYPE; old_pos, new_pos: INTEGER; nb: INTEGER)
-- Copy nb characters from old_pos to
-- new_pos in a_buffer.
require
a_buffer_not_void: a_buffer /= Void;
nb_positive: nb >= 0;
old_pos_large_enough: old_pos >= lower;
enough_characters: old_pos + nb - 1 <= upper(a_buffer);
new_pos_large_enough: new_pos >= lower;
enough_space: new_pos + nb - 1 <= upper(a_buffer);
move_right: old_pos < new_pos
feature(s) from KL_STRING_BUFFER_ROUTINES
-- Resizing
resize (a_buffer: like STRING_BUFFER_TYPE; n: INTEGER): like STRING_BUFFER_TYPE
-- Resize a_buffer so that it contains n characters.
-- Do not lose any previously entered characters.
-- Note: the returned string buffer might be a_buffer or
-- a newly created string buffer where characters from
-- a_buffer have been copied to.
require
a_buffer_not_void: a_buffer /= Void;
n_large_enough: n >= a_buffer.count
ensure
string_buffer_not_void: Result /= Void;
count_set: Result.count = n
end of KL_STRING_BUFFER_ROUTINES