class interface STRING
--
-- Resizable character STRINGs indexed from 1 to count.
--
creation
make (needed_capacity: INTEGER)
-- Initialize the string to have at least needed_capacity
-- characters of storage.
require
non_negative_size: needed_capacity >= 0
ensure
needed_capacity <= capacity;
empty_string: count = 0
copy (other: like Current)
-- Copy other onto Current.
require
standard_same_dynamic_type(other)
ensure
count = other.count;
is_equal(other)
make_empty
-- Create an empty string.
make_filled (c: CHARACTER; n: INTEGER)
-- Initialize string with n copies of c.
require
valid_count: n >= 0
ensure
count_set: count = n;
filled: occurrences(c) = count
from_external (p: POINTER)
-- Internal storage is set using p (may be dangerous because
-- the external C string p is not duplicated). Assume p has a
-- null character at the end in order to compute the Eiffel
-- count. This extra null character is not part of the Eiffel
-- STRING. Also consider from_external_copy to choose the most
-- appropriate.
require
p.is_not_null
ensure
capacity = count + 1;
p = to_external
from_external_copy (p: POINTER)
-- Internal storage is set using a copy of p. Assume p has a
-- null character at the end in order to compute the Eiffel
-- count. This extra null character is not part of the Eiffel
-- STRING. Also consider from_external to choose the most
-- appropriate.
require
p.is_not_null
make_from_string (model: STRING)
-- (Here for ELKS compatibility.)
-- Initialize from the characters of model.
-- Useful in proper descendants of STRING.
require
model /= Void
ensure
count = model.count
blank (nr_blanks: INTEGER)
feature(s) from HASHABLE
hash_code: INTEGER
-- The hash-code value of Current.
ensure
good_hash_value: Result >= 0
feature(s) from COMPARABLE
is_equal (other: like Current): BOOLEAN
-- Do both strings have the same character sequence?
-- (Redefined from GENERAL)
require
other /= Void
ensure
trichotomy: Result = (not (Current < other) and not (other < Current));
same_dynamic_type(other) implies Result = other.is_equal(Current)
infix "<" (other: like Current): BOOLEAN
-- Is Current less than other?
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
-- Is Current less than or equal other?
require
other_exists: other /= Void
ensure
definition: Result = (Current < other or is_equal(other))
infix ">" (other: like Current): BOOLEAN
-- Is Current strictly greater than other?
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
-- Is Current greater than or equal than other?
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
in_range (lower, upper: like Current): BOOLEAN
-- Return true if Current is in range [lower..upper]
ensure
Result = (Current >= lower and Current <= upper)
compare (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
min (other: like Current): like Current
-- Minimum of Current and other.
require
other /= Void
ensure
Result <= Current and then Result <= other;
compare(Result) = 0 or else other.compare(Result) = 0
max (other: like Current): like Current
-- Maximum of Current and other.
require
other /= Void
ensure
Result >= Current and then Result >= other;
compare(Result) = 0 or else other.compare(Result) = 0
feature(s) from STRING
count: INTEGER
-- String length which is also the maximum valid index.
capacity: INTEGER
-- Capacity of the storage area.
lower: INTEGER
-- Minimum index; actually, this is always 1 (this feature is
-- here to mimic the one of the COLLECTIONs hierarchy).
upper: INTEGER
-- Maximum index; actually the same value as count (this
-- feature is here to mimic the one of the COLLECTION hierarchy).
ensure
Result = count
feature(s) from STRING
-- Creation / Modification:
make (needed_capacity: INTEGER)
-- Initialize the string to have at least needed_capacity
-- characters of storage.
require
non_negative_size: needed_capacity >= 0
ensure
needed_capacity <= capacity;
empty_string: count = 0
make_empty
-- Create an empty string.
make_filled (c: CHARACTER; n: INTEGER)
-- Initialize string with n copies of c.
require
valid_count: n >= 0
ensure
count_set: count = n;
filled: occurrences(c) = count
feature(s) from STRING
-- Testing:
is_empty: BOOLEAN
-- Has string length 0?
item (i: INTEGER): CHARACTER
-- Character at position i.
require
valid_index: valid_index(i)
infix "@" (i: INTEGER): CHARACTER
-- Character at position i.
require
valid_index: valid_index(i)
valid_index (i: INTEGER): BOOLEAN
-- True when i is valid (i.e., inside actual bounds).
ensure
definition: Result = (1 <= i and i <= count)
same_as (other: STRING): BOOLEAN
-- Case insensitive is_equal.
require
other /= Void
item_code (i: INTEGER): INTEGER
-- Code of character at position i.
require
valid_index: valid_index(i)
index_of (c: CHARACTER; start_index: INTEGER): INTEGER
-- Index of first occurrence of c at or after start_index,
-- 0 if none.
--
-- Note: see also first_index_of to start searching at 1.
-- Actually first_index_of is not exactely the equivalent of
-- index_of in release -0.76: when the search failed the result is
-- now 0 (and no longer count + 1). So, to update your code from
-- release -0.76 to release -0.75, replace index_of with
-- first_index_of and be careful to see what's done with the
-- result !
require
valid_start_index: start_index >= 1 and start_index <= count + 1
ensure
Result /= 0 implies item(Result) = c
reverse_index_of (c: CHARACTER; start_index: INTEGER): INTEGER
-- Index of first occurrence of c at or before start_index,
-- 0 if none.
--
-- Note: search is done in reverse direction, which means
-- from the index down to the first character.
require
valid_start_index: start_index >= 0 and start_index <= count
ensure
Result /= 0 implies item(Result) = c
first_index_of (c: CHARACTER): INTEGER
-- Index of first occurrence of c at index 1 or after index 1.
ensure
definition: Result = index_of(c,1)
has (c: CHARACTER): BOOLEAN
-- True if c is in the STRING.
has_substring (other: STRING): BOOLEAN
-- True if Current contains other.
require
other_not_void: other /= Void
occurrences (c: CHARACTER): INTEGER
-- Number of times character c appears in the string.
ensure
Result >= 0
has_suffix (s: STRING): BOOLEAN
-- True if suffix of Current is s.
require
s /= Void
has_prefix (p: STRING): BOOLEAN
-- True if prefix of Current is p.
require
p /= Void
feature(s) from STRING
-- Testing and Conversion:
is_boolean: BOOLEAN
-- Does Current represent a BOOLEAN?
-- Valid BOOLEANs are "True" and "False".
to_boolean: BOOLEAN
-- Boolean value
-- "True" yields True, "False" yields False (what a surprise).
require
represents_a_boolean: is_boolean
is_integer: BOOLEAN
-- Does 'Current' represent an INTEGER?
-- Result is true if and only if the following two conditions
-- hold:
--
-- 1. In the following BNF grammar, the value of Current can be
-- produced by "Integer_literal", if leading and trailing
-- separators are ignored:
--
-- Integer_literal = [Sign] Integer
-- Sign = "+" | "-"
-- Integer = Digit | Digit Integer
-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
--
-- 2. The numerical value represented by Current is within the
-- range that can be represented by an instance of type INTEGER.
to_integer: INTEGER
-- Current must look like an INTEGER.
require
is_integer
is_double: BOOLEAN
-- Can contents be read as a DOUBLE?
-- Fails for numbers where the base or "10 ^ exponent" are not in
-- the range Minimum_double ... Maximum_double. Parsing is done
-- positive. That means if Minimum_double.abs is not equal to
-- Maximum_double it will not work correctly. Furthermore the
-- arithmetric package used must support the value 'inf' for a
-- number greater than Maximum_double.
-- Result is true if and only if the following two conditions
-- hold:
--
-- 1. In the following BNF grammar, the value of Current can be
-- produced by "Real_literal", if leading or trailing separators
-- are ignored.
--
-- Real_literal = Mantissa [Exponent_part]
-- Exponent_part = "E" Exponent
-- | "e" Exponent
-- Exponent = Integer_literal
-- Mantissa = Decimal_literal
-- Decimal_literal = Integer_literal ["." Integer]
-- Integer_literal = [Sign] Integer
-- Sign = "+" | "-"
-- Integer = Digit | Digit Integer
-- Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"
--
--
-- 2. The numerical value represented by Current is within the
-- range that can be represented by an instance of type DOUBLE.
to_double: DOUBLE
-- Conversion to the corresponding DOUBLE value. The string must
-- looks like a DOUBLE (or like an INTEGER because fractionnal part
-- is optional). For an exact definition see 'is_double'.
-- Note that this conversion might not be exact.
require
represents_a_double: is_double
is_real: BOOLEAN
-- Can contents be read as a REAL?
to_real: REAL
-- Conversion to the corresponding REAL value.
-- The string must looks like a REAL (or like an
-- INTEGER because fractionnal part is optional).
require
is_integer or is_real
is_number: BOOLEAN
-- Can contents be read as a NUMBER?
to_number: NUMBER
-- Current must looks like an INTEGER.
require
is_number
is_bit: BOOLEAN
-- True when the contents is a sequence of bits (i.e., mixed
-- characters 0 and characters 1).
ensure
Result = (count = occurrences('0') + occurrences('1'))
to_hexadecimal
-- Convert Current bit sequence into the corresponding
-- hexadecimal notation.
require
is_bit
binary_to_integer: INTEGER
-- Assume there is enougth space in the INTEGER to store
-- the corresponding decimal value.
require
is_bit;
count <= Integer_bits
feature(s) from STRING
-- Modification:
resize (new_count: INTEGER)
-- Resize Current. When new_count is greater than
-- count, new positions are initialized with the
-- default value of type CHARACTER ('%U').
require
new_count >= 0
ensure
count = new_count;
capacity >= old capacity
clear
-- Clear out the current STRING.
-- Note: internal storage memory is neither released nor shrunk.
ensure
count = 0
wipe_out
-- Clear out the current STRING.
-- Note: internal storage memory is neither released nor shrunk.
ensure
count = 0
copy (other: like Current)
-- Copy other onto Current.
require
standard_same_dynamic_type(other)
ensure
count = other.count;
is_equal(other)
fill_with (c: CHARACTER)
-- Replace every character with c.
ensure
occurrences(c) = count
replace_all (old_character, new_character: like item)
-- Replace all occurrences of the element old_character by
-- new_character.
ensure
count = old count;
occurrences(old_character) = 0
append (s: STRING)
-- Append a copy of 's' to Current.
require
s_not_void: s /= Void
append_string (s: STRING)
-- Append a copy of 's' to Current.
require
s_not_void: s /= Void
prepend (other: STRING)
-- Prepend other to Current.
require
other /= Void
ensure
Current.is_equal(old other.twin + old Current.twin)
insert_string (s: STRING; i: INTEGER)
-- Insert s at index i, shifting characters from index i
-- to count rightwards.
require
string_not_void: s /= Void;
valid_insertion_index: 1 <= i and i <= count + 1
replace_substring (s: STRING; start_index, end_index: INTEGER)
-- Replace the substring from start_index to end_index,
-- inclusive, with s.
require
string_not_void: s /= Void;
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
infix "+" (other: STRING): like Current
-- Create a new STRING which is the concatenation of
-- Current and other.
require
other_exists: other /= Void
ensure
result_count: Result.count = count + other.count
put (c: CHARACTER; i: INTEGER)
-- Put c at index i.
require
valid_index: valid_index(i)
ensure
item(i) = c
swap (i1, i2: INTEGER)
require
valid_index(i1);
valid_index(i2)
ensure
item(i1) = old item(i2);
item(i2) = old item(i1)
insert_character (c: CHARACTER; i: INTEGER)
-- Inserts c at index i, shifting characters from
-- position 'i' to count rightwards.
require
valid_insertion_index: 1 <= i and i <= count + 1
ensure
item(i) = c
shrink (min_index, max_index: INTEGER)
-- Keep only the slice [min_index .. max_index] or nothing
-- when the slice is empty.
require
1 <= min_index;
max_index <= count;
min_index <= max_index + 1
ensure
count = max_index - min_index + 1
remove (i: INTEGER)
-- Remove character at position i.
require
valid_removal_index: valid_index(i)
ensure
count = old count - 1
add_first (c: CHARACTER)
-- Add c at first position.
ensure
count = 1 + old count;
item(1) = c
precede (c: CHARACTER)
-- Add c at first position.
ensure
count = 1 + old count;
item(1) = c
add_last (c: CHARACTER)
-- Append c to string.
ensure
count = 1 + old count;
item(count) = c
append_character (c: CHARACTER)
-- Append c to string.
ensure
count = 1 + old count;
item(count) = c
extend (c: CHARACTER)
-- Append c to string.
ensure
count = 1 + old count;
item(count) = c
to_lower
-- Convert all characters to lower case.
to_upper
-- Convert all characters to upper case.
as_lower: like Current
-- New object with all letters in lower case.
as_upper: like Current
-- New object with all letters in upper case.
keep_head (n: INTEGER)
-- Remove all characters except for the first n.
-- Do nothing if n >= count.
require
n_non_negative: n >= 0
ensure
count = n.min(old count)
keep_tail (n: INTEGER)
-- Remove all characters except for the last n.
-- Do nothing if n >= count.
require
n_non_negative: n >= 0
ensure
count = n.min(old count)
remove_head (n: INTEGER)
-- Remove n first characters. If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_first (n: INTEGER)
-- Remove n first characters. If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_tail (n: INTEGER)
-- Remove n last characters. If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_last (n: INTEGER)
-- Remove n last characters. If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_substring (start_index, end_index: INTEGER)
-- Remove all characters from strt_index to end_index inclusive.
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
count = old count - (end_index - start_index + 1)
remove_between (start_index, end_index: INTEGER)
-- Remove all characters from strt_index to end_index inclusive.
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
count = old count - (end_index - start_index + 1)
remove_suffix (s: STRING)
-- Remove the suffix s of current string.
require
has_suffix(s)
ensure
(old Current.twin).is_equal(Current + old s.twin)
remove_prefix (s: STRING)
-- Remove the prefix s of current string.
require
has_prefix(s)
ensure
(old Current.twin).is_equal(old s.twin + Current)
left_adjust
-- Remove leading blanks.
ensure
stripped: is_empty or else item(1) /= ' '
right_adjust
-- Remove trailing blanks.
ensure
stripped: is_empty or else item(count) /= ' '
feature(s) from STRING
-- Printing:
out_in_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
ensure
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))
fill_tagged_out_memory
-- Append a viewable information in tagged_out_memory in
-- order to affect the behavior of out, tagged_out, etc.
feature(s) from STRING
-- Agents based features:
do_all (action: ROUTINE[ANY,TUPLE[CHARACTER]])
-- Apply action to every item of Current.
for_all (test: PREDICATE[ANY,TUPLE[CHARACTER]]): BOOLEAN
-- Do all items satisfy test?
exists (test: PREDICATE[ANY,TUPLE[CHARACTER]]): BOOLEAN
-- Does at least one item satisfy test?
feature(s) from STRING
-- Other features:
first: CHARACTER
-- Access to the very first character.
require
not is_empty
ensure
definition: Result = item(1)
last: CHARACTER
-- Access to the very last character.
require
not is_empty
ensure
definition: Result = item(count)
substring (start_index, end_index: INTEGER): like Current
-- New string consisting of items [start_index.. end_index].
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
substring_count: Result.count = end_index - start_index + 1
extend_multiple (c: CHARACTER; n: INTEGER)
-- Extend Current with n times character c.
require
n >= 0
ensure
count = n + old count
precede_multiple (c: CHARACTER; n: INTEGER)
-- Prepend n times character c to Current.
require
n >= 0
ensure
count = n + old count
extend_to_count (c: CHARACTER; needed_count: INTEGER)
-- Extend Current with c until needed_count is reached.
-- Do nothing if needed_count is already greater or equal
-- to count.
require
needed_count >= 0
ensure
count >= needed_count
precede_to_count (c: CHARACTER; needed_count: INTEGER)
-- Prepend c to Current until needed_count is reached.
-- Do nothing if needed_count is already greater or equal
-- to count.
require
needed_count >= 0
ensure
count >= needed_count
reverse
-- Reverse the string.
remove_all_occurrences (ch: CHARACTER)
-- Remove all occurrences of ch.
ensure
count = old count - old occurrences(ch)
substring_index (other: STRING; start_index: INTEGER): INTEGER
-- Position of first occurrence of other at or after start
-- 0 if none.
require
other_not_void: other /= Void;
valid_start_index: start_index >= 1 and start_index <= count + 1
first_substring_index (other: STRING): INTEGER
-- Position of first occurrence of other at or after 1, 0 if none.
require
other_not_void: other /= Void
ensure
definition: Result = substring_index(other,1)
feature(s) from STRING
-- Splitting a STRING:
split: ARRAY[STRING]
-- Split the string into an array of words. Uses is_separator of
-- CHARACTER to find words. Gives Void or a non empty array.
ensure
Result /= Void implies not Result.is_empty
split_in (words: COLLECTION[STRING])
-- Same jobs as split but result is appended in words.
require
words /= Void
ensure
words.count >= old words.count
feature(s) from STRING
-- Other features:
extend_unless (ch: CHARACTER)
-- Extend Current (using extend) with ch unless ch is
-- already the last character.
ensure
last = ch;
count >= old count
get_new_iterator: ITERATOR[CHARACTER]
feature(s) from STRING
-- Interfacing with C string:
to_external: POINTER
-- Gives C access to the internal storage (may be dangerous).
-- To be compatible with C, a null character is added at the end
-- of the internal storage. This extra null character is not
-- part of the Eiffel STRING.
ensure
count = old count;
Result.is_not_null
from_external (p: POINTER)
-- Internal storage is set using p (may be dangerous because
-- the external C string p is not duplicated). Assume p has a
-- null character at the end in order to compute the Eiffel
-- count. This extra null character is not part of the Eiffel
-- STRING. Also consider from_external_copy to choose the most
-- appropriate.
require
p.is_not_null
ensure
capacity = count + 1;
p = to_external
from_external_copy (p: POINTER)
-- Internal storage is set using a copy of p. Assume p has a
-- null character at the end in order to compute the Eiffel
-- count. This extra null character is not part of the Eiffel
-- STRING. Also consider from_external to choose the most
-- appropriate.
require
p.is_not_null
from_c (p: POINTER)
-- Internal storage is set using a copy of p. Assume p has a
-- null character at the end in order to compute the Eiffel
-- count. This extra null character is not part of the Eiffel
-- STRING. Also consider from_external to choose the most
-- appropriate.
require
p.is_not_null
feature(s) from STRING
-- Other features here for ELKS compatibility:
make_from_string (model: STRING)
-- (Here for ELKS compatibility.)
-- Initialize from the characters of model.
-- Useful in proper descendants of STRING.
require
model /= Void
ensure
count = model.count
same_string (other: STRING): BOOLEAN
-- (Here for ELKS compatibility.)
-- Do Current and other have the same character sequence?
-- Useful in proper descendants of STRING.
require
other_not_void: other /= Void
string: STRING
-- (Here for ELKS compatibility.)
-- New STRING having the same character sequence as Current.
-- Useful in proper descendants of STRING.
feature(s)
invariant
0 <= count;
count <= capacity;
capacity > 0 implies storage.is_not_null;
end of STRING