class interface STRING
--
-- Resizable character STRINGs.
--
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
other_not_void: other /= Void
ensure
count = other.count;
is_equal: is_equal(other)
blank (nr_blanks: INTEGER)
-- Initialize string with nr_blanks blanks.
require
nr_blanks >= 0
ensure
count = nr_blanks;
occurrences_of(' ') = 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.
make_from_string (s: STRING)
-- Initialize from the characters of s.
-- (Useful in proper descendants of class STRING, to
-- initialize a string-like object from a manifest string.)
require
s /= Void
ensure
count = s.count
feature(s) from HASHABLE
hash_code: INTEGER
-- The hash-code value of Current.
ensure
good_hash_value: Result >= 0
feature(s) from COMPARABLE
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.
capacity: INTEGER
-- Capacity of the storage.
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
blank (nr_blanks: INTEGER)
-- Initialize string with nr_blanks blanks.
require
nr_blanks >= 0
ensure
count = nr_blanks;
occurrences_of(' ') = count
feature(s) from STRING
-- Testing :
empty: BOOLEAN
-- Has string length 0?
item (index: INTEGER): CHARACTER
-- Character at position index.
require
valid_index(index)
infix "@" (index: INTEGER): CHARACTER
-- Character at position index.
require
valid_index(index)
valid_index (index: INTEGER): BOOLEAN
-- True when index is valid (i.e., inside actual bounds).
ensure
Result = (1 <= index and then index <= count)
same_as (other: STRING): BOOLEAN
-- Case insensitive is_equal.
require
other /= Void
is_equal (other: like Current): BOOLEAN
-- Has Current the same text as other ?
require
other_not_void: other /= Void
ensure
consistent: standard_is_equal(other) implies Result;
symmetric: Result implies other.is_equal(Current)
index_of (ch: CHARACTER): INTEGER
-- Gives the index of the first occurrence ch or
-- count + 1 if none.
ensure
Result /= count + 1 implies item(Result) = ch
index_of_string (other: STRING): INTEGER
-- Position of the first occurrence of other
-- or count + 1 if none.
require
not other.empty
has (ch: CHARACTER): BOOLEAN
-- True if ch is in the STRING.
has_string (other: STRING): BOOLEAN
-- True if other is in the STRING.
occurrences_of (c: CHARACTER): INTEGER
-- Number of times character c appears in the string.
ensure
Result >= 0
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
replace_all (old_character, new_character: like item)
-- Replace all occurrences of the element old_character by
-- new_character.
ensure
count = old count;
occurrences_of(old_character) = 0
is_integer: BOOLEAN
-- Can contents be read as an INTEGER ?
is_real: BOOLEAN
-- Contents can be read as a REAL.
is_double: BOOLEAN
-- Contents can be read as a DOUBLE.
is_bit: BOOLEAN
-- True when the contents is a sequence of bits (i.e., mixed
-- characters 0 and characters 1).
ensure
Result = (count = occurrences_of('0') + occurrences_of('1'))
feature(s) from STRING
-- Modification :
clear
-- Clear out the current STRING.
-- Note : internal storage memory is neither released nor shrunk.
ensure
count = 0
feature(s) from STRING
-- Modification :
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
other_not_void: other /= Void
ensure
count = other.count;
is_equal: is_equal(other)
fill (c: CHARACTER)
-- Replace every character with c.
ensure
occurrences_of(c) = count
fill_with (c: CHARACTER)
-- Replace every character with c.
ensure
occurrences_of(c) = count
fill_blank
-- Fill entire string with blanks
ensure
occurrences_of(' ') = count
append (other: STRING)
-- Append other to Current.
require
other /= Void
append_string (other: STRING)
-- Append other to Current.
require
other /= Void
prepend (other: STRING)
-- Prepend other to Current
require
other /= Void
ensure
count = other.count + old count
infix "+" (other: STRING): STRING
-- Create a new STRING which is the concatenation of
-- Current and other.
require
other /= Void
ensure
Result.count = count + other.count
put (ch: CHARACTER; index: INTEGER)
-- Put ch at position index.
require
valid_index(index)
ensure
item(index) = ch
swap (i1, i2: INTEGER)
require
valid_index(i1);
valid_index(i2)
ensure
item(i1) = old item(i2);
item(i2) = old item(i1)
insert (ch: CHARACTER; index: INTEGER)
-- Insert ch after position index.
require
0 <= index and index <= count
ensure
item(index + 1) = ch
shrink (low, up: INTEGER)
-- Keep only the slice low .. up or nothing
-- when the slice is empty.
require
1 <= low;
low <= count;
1 <= up;
up <= count
ensure
up > low implies count = up - low + 1
remove (index: INTEGER)
-- Remove character at position index.
require
valid_index(index)
ensure
count = old count - 1
add_first (ch: CHARACTER)
-- Add ch at first position.
ensure
count = 1 + old count;
item(1) = ch
add_last (ch: CHARACTER)
-- Append ch to string
ensure
count = 1 + old count;
item(count) = ch
extend (ch: CHARACTER)
-- Append ch to string
ensure
count = 1 + old count;
item(count) = ch
append_character (ch: CHARACTER)
-- Append ch to string
ensure
count = 1 + old count;
item(count) = ch
precede (ch: CHARACTER)
-- Prepend ch to string
ensure
item(1) = ch
to_lower
-- Convert all characters to lower case.
to_upper
-- Convert all characters to upper case.
remove_first (nb: INTEGER)
-- Remove nb first characters.
require
nb >= 0;
count >= nb
ensure
count = old count - nb
remove_last (nb: INTEGER)
-- Remove nb last characters.
require
0 <= nb;
nb <= count
ensure
count = old count - nb
remove_between (low, up: INTEGER)
-- Remove character between positions low and up.
require
valid_index(low);
valid_index(up);
low <= up
ensure
count = old count - up - low + 1
remove_suffix (s: STRING)
-- Remove the suffix s of current string.
require
has_suffix(s)
ensure
old count = count + s.count
remove_prefix (s: STRING)
-- Remove the prefix s of current string.
require
has_prefix(s)
ensure
old count = count + s.count
left_adjust
-- Remove leading blanks.
ensure
stripped: empty or else item(1) /= ' '
right_adjust
-- Remove trailing blanks.
ensure
stripped: empty or else item(count) /= ' '
feature(s) from STRING
-- Features which don't modify the string
first: CHARACTER
require
not empty
last: CHARACTER
require
not empty
feature(s) from STRING
-- Conversion :
to_integer: INTEGER
-- Current must looks like an INTEGER.
require
is_integer
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
to_double: DOUBLE
-- Conversion to the corresponding DOUBLE value.
-- The string must looks like a DOUBLE, like
-- a REAL (or like an INTEGER because fractionnal
-- part is optional).
require
is_integer or is_real
binary_to_integer: INTEGER
-- Assume there is enougth space in the INTEGER to store
-- the corresponding decimal value.
require
is_bit;
count <= Integer_bits
to_hexadecimal
-- Convert Current bit sequence into the corresponding
-- hexadecimal notation.
require
is_bit
feature(s) from STRING
-- Printing :
out_in_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
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
-- Other features :
substring (low, up: INTEGER): like Current
-- Create a new string initialized with range low.. up.
require
1 <= low;
low <= up;
up <= count
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_of(ch)
substring_index (other: STRING; start: INTEGER): INTEGER
-- Position of first occurrence of other at or after
-- start;
-- 0 if none.
require
start_large_enough: start >= 1;
start_small_enough: start <= count;
string_exist: other /= Void
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.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 feature :
set_last (ch: CHARACTER)
ensure
last = ch
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.
feature(s) from STRING
-- Other feature here for ELKS'95 compatibility :
make_from_string (s: STRING)
-- Initialize from the characters of s.
-- (Useful in proper descendants of class STRING, to
-- initialize a string-like object from a manifest string.)
require
s /= Void
ensure
count = s.count
head (n: INTEGER)
-- Remove all characters except fo the first n.
-- Do nothing if n >= count.
require
n >= 0
ensure
count = n.min(old count)
tail (n: INTEGER)
-- Remove all characters except for the last n.
-- Do nothing if n >= count.
require
n >= 0
ensure
count = n.min(old count)
invariant
0 <= count;
count <= capacity;
capacity > 0 implies storage.is_not_null;
end of STRING