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

kernel.spec.ise

Class UC_STRING


Direct ancestors

KS_STRING, STRING, STRING, COMPARABLE, KI_TEXT_OUTPUT_STREAM, UC_STRING_HANDLER, UC_IMPORTED_UNICODE_ROUTINES, UC_IMPORTED_UTF8_ROUTINES, UC_IMPORTED_UTF16_ROUTINES, KL_IMPORTED_INTEGER_ROUTINES, DEBUG_OUTPUT

Known direct descendants

UC_UTF8_STRING

Creation

Features

Invariants

indexing

description

Unicode strings

remark

Unless specified otherwise, STRING and CHARACTER are %
%supposed to contain characters whose code follows the %
%unicode character set. In other words characters whose %
%code is between 128 and 255 should follow the ISO 8859-1 %
%Latin-1 character set.

remark2

By default UC_STRING is implemented using the UTF-8 encoding. %
%Use UC_UTF*_STRING to specify the encoding explicitly.

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/07/13 17:05:11 $

revision

$Revision: 1.49 $

class

UC_STRING

inherit

KS_STRING
STRING
INDEXABLE
TABLE
BAG
COLLECTION
CONTAINER
RESIZABLE
BOUNDED
FINITE
BOX
CONTAINER
HASHABLE
COMPARABLE
PART_COMPARABLE
TO_SPECIAL
STRING_HANDLER
MISMATCH_CORRECTOR
KI_TEXT_OUTPUT_STREAM
UC_STRING_HANDLER
UC_IMPORTED_UNICODE_ROUTINES
UC_IMPORTED_UTF8_ROUTINES
UC_IMPORTED_UTF16_ROUTINES
KL_IMPORTED_INTEGER_ROUTINES
DEBUG_OUTPUT

create

make (suggested_capacity: INTEGER)

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

-- (From KS_STRING)

require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
empty_string: count = 0
ensure then
byte_count_set: byte_count = 0
byte_capacity_set: byte_capacity >= suggested_capacity
make_empty

-- Create empty string.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

ensure
empty: count = 0
make_from_string (a_string: STRING)

-- Initialize from the character sequence of a_string.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

require
s_not_void: s /= Void
ensure
initialized: same_string (s)
ensure then
same_unicode: same_unicode_string (a_string)
make_from_utf8 (s: STRING)

-- Initialize from the bytes sequence of s corresponding
-- to the UTF-8 representation of a string.

require
s_not_void: s /= Void
s_is_string: ANY_.same_types (s,
)
valid_utf8: utf8.valid_utf8 (s)
make_filled (c: CHARACTER; n: INTEGER)

-- Create string of length n filled with character c.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

require
valid_count: n >= 0
ensure
count_set: count = n
filled: occurrences (c) = count
ensure then
filled_code: code_occurrences (c.code) = count
make_filled_code (a_code: INTEGER; n: INTEGER)

-- Create string of length n filled with unicode
-- character of code a_code.

require
valid_code: unicode.valid_code (a_code)
valid_count: n >= 0
ensure
count_set: count = n
filled: code_occurrences (a_code) = count
make_filled_unicode (c: UC_CHARACTER; n: INTEGER)

-- Create string of length n filled with unicode character c.

require
c_not_void: c /= Void
valid_count: n >= 0
ensure
count_set: count = n
filled: unicode_occurrences (c) = count
make_from_substring (a_string: STRING; start_index, end_index: INTEGER)

-- Initialize from the character sequence of a_string
-- between start_index and end_index inclusive.

require
a_string_not_void: a_string /= Void
valid_start_index: 1 <= start_index
valid_end_index: end_index <= a_string.count
meaningful_interval: start_index <= end_index + 1
make_from_utf16 (s: STRING)

-- Initialize from the bytes sequence of s corresponding
-- to the UTF-16 representation of a string.

require
s_not_void: s /= Void
s_is_string: ANY_.same_types (s,
)
valid_utf16: utf16.valid_utf16 (s)

feature -- Initialization

make (suggested_capacity: INTEGER)

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

-- (From KS_STRING)

require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
empty_string: count = 0
ensure then
byte_count_set: byte_count = 0
byte_capacity_set: byte_capacity >= suggested_capacity
make_from_string (a_string: STRING)

