class interface UNICODE_STRING
--
-- WARNING: THIS CLASS IS A WORK IN PROGRESS. SOME FEATURE ARE NOT
-- YET IMPLEMENTED AND SOME FEATURE MAY APPEAR/DISAPPEAR.
--
-- A UNICODE_STRING is a resizable string written with unicode values.
-- From unicode.org: "Unicode provides a unique number for every
-- character ,
-- no matter what the platform,
-- no matter what the program,
-- no matter what the language.
--
-- WARNING: a grapheme may be described with many code.
-- grapheme may be defined as "user character". Angstrom sign is
-- one grapheme but may be defined using (LETTER A + COMBINING RING).
-- Unicode strings may be acceded in two ways:
-- - low-level (code by code)
-- - high-level (grapheme by grapheme)
--
-- Unless otherwise specified, all functions unit is the unicode number.
--
creation
make (needed_capacity: INTEGER)
-- Initialize the string to have at least needed_capacity
-- characters of storage.
require
non_negative_size: needed_capacity >= 0
ensure
needed_capacity <= capacity;
empty_string: count = 0
copy (other: like Current)
-- Copy other onto Current.
require
standard_same_dynamic_type(other)
ensure
count = other.count;
is_equal(other)
make_empty
-- Create an empty string.
make_filled (unicode: INTEGER; n: INTEGER)
-- Initialize string with n copies of unicode.
require
valid_count: n >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count_set: count = n;
filled: occurrences(unicode) = count
from_utf8 (s: STRING)
-- Use s as UTF-8 format encoded unicode string
-- This function may be used for manifest strings
-- See utf8_decode_from for error detection
require
s /= Void
feature(s) from HASHABLE
hash_code: INTEGER
-- The hash-code value of Current.
ensure
good_hash_value: Result >= 0
feature(s) from COMPARABLE
is_equal (other: like Current): BOOLEAN
-- Do both strings have the same character sequence?
-- (Redefined from GENERAL)
require
other /= Void
ensure
trichotomy: Result = (not (Current < other) and not (other < Current));
same_dynamic_type(other) implies Result = other.is_equal(Current)
infix "<" (other: like Current): BOOLEAN
-- Is Current less than other?
require
other_exists: other /= Void
ensure
asymmetric: Result implies not (other < Current)
infix "<=" (other: like Current): BOOLEAN
-- Is Current less than or equal other?
require
other_exists: other /= Void
ensure
definition: Result = (Current < other or is_equal(other))
infix ">" (other: like Current): BOOLEAN
-- Is Current strictly greater than other?
require
other_exists: other /= Void
ensure
definition: Result = (other < Current)
infix ">=" (other: like Current): BOOLEAN
-- Is Current greater than or equal than other?
require
other_exists: other /= Void
ensure
definition: Result = (other <= Current)
in_range (lower, upper: like Current): BOOLEAN
-- Return true if Current is in range [lower..upper]
ensure
Result = (Current >= lower and Current <= upper)
compare (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
three_way_comparison (other: like Current): INTEGER
-- If current object equal to other, 0
-- if smaller, -1; if greater, 1.
require
other_exists: other /= Void
ensure
equal_zero: Result = 0 = is_equal(other);
smaller_negative: Result = -1 = (Current < other);
greater_positive: Result = 1 = (Current > other)
min (other: like Current): like Current
-- Minimum of Current and other.
require
other /= Void
ensure
Result <= Current and then Result <= other;
compare(Result) = 0 or else other.compare(Result) = 0
max (other: like Current): like Current
-- Maximum of Current and other.
require
other /= Void
ensure
Result >= Current and then Result >= other;
compare(Result) = 0 or else other.compare(Result) = 0
feature(s) from UNICODE_STRING
count: INTEGER
-- String length which is also the maximum valid index.
capacity: INTEGER
-- Capacity of the storage area.
lower: INTEGER
-- Minimum index; actually, this is always 1 (this feature is
-- here to mimic the one of the COLLECTIONs hierarchy).
upper: INTEGER
-- Maximum index; actually the same value as count (this
-- feature is here to mimic the one of the COLLECTION hierarchy).
ensure
Result = count
feature(s) from UNICODE_STRING
-- Creation / Modification:
make (needed_capacity: INTEGER)
-- Initialize the string to have at least needed_capacity
-- characters of storage.
require
non_negative_size: needed_capacity >= 0
ensure
needed_capacity <= capacity;
empty_string: count = 0
make_empty
-- Create an empty string.
make_filled (unicode: INTEGER; n: INTEGER)
-- Initialize string with n copies of unicode.
require
valid_count: n >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count_set: count = n;
filled: occurrences(unicode) = count
feature(s) from UNICODE_STRING
-- Testing:
is_empty: BOOLEAN
-- Has string length 0?
item (i: INTEGER): INTEGER
-- Get unicode at position i.
require
valid_index: valid_index(i)
infix "@" (i: INTEGER): INTEGER
-- Get unicode at position i.
require
valid_index: valid_index(i)
valid_index (i: INTEGER): BOOLEAN
-- True when i is valid (i.e., inside actual bounds).
ensure
definition: Result = (1 <= i and i <= count)
same_as (other: UNICODE_STRING): BOOLEAN
-- Case insensitive is_equal.
require
other /= Void
index_of (unicode: INTEGER; start_index: INTEGER): INTEGER
-- Index of first occurrence of unicode at or after start_index,
-- 0 if none.
--
-- Note: see also first_index_of to start searching at 1.
require
valid_start_index: start_index >= 1 and start_index <= count + 1;
valid_unicode_value: valid_unicode(unicode)
ensure
Result /= 0 implies item(Result) = unicode
reverse_index_of (unicode: INTEGER; start_index: INTEGER): INTEGER
-- Index of first occurrence of unicode at or before start_index,
-- 0 if none.
--
-- Note: search is done in reverse direction, which means
-- from the index down to the first character.
require
valid_start_index: start_index >= 0 and start_index <= count;
valid_unicode_value: valid_unicode(unicode)
ensure
Result /= 0 implies item(Result) = unicode
first_index_of (unicode: INTEGER): INTEGER
-- Index of first occurrence of unicode at index 1 or after index 1.
require
valid_unicode_value: valid_unicode(unicode)
ensure
definition: Result = index_of(unicode,1)
has (unicode: INTEGER): BOOLEAN
-- True if unicode is in the STRING.
require
valid_unicode_value: valid_unicode(unicode)
has_substring (other: UNICODE_STRING): BOOLEAN
-- True if Current contains other.
require
other_not_void: other /= Void
occurrences (unicode: INTEGER): INTEGER
-- Number of times character unicode appears in the string.
require
valid_unicode_value: valid_unicode(unicode)
ensure
Result >= 0
has_suffix (s: UNICODE_STRING): BOOLEAN
-- True if suffix of Current is s.
require
s /= Void
has_prefix (p: UNICODE_STRING): BOOLEAN
-- True if prefix of Current is p.
require
p /= Void
feature(s) from UNICODE_STRING
-- Testing and Conversion:
is_ascii: BOOLEAN
-- True if all unicode value is in range 0..127
to_utf8: STRING
-- New string is created, current unicode string is encoded
-- with UTF-8 format.
-- Note: see also utf8_encode_in to save memory.
to_string: STRING
-- New string is created, current unicode string is encoded
-- with UTF-8 format.
-- Note: see also utf8_encode_in to save memory.
utf8_encode_in (s: STRING)
-- append current unicode string in s with UTF-8 format
require
s /= Void
utf16be_encode_in (s: STRING)
-- append current unicode string in s with UTF-16BE format
require
s /= Void
utf8_decode_from (s: STRING): BOOLEAN
-- Use s as UTF-8 format encoded unicode string
-- Return False if decoding process failed
require
s /= Void
feature(s) from UNICODE_STRING
-- Modification:
resize (new_count: INTEGER)
-- Resize Current. When new_count is greater than
-- count, new positions are initialized with unicode 0.
require
new_count >= 0
ensure
count = new_count;
capacity >= old capacity
clear
-- Clear out the current STRING.
-- Note: internal storage memory is neither released nor shrunk.
ensure
count = 0
wipe_out
-- Clear out the current STRING.
-- Note: internal storage memory is neither released nor shrunk.
ensure
count = 0
copy (other: like Current)
-- Copy other onto Current.
require
standard_same_dynamic_type(other)
ensure
count = other.count;
is_equal(other)
fill_with (unicode: INTEGER)
-- Replace every unicode with the new value.
require
valid_unicode_value: valid_unicode(unicode)
ensure
occurrences(unicode) = count
replace_all (old_code, new_code: like item)
-- Replace all occurrences of the element old_code by
-- new_code.
ensure
count = old count;
occurrences(old_code) = 0
append (s: UNICODE_STRING)
-- Append a copy of 's' to Current.
require
s_not_void: s /= Void
append_string (s: UNICODE_STRING)
-- Append a copy of 's' to Current.
require
s_not_void: s /= Void
prepend (other: UNICODE_STRING)
-- Prepend other to Current.
require
other /= Void
ensure
Current.is_equal(old other.twin + old Current.twin)
insert_string (s: UNICODE_STRING; i: INTEGER)
-- Insert s at index i, shifting characters from index i
-- to count rightwards.
require
string_not_void: s /= Void;
valid_insertion_index: 1 <= i and i <= count + 1
replace_substring (s: UNICODE_STRING; start_index, end_index: INTEGER)
-- Replace the substring from start_index to end_index,
-- inclusive, with s.
require
string_not_void: s /= Void;
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
infix "+" (other: UNICODE_STRING): like Current
-- Create a new UNICODE_STRING which is the concatenation of
-- Current and other.
require
other_exists: other /= Void
ensure
result_count: Result.count = count + other.count
put (unicode: INTEGER; i: INTEGER)
-- Put unicode at position i.
require
valid_index: valid_index(i);
valid_unicode_value: valid_unicode(unicode)
ensure
item(i) = unicode
swap (i1, i2: INTEGER)
require
valid_index(i1);
valid_index(i2)
ensure
item(i1) = old item(i2);
item(i2) = old item(i1)
insert_character (unicode: INTEGER; i: INTEGER)
-- Inserts unicode at index i, shifting characters from
-- position 'i' to count rightwards.
require
valid_insertion_index: 1 <= i and i <= count + 1;
valid_unicode_value: valid_unicode(unicode)
ensure
item(i) = unicode
shrink (min_index, max_index: INTEGER)
-- Keep only the slice [min_index .. max_index] or nothing
-- when the slice is empty.
require
1 <= min_index;
max_index <= count;
min_index <= max_index + 1
ensure
count = max_index - min_index + 1
remove (i: INTEGER)
-- Remove character at position i.
require
valid_removal_index: valid_index(i)
ensure
count = old count - 1
add_first (unicode: INTEGER)
-- Add unicode at first position.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = 1 + old count;
item(1) = unicode
precede (unicode: INTEGER)
-- Add unicode at first position.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = 1 + old count;
item(1) = unicode
add_last (unicode: INTEGER)
-- Append unicode to string.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = 1 + old count;
item(count) = unicode
append_character (unicode: INTEGER)
-- Append unicode to string.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = 1 + old count;
item(count) = unicode
extend (unicode: INTEGER)
-- Append unicode to string.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = 1 + old count;
item(count) = unicode
to_lower
-- Convert the string to lower case.
to_upper
-- Convert the string to upper case.
as_lower: like Current
-- New object in lower case.
as_upper: like Current
-- New object in upper case.
keep_head (n: INTEGER)
-- Remove all characters except for the first n.
-- Do nothing if n >= count.
require
n_non_negative: n >= 0
ensure
count = n.min(old count)
keep_tail (n: INTEGER)
-- Remove all characters except for the last n.
-- Do nothing if n >= count.
require
n_non_negative: n >= 0
ensure
count = n.min(old count)
remove_head (n: INTEGER)
-- Remove n first characters.
-- If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_first (n: INTEGER)
-- Remove n first characters.
-- If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_tail (n: INTEGER)
-- Remove n last characters.
-- If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_last (n: INTEGER)
-- Remove n last characters.
-- If n >= count, remove all.
require
n_non_negative: n >= 0
ensure
count = (0).max(old count - n)
remove_substring (start_index, end_index: INTEGER)
-- Remove all characters from strt_index to end_index inclusive.
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
count = old count - (end_index - start_index + 1)
remove_between (start_index, end_index: INTEGER)
-- Remove all characters from strt_index to end_index inclusive.
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
count = old count - (end_index - start_index + 1)
remove_suffix (s: UNICODE_STRING)
-- Remove the suffix s of current string.
require
has_suffix(s)
ensure
(old Current.twin).is_equal(Current + old s.twin)
remove_prefix (s: UNICODE_STRING)
-- Remove the prefix s of current string.
require
has_prefix(s)
ensure
(old Current.twin).is_equal(old s.twin + Current)
left_adjust
-- Remove leading blanks.
ensure
-- not_yet_implemented -- handle combining characters
stripped: is_empty or else not is_space(item(1))
right_adjust
-- Remove trailing blanks.
ensure
-- not_yet_implemented -- handle combining characters
stripped: is_empty or else not is_space(item(count))
feature(s) from UNICODE_STRING
-- Printing:
out_in_tagged_out_memory
-- Append terse printable represention of current object
-- in tagged_out_memory.
ensure
not_cleared: tagged_out_memory.count >= old tagged_out_memory.count;
append_only: (old tagged_out_memory.twin).is_equal(tagged_out_memory.substring(1,old tagged_out_memory.count))
fill_tagged_out_memory
-- Append a viewable information in tagged_out_memory in
-- order to affect the behavior of out, tagged_out, etc.
feature(s) from UNICODE_STRING
-- Agents based features:
do_all (action: ROUTINE[ANY,TUPLE[INTEGER]])
-- Apply action to every item of Current.
for_all (test: PREDICATE[ANY,TUPLE[INTEGER]]): BOOLEAN
-- Do all items satisfy test?
exists (test: PREDICATE[ANY,TUPLE[INTEGER]]): BOOLEAN
-- Does at least one item satisfy test?
feature(s) from UNICODE_STRING
-- Other features:
first: INTEGER
-- Access to the very first character.
require
not is_empty
ensure
definition: Result = item(1)
last: INTEGER
-- Access to the very last character.
require
not is_empty
ensure
definition: Result = item(count)
substring (start_index, end_index: INTEGER): like Current
-- New string consisting of items [start_index.. end_index].
require
valid_start_index: 1 <= start_index;
valid_end_index: end_index <= count;
meaningful_interval: start_index <= end_index + 1
ensure
substring_count: Result.count = end_index - start_index + 1
extend_multiple (unicode: INTEGER; n: INTEGER)
-- Extend Current with n times character unicode.
require
n >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count = n + old count
precede_multiple (unicode: INTEGER; n: INTEGER)
-- Prepend n times character unicode to Current.
require
n >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count = n + old count
extend_to_count (unicode: INTEGER; needed_count: INTEGER)
-- Extend Current with unicode until needed_count is reached.
-- Do nothing if needed_count is already greater or equal
-- to count.
require
needed_count >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count >= needed_count
precede_to_count (unicode: INTEGER; needed_count: INTEGER)
-- Prepend unicode to Current until needed_count is reached.
-- Do nothing if needed_count is already greater or equal
-- to count.
require
needed_count >= 0;
valid_unicode_value: valid_unicode(unicode)
ensure
count >= needed_count
reverse
-- Reverse the string.
remove_all_occurrences (unicode: INTEGER)
-- Remove all occurrences of unicode.
require
valid_unicode_value: valid_unicode(unicode)
ensure
count = old count - old occurrences(unicode)
substring_index (other: UNICODE_STRING; start_index: INTEGER): INTEGER
-- Position of first occurrence of other at or after start;
-- 0 if none.
require
other_not_void: other /= Void;
valid_start_index: start_index >= 1 and start_index <= count + 1
first_substring_index (other: UNICODE_STRING): INTEGER
-- Position of first occurrence of other at or after 1;
-- 0 if none.
require
other_not_void: other /= Void
ensure
definition: Result = substring_index(other,1)
feature(s) from UNICODE_STRING
-- Splitting a STRING:
split: ARRAY[UNICODE_STRING]
-- Split the string into an array of words. Uses is_separator
-- to find words. Gives Void or a non empty array.
ensure
Result /= Void implies not Result.is_empty
split_in (words: COLLECTION[UNICODE_STRING])
-- Same jobs as split but result is appended in words.
require
words /= Void
ensure
words.count >= old words.count
feature(s) from UNICODE_STRING
-- Other features:
extend_unless (unicode: INTEGER)
-- Extend Current (using extend) with unicode unless
-- unicode ch is already the last character.
require
valid_unicode_value: valid_unicode(unicode)
ensure
last = unicode;
count >= old count
get_new_iterator: ITERATOR[INTEGER]
valid_unicode (unicode: INTEGER): BOOLEAN
is_space (unicode: INTEGER): BOOLEAN
is_separator (unicode: INTEGER): BOOLEAN
is_combining (unicode: INTEGER): BOOLEAN
feature(s)
invariant
0 <= count;
count <= capacity;
capacity > 0 implies storage.is_not_null;
low_surrogate_values.count = low_surrogate_indexes.count;
valid_surrogates;
end of UNICODE_STRING