Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.elks

Class KS_STRING


Direct ancestors

KS_HASHABLE, KS_COMPARABLE, KL_IMPORTED_STRING_ROUTINES, KL_IMPORTED_ANY_ROUTINES, KL_IMPORTED_CHARACTER_ROUTINES, KL_SHARED_PLATFORM

Known direct descendants

UC_STRING

Features

Invariants

indexing

description

Portable interface for class STRING

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001-2004, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/06/04 20:08:11 $

revision

$Revision: 1.16 $

deferred class

KS_STRING

inherit

KS_HASHABLE
KS_COMPARABLE
KL_IMPORTED_STRING_ROUTINES
KL_IMPORTED_ANY_ROUTINES
KL_IMPORTED_CHARACTER_ROUTINES
KL_SHARED_PLATFORM

feature -- Initialization

make (suggested_capacity: INTEGER)

-- Create empty string, or remove all characters from
-- existing string.
-- (ELKS 2001 STRING)

require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
empty_string: count = 0
make_from_string (s: STRING)

-- Initialize from the character sequence of s.
-- (ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.make_from_string instead of this
-- routine when Current can be of dynamic type STRING and s
-- of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.

require
s_not_void: s /= Void
ensure
initialized: same_string (s)

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
character_: KL_CHARACTER_ROUTINES

-- Routines that ought to be in class CHARACTER

-- (From KL_IMPORTED_CHARACTER_ROUTINES)

ensure
character_routines_not_void: Result /= Void
platform: KL_PLATFORM

-- Platform-dependent properties

-- (From KL_SHARED_PLATFORM)

ensure
platform_not_void: Result /= Void
string_: KL_STRING_ROUTINES

-- Routines that ought to be in class STRING

-- (From KL_IMPORTED_STRING_ROUTINES)

ensure
string_routines_not_void: Result /= Void
hash_code: INTEGER

-- Hash code value
-- (ELKS 95 HASHABLE)

-- (From KS_HASHABLE)

ensure
good_hash_value: Result >= 0
index_of (c: CHARACTER; start_index: INTEGER): INTEGER

-- Index of first occurrence of c at or after start_index;
-- 0 if none
-- (ELKS 2001 STRING)

require
valid_start_index: start_index >= 1 and start_index <= count + 1
ensure
valid_result: Result = 0 or (start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) = not substring (start_index, count).has (c)
found_if_present: substring (start_index, count).has (c) implies item (Result) = c
none_before: substring (start_index, count).has (c) implies not substring (start_index, Result - 1).has (c)
infix "+" (other: STRING): like Current

-- New object which is a clone of Current extended
-- by the characters of other
-- (ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.concat instead of this routine when
-- Current can be of dynamic type STRING and other of dynamic
-- type other than STRING such as UC_STRING, because class STRING
-- provided by the Eiffel compilers is not necessarily aware of
-- the implementation of UC_STRING and this may lead to run-time
-- errors or crashes.

require
other_not_void: other /= Void
ensure
result_not_void: Result /= Void
result_count: Result.count = count + other.count
initial: Result.substring (1, count).is_equal (Current)
final: Result.substring (count + 1, count + other.count).same_string (other)
infix "@" (i: INTEGER): CHARACTER

-- Character at index i
-- (ELKS 2001 STRING)

require
valid_index: valid_index (i)
ensure
definition: Result = item (i)
item (i: INTEGER): CHARACTER

-- Character at index i;
-- '%U' if the character at index i cannot fit into a CHARACTER
-- (Extended from ELKS 2001 STRING)
-- Note: Use item_code instead of this routine when Current
-- can be of dynamic type other than STRING (e.g. UC_STRING) and
-- its characters may not fit into a CHARACTER.

require
valid_index: valid_index (i)
ensure
code_small_enough: item_code (i) <= Platform.Maximum_character_code implies Result.code = item_code (i)
overflow: item_code (i) > Platform.Maximum_character_code implies Result = '%U'
item_code (i: INTEGER): INTEGER

-- Code of character at index i

require
valid_index: valid_index (i)
ensure
item_code_positive: Result >= 0
string: STRING

-- New STRING having the same character sequence as Current
-- where characters which do not fit in a CHARACTER are
-- replaced by a '%U'
-- (Extended from ELKS 2001 STRING)

ensure
string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
first_item: count > 0 implies Result.item (1) = item (1)
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).string)
substring (start_index, end_index: INTEGER): like Current