-- Initialize from the character sequence of a_string.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

require
s_not_void: s /= Void
ensure
initialized: same_string (s)
ensure then
same_unicode: same_unicode_string (a_string)

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
integer_: KL_INTEGER_ROUTINES

-- Routines that ought to be in class INTEGER

-- (From KL_IMPORTED_INTEGER_ROUTINES)

ensure
integer_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
area: SPECIAL [CHARACTER]

-- Special data zone

-- (From TO_SPECIAL)

hash_code: INTEGER

-- Hash code
-- (ELKS 2001 STRING)

-- (From KS_HASHABLE)

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

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

-- (From KS_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)
index_of_code (a_code: INTEGER; start_index: INTEGER): INTEGER

-- Index of first occurrence of unicode character with
-- code a_code at or after start_index; 0 if none

require
valid_start_index: start_index >= 1 and start_index <= count + 1
valid_code: unicode.valid_code (a_code)
ensure
valid_result: Result = 0 or (start_index <= Result and Result <= count)
zero_if_absent: (Result = 0) = not substring (start_index, count).has_code (a_code)
found_if_present: substring (start_index, count).has_code (a_code) implies item_code (Result) = a_code
none_before: substring (start_index, count).has_code (a_code) implies not substring (start_index, Result - 1).has_code (a_code)
index_of_unicode (c: UC_CHARACTER; start_index: INTEGER): INTEGER

-- Index of first occurrence of c at or after start_index;
-- 0 if none

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_unicode (c)
found_if_present: substring (start_index, count).has_unicode (c) implies item_code (Result) = c.code
none_before: substring (start_index, count).has_unicode (c) implies not substring (start_index, Result - 1).has_unicode (c)
infix "+" (other: STRING): like Current

-- New object which is a clone of Current extended
-- by the characters of other
-- (ELKS 2001 STRING)

-- (From KS_STRING)

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)
ensure then
final_unicode: Result.substring (count + 1, count + other.count).same_unicode_string (other)
infix "@" (i: INTEGER): CHARACTER

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

-- (From KS_STRING)

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

-- Character at index i;
-- '%U' if the unicode 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 contain characters which may not fit into a CHARACTER.

-- (From KS_STRING)

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

-- (From KS_STRING)

require
valid_index: valid_index (i)
ensure
item_code_positive: Result >= 0
ensure then
valid_item_code: unicode.valid_code (Result)
new_empty_string (suggested_capacity: INTEGER): like Current

-- New empty string with same dynamic type as Current

require
non_negative_suggested_capacity: suggested_capacity >= 0
ensure
new_string_not_void: Result /= Void
same_type: ANY_.same_types (Result, Current)
new_string_empty: Result.count = 0
byte_count_set: Result.byte_count = 0
byte_capacity_set: Result.byte_capacity >= suggested_capacity
prefixed_string (other: STRING): like Current

-- New object which is a clone of Current preceded
-- by the characters of other

require
other_not_void: other /= Void
ensure
prefixed_string_not_void: Result /= Void
prefixed_string_count: Result.count = other.count + count
initial: Result.substring (1, other.count).same_unicode_string (other)
final: Result.substring (other.count + 1, Result.count).is_equal (Current)
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)

-- (From KS_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)

-- (From KS_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)
ensure then
first_unicode_item: Result.count > 0 implies Result.item_code (1) = item_code (start_index)
substring_index (other: STRING; start_index: INTEGER): INTEGER

-- Index of first occurrence of other at or after start_index;
-- 0 if none. other and Current are considered with their
-- characters which do not fit in a CHARACTER replaced by a '%U'
-- (Extended from ELKS 2001 STRING)

-- (From KS_STRING)

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)
unicode: UC_UNICODE_ROUTINES

-- Unicode routines

-- (From UC_IMPORTED_UNICODE_ROUTINES)

ensure
unicode_not_void: Result /= Void
unicode_item (i: INTEGER): UC_CHARACTER

-- Unicode character at index i;
-- Return a new object at each call

