Class STRING
Halstenbach Eiffel 3.1
indexing
description: "Sequences of characters, accessible through integer indices", "in a contiguous range."
class interface
STRING
creation
make (n: INTEGER)
-- Allocate space for at least n characters.
require
non_negative_size: n >= 0
ensure
empty_string: count = 0;
area_allocated: capacity >= n
feature -- Initialization
adapt (s: STRING): like Current
-- Object of a type conforming to the type of s,
-- initialized with attributes from s
from_c (c_string: POINTER)
-- Reset contents of string from contents of c_string,
-- a string created by some external C function.
require
c_string_exists: c_string /= default_pointer
from_c_substring (c_string: POINTER; start_pos, end_pos: INTEGER)
-- Reset contents of string from substring of c_string,
-- a string created by some external C function.
require
c_string_exists: c_string /= default_pointer;
start_position_big_enough: start_pos >= 1;
end_position_big_enough: start_pos <= end_pos + 1
ensure
valid_count: count = end_pos - start_pos + 1
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
string_exists: s /= void
ensure
shared_implementation: shared_with (s)
remake (n: INTEGER)
-- Allocate space for at least n characters.
require
non_negative_size: n >= 0
ensure
empty_string: count = 0;
area_allocated: capacity >= n
feature -- Access
area: SPECIAL [CHARACTER]
-- Special data zone
-- (from TO_SPECIAL)
False_constant: STRING is "false"
-- Constant string "false"
fuzzy_index (other: STRING; start: INTEGER; fuzz: INTEGER): INTEGER
-- Position of first occurrence of other at or after start
-- with 0..fuzz mismatches between the string and other.
-- 0 if there are no fuzzy matches
require
other_exists: other /= void;
other_not_empty: not other.empty;
start_large_enough: start >= 1;
start_small_enough: start <= count;
acceptable_fuzzy: fuzz <= other.count
has (c: CHARACTER): BOOLEAN
-- Does string include c?
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
hash_code: INTEGER
-- Hash code value
ensure -- from HASHABLE
good_hash_value: Result >= 0
index_of (c: CHARACTER; start: INTEGER): INTEGER
-- Position of first occurrence of c at or after start;
-- 0 if none.
require
start_large_enough: start >= 1;
start_small_enough: start <= count
ensure
correct_place: Result > 0 implies item (Result) = c
item (i: INTEGER): CHARACTER
-- Character at position i
-- Was declared in STRING as synonym of item and @.
require -- from TABLE
valid_key: valid_index (i)
shared_with (other: like Current): BOOLEAN
-- Does string share the text of other?
substring_index (other: STRING; start: INTEGER): INTEGER
-- Position of first occurrence of other at or after start;
-- 0 if none.
require
other_nonvoid: other /= void;
other_notempty: not other.empty;
start_large_enough: start >= 1;
start_small_enough: start <= count
ensure
correct_place: Result > 0 implies substring (Result, Result + other.count - 1).is_equal (other)
True_constant: STRING is "true"
-- Constant string "true"
infix "@" (i: INTEGER): CHARACTER
-- Character at position i
-- Was declared in STRING as synonym of item and @.
require -- from TABLE
valid_key: valid_index (i)
feature -- Measurement
additional_space: INTEGER
-- Proposed number of additional items
-- (from RESIZABLE)
ensure -- from RESIZABLE
at_least_one: Result >= 1
capacity: INTEGER
-- Allocated space
count: INTEGER
-- Actual number of characters making up the string
Growth_percentage: INTEGER is 50
-- Percentage by which structure will grow automatically
-- (from RESIZABLE)
Minimal_increase: INTEGER is 5
-- Minimal number of additional items
-- (from RESIZABLE)
occurrences (c: CHARACTER): INTEGER
-- Number of times c appears in the string
ensure -- from BAG
non_negative_occurrences: Result >= 0
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is string made of same character sequence as other
-- (possibly with a different capacity)?
require -- COMPARABLE
precursor: True
require -- from GENERAL
other_not_void: other /= void
ensure then -- from COMPARABLE
trichotomy: Result = (not (Current < other) and not (other < Current))
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
max (other: like Current): like Current
-- The greater of current object and other
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
current_if_not_smaller: Current >= other implies Result = Current;
other_if_smaller: Current < other implies Result = other
min (other: like Current): like Current
-- The smaller of current object and other
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
current_if_not_greater: Current <= other implies Result = Current;
other_if_greater: Current > other implies Result = other
three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
-- (from COMPARABLE)
require -- from COMPARABLE
other_exists: other /= void
ensure -- from COMPARABLE
equal_zero: (Result = 0) = is_equal (other);
smaller_negative: (Result = - 1) = (Current < other);
greater_positive: (Result = 1) = (Current > other)
infix "<" (other: like Current): BOOLEAN
-- Is string lexicographically lower than other?
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
-- Is current object less than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (Current < other) or is_equal (other)
infix ">" (other: like Current): BOOLEAN
-- Is current object greater than other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
-- Is current object greater than or equal to other?
-- (from COMPARABLE)
require -- from PART_COMPARABLE
other_exists: other /= void
ensure then -- from COMPARABLE
definition: Result = (other <= Current)
feature -- Status report
Changeable_comparison_criterion: BOOLEAN is false
consistent (other: like Current): BOOLEAN
-- Is object in a consistent state so that other
-- may be copied onto it? (Default answer: yes).
empty: BOOLEAN
-- Is structure empty?
-- (from FINITE)
Extendible: BOOLEAN is true
-- May new items be added? (Answer: yes.)
full: BOOLEAN
-- Is structure full?
-- (from BOUNDED)
is_boolean: BOOLEAN
-- Is the string representing a boolean?
is_double: BOOLEAN
-- Is the string representing a double?
is_hashable: BOOLEAN
-- May current object be hashed?
-- (True if it is not its type's default.)
-- (from HASHABLE)
ensure -- from HASHABLE
ok_if_not_default: Result implies (Current /= default)
is_integer: BOOLEAN
-- Is the string representing an integer?
is_real: BOOLEAN
-- Is the string representing a real?
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
prunable: BOOLEAN
-- May items be removed? (Answer: yes.)
resizable: BOOLEAN
-- May capacity be changed? (Answer: yes.)
-- (from RESIZABLE)
valid_index (i: INTEGER): BOOLEAN
-- Is i within the bounds of the string?
feature -- Status setting
compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison
compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison
feature -- Element change
append (s: STRING)
-- Append a copy of s at end.
require
argument_not_void: s /= void
ensure then
new_count: count = old count + old (s.count)
append_boolean (b: BOOLEAN)
-- Append the string representation of b at end.
append_character (c: CHARACTER)
-- Append c at end.
-- Was declared in STRING as synonym of append_character and extend.
ensure then
item_inserted: item (count) = c
append_double (d: DOUBLE)
-- Append the string representation of d at end.
append_integer (i: INTEGER)
-- Append the string representation of i at end.
append_real (r: REAL)
-- Append the string representation of r at end.
append_string (s: STRING)
-- Append a copy of s, if not void, at end.
copy (other: like Current)
-- Reinitialize by copying the characters of other.
-- (This is also used by clone.)
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
ensure then
new_result_count: count = other.count
extend (c: CHARACTER)
-- Append c at end.
-- Was declared in STRING as synonym of append_character and extend.
require -- from COLLECTION
extendible: extendible
ensure -- from COLLECTION
item_inserted: has (c)
ensure then -- from BAG
one_more_occurrence: occurrences (c) = old (occurrences (c)) + 1
ensure then
item_inserted: item (count) = c
fill_from_container (other: CONTAINER [CHARACTER])
-- Fill with as many items of other as possible.
-- The representations of other and current structure
-- need not be the same.
-- (from COLLECTION)
require -- from COLLECTION
other_not_void: other /= void;
extendible
fill_blank
-- Fill with blanks.
fill_character (c: CHARACTER)
-- Fill with c.
head (n: INTEGER)
-- Remove all characters except for the first n;
-- do nothing if n >= count.
require
non_negative_argument: n >= 0
ensure
new_count: count = n.min (old count)
insert (s: like Current; i: INTEGER)
-- Add s to the left of position i in current string.
require
string_exists: s /= void;
index_small_enough: i <= count;
index_large_enough: i > 0
ensure
new_count: count = old count + s.count
insert_character (c: CHARACTER; i: INTEGER)
-- Add c to the left of position i in current string.
require
index_small_enough: i <= count;
index_large_enough: i > 0
ensure
new_count: count = old count + 1;
inserted: item (i + 1) = c
left_adjust
-- Remove leading whitespace.
ensure
new_count: (count /= 0) implies ((item (1) /= ' ') and (item (1) /= '%T') and (item (1) /= '%R') and (item (1) /= '%N'))
precede (c: CHARACTER)
-- Add c at front.
ensure
new_count: count = old count + 1
prepend (s: STRING)
-- Prepend a copy of s at front.
require
argument_not_void: s /= void
ensure
new_count: count = old count + s.count
prepend_boolean (b: BOOLEAN)
-- Prepend the string representation of b at front.
prepend_character (c: CHARACTER)
-- Prepend the string representation of c at front.
prepend_double (d: DOUBLE)
-- Prepend the string representation of d at front.
prepend_integer (i: INTEGER)
-- Prepend the string representation of i at front.
prepend_real (r: REAL)
-- Prepend the string representation of r at front.
prepend_string (s: STRING)
-- Prepend a copy of s, if not void, at front.
put (c: CHARACTER; i: INTEGER)
-- Replace character at position i by c.
require -- from TABLE
valid_key: valid_index (i)
ensure then -- from INDEXABLE
insertion_done: item (i) = c
put_substring (s: like Current; start_pos, end_pos: INTEGER)
-- Copy the characters of s to positions
-- start_pos .. end_pos.
-- Was declared in STRING as synonym of put_substring and replace_substring.
require
string_exists: s /= void;
index_small_enough: end_pos <= count;
order_respected: start_pos <= end_pos;
index_large_enough: start_pos > 0
ensure
new_count: count = old count + s.count - end_pos + start_pos - 1
replace_substring (s: like Current; start_pos, end_pos: INTEGER)
-- Copy the characters of s to positions
-- start_pos .. end_pos.
-- Was declared in STRING as synonym of put_substring and replace_substring.
require
string_exists: s /= void;
index_small_enough: end_pos <= count;
order_respected: start_pos <= end_pos;
index_large_enough: start_pos > 0
ensure
new_count: count = old count + s.count - end_pos + start_pos - 1
replace_substring_all (original, new: like Current)
-- Replace every occurence of original with new.
require
original_exists: original /= void;
new_exists: new /= void;
original_not_empty: not original.empty;
not_empty: not empty
right_adjust
-- Remove trailing whitespace.
ensure
new_count: (count /= 0) implies ((item (count) /= ' ') and (item (count) /= '%T') and (item (count) /= '%R') and (item (count) /= '%N'))
set (t: like Current; n1, n2: INTEGER)
-- Set current string to substring of t from indices n1
-- to n2, or to empty string if no such substring.
require
argument_not_void: t /= void
ensure
is_substring: is_equal (t.substring (n1, n2))
share (other: like Current)
-- Make current string share the text of other.
-- Subsequent changes to the characters of current string
-- will also affect other, and conversely.
require
argument_not_void: other /= void
ensure
shared_count: other.count = count
subcopy (other: like Current; start_pos, end_pos, index_pos: INTEGER)
-- Copy characters of other within bounds start_pos and
-- end_pos to current string starting at index index_pos.
require
other_not_void: other /= void;
valid_start_pos: other.valid_index (start_pos);
valid_end_pos: other.valid_index (end_pos);
valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1);
valid_index_pos: valid_index (index_pos);
enough_space: (count - index_pos) >= (end_pos - start_pos)
tail (n: INTEGER)
-- Remove all characters except for the last n;
-- do nothing if n >= count.
require
non_negative_argument: n >= 0
ensure
new_count: count = n.min (old count)
feature -- Removal
prune (c: CHARACTER)
-- Remove first occurrence of c, if any.
require -- from COLLECTION
prunable: prunable
require else
true
prune_all (c: CHARACTER)
-- Remove all occurrences of c.
require -- from COLLECTION
prunable
require else
true
ensure -- from COLLECTION
no_more_occurrences: not has (c)
ensure then
changed_count: count = (old count) - (old occurrences (c))
prune_all_leading (c: CHARACTER)
-- Remove all leading occurrences of c.
prune_all_trailing (c: CHARACTER)
-- Remove all trailing occurrences of c.
remove (i: INTEGER)
-- Remove i-th character.
require
index_small_enough: i <= count;
index_large_enough: i > 0
ensure
new_count: count = old count - 1
wipe_out
-- Remove all characters.
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: empty
ensure then
empty_string: count = 0;
empty_area: capacity = 0;
wiped_out: empty
feature -- Resizing
adapt_size
-- Adapt the size to accommodate count characters.
automatic_grow
-- Change the capacity to accommodate at least
-- Growth_percentage more items.
-- (from RESIZABLE)
ensure -- from RESIZABLE
increased_capacity: capacity >= old capacity + old capacity * growth_percentage // 100
grow (newsize: INTEGER)
-- Ensure that the capacity is at least newsize.
require -- RESIZABLE
precursor: True
require else
new_size_non_negative: newsize >= 0
ensure -- from RESIZABLE
new_capacity: capacity >= newsize
resize (newsize: INTEGER)
-- Rearrange string so that it can accommodate
-- at least newsize characters.
-- Do not lose any previously entered character.
require
new_size_non_negative: newsize >= 0
feature -- Conversion
center_justify
-- Center justify the string using
-- the capacity as the width
character_justify (pivot: CHARACTER; position: INTEGER)
-- Justify a string based on a pivot
-- and the position it needs to be in
-- the final string.
-- This will grow the string if necessary
-- to get the pivot in the correct place.
require
valid_position: position <= capacity;
positive_position: position >= 1;
pivot_not_space: pivot /= ' ';
not_empty: not empty
left_justify
-- Left justify the string using
-- the capacity as the width
linear_representation: LINEAR [CHARACTER]
-- Representation as a linear structure
mirror
-- Reverse the order of characters.
-- "Hello world" -> "dlrow olleH".
ensure
same_count: count = old count
mirrored: like Current
-- Mirror image of string;
-- result for "Hello world" is "dlrow olleH".
ensure
same_count: Result.count = count
right_justify
-- Right justify the string using
-- the capacity as the width
to_boolean: BOOLEAN
-- Boolean value;
-- "true" yields True, "false" yields False
-- (case-insensitive)
require
is_boolean: is_boolean
frozen to_c: ANY
-- A reference to a C form of current string.
-- Useful only for interfacing with C software.
to_double: DOUBLE
-- "Double" value;
-- for example, when applied to "123.0", will yield 123.0 (double)
require
is_double: is_double
to_integer: INTEGER
-- Integer value;
-- for example, when applied to "123", will yield 123
require
is_integer: is_integer
to_lower
-- Convert to lower case.
to_real: REAL
-- Real value;
-- for example, when applied to "123.0", will yield 123.0
require
is_real: is_real
to_upper
-- Convert to upper case.
feature -- Duplication
multiply (n: INTEGER)
-- Duplicate a string within itself
-- ("hello").multiply(3) => "hellohellohello"
require
meaningful_multiplier: n >= 1
substring (n1, n2: INTEGER): like Current
-- Copy of substring containing all characters at indices
-- between n1 and n2
require
meaningful_origin: 1 <= n1;
meaningful_interval: n1 <= n2;
meaningful_end: n2 <= count
ensure
new_result_count: Result.count = n2 - n1 + 1
infix "+" (other: ANY): like Current
-- New string built by appending other.out to
-- the current object
require
other_not_void: other /= void
ensure
new_string: Result /= Current and Result /= other;
correct_count: Result.count = count + other.out.count;
correct_characters: Result.substring_index (Current, 1) = 1 and Result.substring_index (other.out, count + 1) = count + 1
feature -- Output
out: like Current
-- Printable representation
ensure then
result_not_void: Result /= void
invariant
extendible: extendible;
compare_character: object_comparison = false;
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
-- from RESIZABLE
increase_by_at_least_one: minimal_increase >= 1;
-- from BOUNDED
valid_count: count <= capacity;
full_definition: full = (count = capacity);
-- from FINITE
empty_definition: empty = (count = 0);
non_negative_count: count >= 0;
-- from COMPARABLE
irreflexive_comparison: not (Current < Current);
end -- class STRING