-- New object containing all characters from start_index
-- to end_index inclusive
-- (ELKS 2001 STRING)

require
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningful_interval: start_index <= end_index + 1
ensure
substring_not_void: Result /= Void
substring_count: Result.count = end_index - start_index + 1
first_item: Result.count > 0 implies Result.item (1) = item (start_index)
substring_index (other: STRING; start_index: INTEGER): INTEGER

-- Index of first occurrence of other at or after start_index in
-- a_string; 0 if none. a_string and other are considered with
-- their characters which do not fit in a CHARACTER replaced by a '%U'.
-- (Extended from ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.substring_index instead of this
-- routine when Current can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.

require
other_not_void: other /= Void
valid_start_index: start_index >= 1 and start_index <= count + 1
ensure
valid_result: Result = 0 or else (start_index <= Result and Result <= count - other.count + 1)
zero_if_absent: (Result = 0) = not substring (start_index, count).has_substring (other)
at_this_index: Result >= start_index implies other.same_string (substring (Result, Result + other.count - 1).current_string)
none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_substring (other)

feature -- Measurement

count: INTEGER

-- Number of characters
-- (ELKS 2001 STRING)

occurrences (c: CHARACTER): INTEGER

-- Number of times c appears in the string
-- (ELKS 2001 STRING)

ensure
zero_if_empty: count = 0 implies Result = 0
recurse_if_not_found_at_first_position: (count > 0 and then item (1) /= c) impliesResult = substring (2, count).occurrences (c)
recurse_if_found_at_first_position: (count > 0 and then item (1) = c) impliesResult = 1 + substring (2, count).occurrences (c)

feature -- Comparison

infix "<" (other: like Current): BOOLEAN

-- Note: ELKS 2001 specifies other of type STRING, but this routine
-- is inherited from COMPARABLE with another signature:
-- infix "<" (other: STRING): BOOLEAN is
-- Is string lexicographically lower than other?
-- (Extended from ELKS 2001 STRING)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
asymmetric: Result implies not (other < Current)
ensure then
definition: ANY_.same_types (Current,
) implies Result = (count = 0 and other.count > 0 orcount > 0 and then other.count > 0 and then (item (1) < other.item (1) oritem (1) = other.item (1) and substring (2, count) < other.substring (2, other.count)))
infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
definition: Result = (Current < other or is_equal (other))
infix ">" (other: like Current): BOOLEAN

-- Is current object greater than other?
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN

-- Is current object greater than or equal to other?
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
definition: Result = (other <= Current)
is_equal (other: like Current): BOOLEAN

-- Is other attached to an object considered equal
-- to current object?
-- (Extended from ELKS 2001 STRING)

-- (From ANY)

require
other_not_void: other /= Void
ensure
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then
definition: ANY_.same_types (Current,
) implies(Result = (ANY_.same_types (Current, other) and then count = other.count and then(count > 0 implies (item (1) = other.item (1) and(count > 1 implies substring (2, count).is_equal (other.substring (2, count)))))))
max (other: like Current): like Current

-- The greater of current object and other
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
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
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
current_if_not_greater: (Current <= other) implies (Result = Current)
other_if_greater: (Current > other) implies (Result = other)
same_string (other: STRING): BOOLEAN

-- Do Current and other have the same character sequence?
-- Current is considered with its characters which do not
-- fit in a CHARACTER replaced by a '%U'.
-- (Extended from ELKS 2001 STRING)
-- Note: Use feature KL_STRING_ROUTINES.elks_same_string instead of
-- this routine when Current can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING,
-- because class STRING provided by the Eiffel compilers is
-- not necessarily aware of the implementation of UC_STRING
-- and this may lead to run-time errors or crashes.

require
other_not_void: other /= Void
ensure
definition: Result = string.is_equal (other.string)
three_way_comparison (other: like Current): INTEGER

-- If current object equal to other, 0; if smaller,
-- -1; if greater, 1.
-- (ELKS 95 COMPARABLE)

-- (From KS_COMPARABLE)

require
other_not_void: other /= Void
ensure
equal_zero: (Result = 0) = is_equal (other)
smaller_negative: (Result = -1) = (Current < other)
greater_positive: (Result = 1) = (Current > other)

feature -- Status report

has (c: CHARACTER): BOOLEAN

-- Does Current contain c?
-- (ELKS 2001 STRING)

ensure
false_if_empty: count = 0 implies not Result
true_if_first: count > 0 and then item (1) = c implies Result
recurse: (count > 0 and then item (1) /= c) implies (Result = substring (2, count).has (c))
has_substring (other: STRING): BOOLEAN

-- Does Current contain other?
-- other and Current are considered with their characters
-- which do not fit in a CHARACTER replaced by a '%U'.
-- (Extented from ELKS 2001 STRING)
-- Note: Use feature KL_STRING_ROUTINES.has_substring instead of
-- this routine when Current can be of dynamic type STRING and
-- other of dynamic type other than STRING such as UC_STRING,
-- because class STRING provided by the Eiffel compilers is
-- not necessarily aware of the implementation of UC_STRING
-- and this may lead to run-time errors or crashes.

require
other_not_void: other /= Void
ensure
false_if_too_small: count < other.count implies not Result
true_if_initial: (count >= other.count and then other.same_string (substring (1, other.count).current_string)) implies Result
recurse: (count >= other.count and then not other.same_string (substring (1, other.count).current_string)) implies (Result = substring (2, count).has_substring (other))
is_empty: BOOLEAN

-- Is string empty?
-- (ELKS 2001 STRING)

ensure
definition: Result = (count = 0)
valid_index (i: INTEGER): BOOLEAN

-- Is i within the bounds of the string?
-- (ELKS 2001 STRING)

ensure
definition: Result = (1 <= i and i <= count)

feature -- Element change

append_character (c: CHARACTER)

-- Append c at end.
-- (ELKS 2001 STRING)

ensure
new_count: count = old count + 1
appended: item (count) = c
stable_before: substring (1, count - 1).current_string.is_equal (old STRING_.cloned_string (current_string))
append_string (s: STRING)

-- Append a copy of s at end.
-- (ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.appended_string instead of
-- this routine when Current can be of dynamic type STRING and
-- s of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.

require
s_not_void: s /= Void
ensure
appended: current_string.is_equal (old STRING_.cloned_string (current_string) + old STRING_.cloned_string (s))
fill_with (c: CHARACTER)

-- Replace every character with c.
-- (ELKS 2001 STRING)

ensure
same_count: old count = count
filled: occurrences (c) = count
insert_character (c: CHARACTER; i: INTEGER)

-- Insert c at index i, shifting characters between
-- ranks i and count rightwards.
-- (ELKS 2001 STRING)

require
valid_insertion_index: 1 <= i and i <= count + 1
ensure
one_more_character: count = old count + 1
inserted: item (i) = c
stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1))
stable_after_i: substring (i + 1, count).is_equal (old substring (i, count))
insert_string (s: STRING; i: INTEGER)