require
valid_index: valid_index (i)
ensure
item_not_void: Result /= Void
code_set: Result.code = item_code (i)
unicode_substring_index (other: STRING; start_index: INTEGER): INTEGER

-- Index of first occurrence of other at or after start_index;
-- 0 if none

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_unicode_substring (other)
at_this_index: Result >= start_index implies substring (Result, Result + other.count - 1).same_unicode_string (other)
none_before: Result > start_index implies not substring (start_index, Result + other.count - 2).has_unicode_substring (other)
utf16: UC_UTF16_ROUTINES

-- UTF-16 encoding routines

-- (From UC_IMPORTED_UTF16_ROUTINES)

ensure
utf16_not_void: Result /= Void
utf8: UC_UTF8_ROUTINES

-- UTF-8 encoding routines

-- (From UC_IMPORTED_UTF8_ROUTINES)

ensure
utf8_not_void: Result /= Void

feature -- Measurement

byte_capacity: INTEGER

-- Maximum number of bytes that can be put in
-- internal storage

-- (From BOUNDED)

byte_count: INTEGER

-- Number of bytes in internal storage

code_occurrences (a_code: INTEGER): INTEGER

-- Number of times unicode character of code
-- a_code appears in the string

require
valid_code: unicode.valid_code (a_code)
ensure
zero_if_empty: count = 0 implies Result = 0
recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= a_code) impliesResult = substring (2, count).code_occurrences (a_code)
recurse_if_found_at_first_position: (count > 0 and then item_code (1) = a_code) impliesResult = 1 + substring (2, count).code_occurrences (a_code)
count: INTEGER

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

-- (From KS_STRING)

occurrences (c: CHARACTER): INTEGER

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

-- (From KS_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)
unicode_occurrences (c: UC_CHARACTER): INTEGER

-- Number of times c appears in the string

require
c_not_void: c /= Void
ensure
zero_if_empty: count = 0 implies Result = 0
recurse_if_not_found_at_first_position: (count > 0 and then item_code (1) /= c.code) impliesResult = substring (2, count).unicode_occurrences (c)
recurse_if_found_at_first_position: (count > 0 and then item_code (1) = c.code) impliesResult = 1 + substring (2, count).unicode_occurrences (c)

feature -- Comparison

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

-- Is string lexicographically lower than other?
-- (Extended from ELKS 2001 STRING, inherited from COMPARABLE)

-- (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)))
ensure then
unicode_definition: Result = (count = 0 and other.count > 0 orcount > 0 and then other.count > 0 and then (item_code (1) < other.item_code (1) oritem_code (1) = other.item_code (1) and substring (2, count) < other.substring (2, other.count)))
infix "<=" (other: like Current): BOOLEAN

-- Is current object less than or equal to other?

-- (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?

-- (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?

-- (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)))))))
ensure then
unicode_definition: Result = (ANY_.same_types (Current, other) and then count = other.count and then(count > 0 implies (item_code (1) = other.item_code (1) andsubstring (2, count).is_equal (other.substring (2, count)))))
max (other: like Current): like Current

-- The greater of current object and other

-- (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

-- (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)

-- (From KS_STRING)

require
other_not_void: other /= Void
ensure
definition: Result = string.is_equal (other.string)
same_unicode_string (other: STRING): BOOLEAN

-- Do Current and other have the same unicode character sequence?

require
other_not_void: other /= Void
ensure
definition: Result = (count = other.count and then(count > 0 implies (item_code (1) = other.item_code (1) and(count >= 2 implies substring (2, count).same_unicode_string (other.substring (2, count))))))
same_string: Result implies same_string (other)
three_way_comparison (other: like Current): INTEGER

-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
-- (ELKS 2001 STRING, inherited from COMPARABLE)
-- Note: there is a bug in the specification of the
-- contracts of three_way_comparison inherited
-- from COMPARABLE. This routine cannot satisfy
-- its postconditions if other is not of the
-- same type as Current because the postcondition
-- uses is_equal and is_equal has a postcondition
-- inherited from ANY which says if it returns true
-- then other has the same type as Current.

-- (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)
three_way_unicode_comparison (other: STRING): INTEGER

-- If current object equal to other, 0;
-- if smaller, -1; if greater, 1
-- Note: there is a bug in the specification of the
-- contracts of three_way_comparison inherited
-- from COMPARABLE. This routine cannot satisfy
-- its postconditions if other is not of the
-- same type as Current because the postcondition
-- uses is_equal and is_equal has a postcondition
-- inherited from ANY which says if it returns true
-- then other has the same type as Current.
-- three_way_unicode_comparison solves this problem
-- and make the comparison polymorphically safe by
-- changing the signature from 'like Current' to
-- 'STRING' and by using same_unicode_string instead
-- of is_equal in its postcondition.

require
other_not_void: other /= Void
ensure
equal_zero: (Result = 0) = same_unicode_string (other)

feature -- Status report

has (c: CHARACTER): BOOLEAN

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

-- (From KS_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_code (a_code: INTEGER): BOOLEAN

-- Does Current contain the unicode character of code a_code?

require
valid_code: unicode.valid_code (a_code)
ensure
false_if_empty: count = 0 implies not Result
true_if_first: count > 0 and then item_code (1) = a_code implies Result
recurse: (count > 0 and then item_code (1) /= a_code) implies (Result = substring (2, count).has_code (a_code))
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)

-- (From KS_STRING)

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))
has_unicode (c: UC_CHARACTER): BOOLEAN

-- Does Current contain c?

require
c_not_void: c /= Void
ensure
false_if_empty: count = 0 implies not Result
true_if_first: count > 0 and then item_code (1) = c.code implies Result
recurse: (count > 0 and then item_code (1) /= c.code) implies (Result = substring (2, count).has_unicode (c))
has_unicode_substring (other: STRING): BOOLEAN

-- Does Current contain other?

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 substring (1, other.count).same_unicode_string (other)) implies Result
recurse: (count >= other.count and then not substring (1, other.count).same_unicode_string (other)) implies (Result = substring (2, count).has_unicode_substring (other))
has_substring: Result implies has_substring (other)
is_ascii: BOOLEAN

-- Does string contain only ASCII characters?

ensure
empty: count = 0 implies Result
recurse: count > 0 implies Result = (unicode_item (1).is_ascii and substring (2, count).is_ascii)
is_closable: BOOLEAN

-- Can current output stream be closed?

-- (From KI_OUTPUT_STREAM)

ensure
is_open: Result implies is_open_write
is_empty: BOOLEAN

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

-- (From KS_STRING)

ensure
definition: Result = (count = 0)
old_is_empty: BOOLEAN

-- Is structure empty?

-- (From CONTAINER)

valid_index (i: INTEGER): BOOLEAN

-- Is i within the bounds of the string?

-- (From KS_STRING)

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

feature -- Element change

append_character (c: CHARACTER)

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

-- (From KS_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))
ensure then
unicode_appended: item_code (count) = c.code
append_code (a_code: INTEGER)

-- Append unicode character of code a_code at end.

require
valid_item_code: unicode.valid_code (a_code)
ensure
new_count: count = old count + 1
appended: item_code (count) = a_code
stable_before: substring (1, count - 1).is_equal (old cloned_string)
append_string (a_string: STRING)

-- Append a copy of a_string at end.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

require
s_not_void: s /= Void
ensure
append_substring (a_string: STRING; s, e: INTEGER)

-- Append substring of a_string between indexes
-- s and e at end of current string.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
s_large_enough: s >= 1
e_small_enough: e <= a_string.count
valid_interval: s <= e + 1
ensure then
appended: is_equal (old cloned_string + old a_string.substring (s, e))
append_unicode_character (c: UC_CHARACTER)

-- Append unicode character c at end.

require
c_not_void: c /= Void
ensure
new_count: count = old count + 1
appended: item_code (count) = c.code
stable_before: substring (1, count - 1).is_equal (old cloned_string)
append_utf16 (s: STRING)

-- Append UTF-16 encoded string s at end of current string.

require
s_not_void: s /= Void
s_is_string: ANY_.same_types (s,
)
valid_utf16: utf16.valid_utf16 (s)
append_utf8 (s: STRING)

-- Append UTF-8 encoded string s at end of current string.