-- Insert s at index i, shifting characters between ranks
-- i and count rightwards.
-- (ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.appended_string instead of
-- this routine when Current can be of dynamic type STRING and
-- s of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.
-- Note2: There is a bug in ISE 5.4/5.5 when inserting a string
-- to itself.

require
string_not_void: s /= Void
valid_insertion_index: 1 <= i and i <= count + 1
not_current: s /= current_string
ensure
inserted: is_equal (old substring (1, i - 1) + old STRING_.cloned_string (s) + old substring (i, count).current_string)
put (c: CHARACTER; i: INTEGER)

-- Replace character at index i by c.
-- (ELKS 2001 STRING)

require
valid_index: valid_index (i)
ensure
stable_count: count = old count
replaced: item (i) = c
stable_before_i: substring (1, i - 1).is_equal (old substring (1, i - 1))
stable_after_i: substring (i + 1, count).is_equal (old substring (i + 1, count))
replace_substring (s: like Current; start_index, end_index: INTEGER)

-- Note: VE 4.1 has 'like Current' in its signature instead
-- of STRING as specified in ELKS 2001:
-- replace_substring (s: STRING; start_index, end_index: INTEGER) is
-- Replace the substring from start_index to end_index,
-- inclusive, with s.
-- (ELKS 2001 STRING)
-- Note: Use KL_STRING_ROUTINES.replaced_substring instead of
-- this routine when Current can be of dynamic type STRING and
-- s of dynamic type other than STRING such as UC_STRING, because
-- class STRING provided by the Eiffel compilers is not necessarily
-- aware of the implementation of UC_STRING and this may lead to
-- run-time errors or crashes.

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
ensure
replaced: is_equal (old (substring (1, start_index - 1) + s.current_string + substring (end_index + 1, count).current_string))

feature -- Removal

keep_head (n: INTEGER)

-- Remove all the characters except for the first n;
-- if n > count, do nothing.
-- (ELKS 2001 STRING)

require
n_non_negative: n >= 0
ensure
kept: is_equal (old substring (1, n.min (count)))
keep_tail (n: INTEGER)

-- Remove all the characters except for the last n;
-- if n > count, do nothing.
-- (ELKS 2001 STRING)

require
n_non_negative: n >= 0
ensure
kept: is_equal (old substring (count - n.min (count) + 1, count))
remove (i: INTEGER)

-- Remove i-th character, shifting characters between
-- ranks i + 1 and count leftwards.
-- (ELKS 2001 STRING)

require
valid_removal_index: valid_index (i)
ensure
removed: is_equal (old substring (1, i - 1) + old substring (i + 1, count).current_string)
remove_head (n: INTEGER)

-- Remove the first n characters;
-- if n > count, remove all.
-- (ELKS 2001 STRING)

require
n_non_negative: n >= 0
ensure
removed: is_equal (old substring (n.min (count) + 1, count))
remove_substring (start_index, end_index: INTEGER)

-- Remove all characters from start_index
-- to end_index inclusive.
-- (ELKS 2001 STRING)

require
valid_start_index: 1 <= start_index
valid_end_index: end_index <= count
meaningful_interval: start_index <= end_index + 1
ensure
removed: is_equal (old substring (1, start_index - 1) + old substring (end_index + 1, count).current_string)
remove_tail (n: INTEGER)

-- Remove the last n characters;
-- if n > count, remove all.
-- (ELKS 2001 STRING)

require
n_non_negative: n >= 0
ensure
removed: is_equal (old substring (1, count - n.min (count)))
wipe_out

-- Remove all characters.
-- (ELKS 2001 STRING)

ensure
empty_string: count = 0

feature -- Conversion

as_lower: like Current

-- New object with all letters in lower case
-- (Extended from ELKS 2001 STRING)

ensure
as_lower_not_void: Result /= Void
length: Result.count = count
anchor: count > 0 implies Result.item (1) = CHARACTER_.as_lower (item (1))
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_lower)
as_upper: like Current