require
s_not_void: s /= Void
s_is_string: ANY_.same_types (s,
)
valid_utf8: utf8.valid_utf8 (s)
fill_with (c: CHARACTER)

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

-- (From KS_STRING)

ensure
same_count: old count = count
filled: occurrences (c) = count
ensure then
all_code: code_occurrences (c.code) = count
fill_with_code (a_code: INTEGER)

-- Replace every character with unicode character of code a_code.

require
valid_code: unicode.valid_code (a_code)
ensure
same_count: old count = count
filled: code_occurrences (a_code) = count
fill_with_unicode (c: UC_CHARACTER)

-- Replace every character with unicode character c.

require
c_not_void: c /= Void
ensure
same_count: old count = count
filled: unicode_occurrences (c) = count
insert_character (c: CHARACTER; i: INTEGER)

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

-- (From KS_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))
ensure then
code_inserted: item_code (i) = c.code
insert_code (a_code: INTEGER; i: INTEGER)

-- Insert unicode character of code a_code
-- at index i, shifting characters between
-- ranks i and count rightwards.

require
valid_code: unicode.valid_code (a_code)
valid_insertion_index: 1 <= i and i <= count + 1
ensure
one_more_character: count = old count + 1
inserted: item_code (i) = a_code
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 (a_string: STRING; i: INTEGER)

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

-- (From KS_STRING)

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

-- Insert unicode character c at index i, shifting
-- characters between ranks i and count rightwards.

require
c_not_void: c /= Void
valid_insertion_index: 1 <= i and i <= count + 1
ensure
one_more_character: count = old count + 1
inserted: item_code (i) = c.code
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))
put (c: CHARACTER; i: INTEGER)

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

-- (From KS_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))
ensure then
unicode_replaced: item_code (i) = c.code
put_code (a_code: INTEGER; i: INTEGER)

-- Replace unicode character at index i
-- by unicode character of code a_code.

require
valid_index: valid_index (i)
valid_item_code: unicode.valid_code (a_code)
ensure
stable_count: count = old count
replaced: item_code (i) = a_code
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))
put_unicode (c: UC_CHARACTER; i: INTEGER)

-- Replace unicode character at index i by c.

require
valid_index: valid_index (i)
c_not_void: c /= Void
ensure
stable_count: count = old count
replaced: item_code (i) = c.code
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 (a_string: 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 (a_string: STRING; start_index, end_index: INTEGER) is
-- Replace the substring from start_index to end_index,
-- inclusive, with a_string.
-- (ELKS 2001 STRING)

-- (From KS_STRING)

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))
replace_substring_by_string (a_string: STRING; start_index, end_index: INTEGER)

-- Replace the substring from start_index to end_index,
-- inclusive, with a_string.

share (other: STRING)

-- Make current string share the text of other.
-- Subsequent changes to the characters of current string
-- will also affect other, and conversely.

-- (From STRING)

require
argument_not_void: other /= Void
ensure
shared_count: other.count = count
shared_area: other.area = area

feature -- Removal

keep_head (n: INTEGER)

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

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)

-- (From KS_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)
ensure then
unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_lower)
unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_lower)
as_string: STRING

-- STRING version of current string;
-- Return the UTF8 representation if it is encoded
-- with UTF8, the UTF16 representation if it is
-- encoded with UTF16, etc.

ensure
as_string_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
as_upper: like Current

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

-- (From KS_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)
ensure then
unicode_anchor: count > 0 implies Result.unicode_item (1).is_equal (unicode_item (1).as_upper)
unicode_recurse: count > 1 implies Result.substring (2, count).is_equal (substring (2, count).as_upper)
mirror

-- Reverse the order of characters.
-- "Hello world" -> "dlrow olleH".

-- (From STRING)

ensure
same_count: count = old count
to_lower

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

-- (From KS_STRING)

to_upper

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

-- (From KS_STRING)

to_utf8: STRING

-- New STRING made up of bytes corresponding to
-- the UTF-8 representation of current string

ensure
to_utf8_not_void: Result /= Void
string_type: ANY_.same_types (Result,
)
valid_utf8: utf8.valid_utf8 (Result)

feature -- Duplication

cloned_string: like Current

-- New object equal to Current

ensure
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
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 -- Basic operations

close

-- Try to close output stream if it is closable. Set
-- is_open_write to false if operation was successful.

-- (From KI_OUTPUT_STREAM)

require
is_closable: is_closable

feature -- Output stream

eol: STRING

-- Line separator

-- (From KI_TEXT_OUTPUT_STREAM)

ensure
eol_not_void: Result /= Void
eol_not_empty: Result.count > 0
flush

-- Do nothing (operation does not apply to string).

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
is_open_write: BOOLEAN

-- Can characters be written to output stream?

-- (From KI_OUTPUT_STREAM)

name: STRING

-- Name of output stream

-- (From KI_OUTPUT_STREAM)

ensure
name_not_void: Result /= Void

feature {UC_STRING} -- Byte index cache

last_byte_index_input: INTEGER

-- Last byte_index requested
-- (Cache for 'i := i + 1' iterations and similar)

last_byte_index_result: INTEGER

-- Last byte_index Result
-- (Cache for 'i := i + 1' iterations and similar)

reset_byte_index_cache

-- Reset byte index (after write operation for example).

feature -- Output

append_stream (an_input_stream: KI_INPUT_STREAM [CHARACTER])

-- Read items of an_input_stream until the end
-- of input is reached, and write these items to
-- current output stream.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
an_input_stream_not_void: an_input_stream /= Void
an_input_stream_open_read: an_input_stream.is_open_read
ensure
end_of_input: an_input_stream.end_of_input
debug_output: STRING

-- String that should be displayed in debugger to represent Current.

-- (From DEBUG_OUTPUT)

ensure
result_not_void: Result /= Void
out: STRING

-- New STRING containing terse printable representation
-- of current object; Non-ascii characters are represented
-- with the %/code/ convention.
-- (ELKS 2001 STRING)

-- (From ANY)

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

-- Write "True" to output stream if
-- b is true, "False" otherwise.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_integer (i: INTEGER)

-- Write decimal representation
-- of i to output stream.
-- Regexp: 0|(-?[1-9][0-9]*)

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_line (a_string: STRING)

-- Write a_string to output stream
-- followed by a line separator.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
put_new_line

-- Write a line separator to output stream.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write

feature -- Traversal

byte_index (i: INTEGER): INTEGER

-- Byte index of character at index i

require
valid_index: valid_index (i)
ensure
byte_index_large_enough: Result >= 1
byte_index_small_enough: Result <= byte_count
is_encoded_first_byte: is_encoded_first_byte (Result)
character_item_at_byte_index (i: INTEGER): CHARACTER

-- Character at byte_index i;
-- '%U' is the unicode character at byte index
-- i cannot fit into a CHARACTER

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
is_encoded_first_byte: is_encoded_first_byte (i)
ensure
code_small_enough: item_code_at_byte_index (i) <= Platform.Maximum_character_code implies Result.code = item_code_at_byte_index (i)
overflow: item_code_at_byte_index (i) > Platform.Maximum_character_code implies Result = '%U'
is_encoded_first_byte (i: INTEGER): BOOLEAN

-- Is byte at index i the first byte of an encoded unicode character?

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
item_code_at_byte_index (i: INTEGER): INTEGER

-- Code of character at byte index i

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
is_encoded_first_byte: is_encoded_first_byte (i)
ensure
valid_item_code: unicode.valid_code (Result)
next_byte_index (i: INTEGER): INTEGER

-- Byte index of unicode character after character
-- at byte index i; Return 'byte_count + 1' if
-- character at byte index i is the last character
-- in the string

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
is_encoded_first_byte: is_encoded_first_byte (i)
ensure
next_byte_index_large_enough: Result > i
next_byte_index_small_enough: Result <= byte_count + 1
shifted_byte_index (i: INTEGER; n: INTEGER): INTEGER

-- Byte index of unicode character n positions after
-- character at byte index i; Return 'byte_count + 1'
-- if no such character in the string

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
is_encoded_first_byte: is_encoded_first_byte (i)
n_positive: n >= 0
ensure
next_byte_index_large_enough: Result >= i
next_byte_index_small_enough: Result <= byte_count + 1

feature -- Obsolete

append_uc_character (c: UC_CHARACTER)