-- New object with all letters in upper case
-- (Extended from ELKS 2001 STRING)

ensure
as_upper_not_void: Result /= Void
length: Result.count = count
anchor: count > 0 implies Result.item (1) = CHARACTER_.as_upper (item (1))
recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_upper)
to_lower

-- Convert all letters to lower case.
-- (ELKS 2001 STRING)

to_upper

-- Convert all letters to upper case.
-- (ELKS 2001 STRING)

feature -- Duplication

copy (other: like Current)

-- Reinitialize by copying the characters of other.
-- (This is also used by clone.)
-- (ELKS 2001 STRING)

-- (From ANY)

require
other_not_void: other /= Void
type_identity: same_type (other)
ensure
is_equal: is_equal (other)

feature -- Output

out: STRING

-- New STRING containing terse printable representation
-- of current object
-- (ELKS 2001 STRING)

-- (From ANY)

ensure then
out_not_void: Result /= Void
same_items: ANY_.same_types (Current,
) implies Result.same_string (current_string)

feature -- Obsolete

platform_: KL_PLATFORM

-- Platform-dependent properties

-- (From KL_SHARED_PLATFORM)

obsolete

[040101] Use Platform instead.

ensure
platform_not_void: Result /= Void

feature -- Implementation

current_any: ANY

-- Current any

ensure
definition: Result = Current
current_string: STRING

-- Current string

ensure
definition: Result = current_any

invariant

non_negative_count: count >= 0

-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

end