-- Append unicode character c at end.

obsolete

[020720] Use append_unicode_character instead.

require
c_not_void: c /= Void
append_uc_string (a_string: UC_STRING)

-- Append a copy of a_string at end.

obsolete

[011225] Use append_string instead.

require
a_string_not_void: a_string /= Void
append_unicode (c: UC_CHARACTER)

-- Append unicode character c at end.

obsolete

[020720] Use append_unicode_character instead.

require
c_not_void: c /= Void
empty: BOOLEAN

-- Is string empty?

obsolete

[011225] Use is_empty instead.

head (n: INTEGER)

-- Remove all the characters except for the first n;
-- if n > count, do nothing.

-- (From STRING)

obsolete

[020602] Use keep_head instead.

require
non_negative_argument: n >= 0
ensure
new_count: count = n.min (old count)
kept: elks_checking implies is_equal (old substring (1, n.min (count)))
insert_unicode (c: UC_CHARACTER; i: INTEGER)

-- Insert unicode character c at index i, shifting
-- characters between ranks i and count rightwards.

obsolete

[020720] Use insert_unicode_character instead.

require
c_not_void: c /= Void
valid_insertion_index: 1 <= i and i <= count + 1
ensure
one_more_character: count = old count + 1
inserted: item_code (i) = c.code
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))
platform_: KL_PLATFORM

-- Platform-dependent properties

-- (From KL_SHARED_PLATFORM)

obsolete

[040101] Use Platform instead.

ensure
platform_not_void: Result /= Void
tail (n: INTEGER)

-- Remove all the characters except for the last n;
-- if n > count, do nothing.

-- (From STRING)

obsolete

[020602] Use keep_tail instead.

require
non_negative_argument: n >= 0
ensure
new_count: count = n.min (old count)
kept: elks_checking implies is_equal (old substring (count - n.min(count) + 1, count))

feature {UC_STRING_HANDLER} -- Implementation

byte_item (i: INTEGER): CHARACTER

-- Byte at index i

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
current_any: ANY

-- Current any

-- (From KS_STRING)

ensure
definition: Result = Current
current_string: STRING

-- Current string

-- (From KS_STRING)

ensure
definition: Result = current_any
move_bytes_left (i, offset: INTEGER)

-- Move bytes at and after position i
-- by offset positions to the left.

require
valid_index: 1 <= i and i <= byte_count + 1
positive_offset: offset >= 0
constraint: offset < i
ensure
byte_count_set: byte_count = old byte_count - offset
move_bytes_right (i, offset: INTEGER)

-- Move bytes at and after position i
-- by offset positions to the right.

require
valid_index: 1 <= i and i <= byte_count + 1
positive_offset: offset >= 0
offset_small_enough: offset <= (byte_capacity - byte_count)
ensure
byte_count_set: byte_count = old byte_count + offset
put_byte (c: CHARACTER; i: INTEGER)

-- Replace byte at index i by c.

require
i_large_enough: i >= 1
i_small_enough: i <= byte_count
resize_byte_storage (n: INTEGER)

-- Resize space for n bytes.
-- Do not lose previously stored bytes.

require
n_large_enough: n >= byte_capacity
ensure
byte_capacity_set: byte_capacity = n
set_byte_count (nb: INTEGER)

-- Set byte_count to nb.

require
nb_large_enough: nb >= 0
nb_small_enough: nb <= byte_capacity
ensure
byte_count_set: byte_count = nb
set_count (nb: INTEGER)

-- Set count to nb.

require
nb_positive: nb >= 0
ensure
count_set: count = nb

invariant

non_negative_byte_count: byte_count >= 0
byte_count_small_enough: byte_count <= byte_capacity
count_small_enough: count <= byte_count

-- From KS_STRING
non_negative_count: count >= 0

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


-- From STRING
extendible: extendible
compare_character: not object_comparison
index_set_has_same_count: index_set.count = count
area_not_void: area /= Void

-- From INDEXABLE
index_set_not_void: index_set /= Void

-- 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: is_empty = (count = 0)
non_negative_count: count >= 0

-- From COMPARABLE
irreflexive_comparison: not (Current < Current)

end