class UNICODE_STRING

Features exported to ANY

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.

Direct parents

conformant parents

COMPARABLE, HASHABLE, TRAVERSABLE

Summary

creation features

exported features

Creation / Modification:

Testing:

Testing and Conversion:

Modification:

Printing:

Agents based features:

Other features:

Splitting a STRING:

Other features:

Indexing:

Details

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: UNICODE_STRING)

Copy other onto Current.

require

  • 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

count: INTEGER

String length which is also the maximum valid index.

ensure

  • definition: Result = upper - lower + 1

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

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

is_empty: BOOLEAN

Has string length 0?

ensure

  • definition: Result = (count = 0)

item (i: INTEGER): INTEGER

Get unicode at position i.

require

  • valid_index(i)

@ (i: INTEGER): INTEGER

The infix notation which is actually just a synonym for item.

require

  • valid_index(i)

ensure

  • definition: Result = item(i)

hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

< (other: UNICODE_STRING): BOOLEAN

Is Current less than other?

require

  • other_exists: other /= Void

ensure

  • asymmetric: Result implies not (other < Current)

compare (other: UNICODE_STRING): INTEGER

If current object equal to other, 0 if smaller, -1; if greater, 1.

See also min, max, in_range.

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: UNICODE_STRING): INTEGER

If current object equal to other, 0 if smaller, -1; if greater, 1.

See also min, max, in_range.

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)

is_equal (other: UNICODE_STRING): BOOLEAN

Do both strings have the same character sequence?

require

  • other /= Void

ensure

  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
  • trichotomy: Result = (not (Current < other) and not (other < Current))
  • Result implies hash_code = other.hash_code

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

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

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
This feature is obsolete: Now use `clear_count' or `clear_count_and_capacity' (july 17th 2004).
clear_count

Discard all characters (is_empty is True after that call). The internal capacity is not changed by this call. See also clear_count_and_capacity to select the most appropriate. Note: internal storage memory is neither released nor shrunk.

ensure

  • count = 0

wipe_out

Discard all characters (is_empty is True after that call). The internal capacity is not changed by this call. See also clear_count_and_capacity to select the most appropriate. Note: internal storage memory is neither released nor shrunk.

ensure

  • count = 0

clear_count_and_capacity

Discard all characters (is_empty is True after that call). The internal capacity may also be reduced after this call. See also clear_count to select the most appropriate.

ensure

  • is_empty: count = 0
  • capacity = 0

copy (other: UNICODE_STRING)

Copy other onto Current.

require

  • 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: INTEGER, new_code: INTEGER)

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: INTEGER, 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

+ (other: UNICODE_STRING): UNICODE_STRING

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: INTEGER, 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: INTEGER, 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: UNICODE_STRING

New object in lower case.

as_upper: UNICODE_STRING

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: INTEGER, 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: INTEGER, 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

  • stripped: is_empty or else not is_space(first)

right_adjust

Remove trailing blanks.

ensure

  • stripped: is_empty or else not is_space(last)

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.

do_all (action: ROUTINE [O_ -> TUPLE][TUPLE 1 [A_][INTEGER]])

Apply action to every item of Current.

See also for_all, exists.

for_all (test: FUNCTION [O_ -> TUPLE, R_][TUPLE 1 [A_][INTEGER]BOOLEAN]): BOOLEAN

Do all items satisfy test?

See also do_all, exists.

exists (test: FUNCTION [O_ -> TUPLE, R_][TUPLE 1 [A_][INTEGER]BOOLEAN]): BOOLEAN

Does at least one item satisfy test?

See also do_all, for_all.

first: INTEGER

Access to the very first character.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: INTEGER

Access to the very last character.

require

  • not is_empty

ensure

  • definition: Result = item(upper)

substring (start_index: INTEGER, end_index: INTEGER): UNICODE_STRING

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)

split: ARRAY [E_][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 [E_][UNICODE_STRING])

Same jobs as split but result is appended in words.

require

  • words /= Void

ensure

  • words.count >= old words.count

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 [E_][INTEGER]
valid_unicode (unicode: INTEGER): BOOLEAN
is_space (unicode: INTEGER): BOOLEAN
is_separator (unicode: INTEGER): BOOLEAN
is_combining (unicode: INTEGER): BOOLEAN
deferred is_equal (other: UNICODE_STRING): BOOLEAN

Is other attached to an object considered equal to current object ?

require

  • other /= Void

ensure

  • Result implies hash_code = other.hash_code
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

is_equal (other: UNICODE_STRING): BOOLEAN

Is other attached to an object considered equal to current object ?

require

  • other /= Void

ensure

  • trichotomy: Result = (not (Current < other) and not (other < Current))
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)

<= (other: UNICODE_STRING): BOOLEAN

Is Current less than or equal other?

See also >=, <, >, min, max.

require

  • other_exists: other /= Void

ensure

  • definition: Result = (Current < other or is_equal(other))

> (other: UNICODE_STRING): BOOLEAN

Is Current strictly greater than other?

See also <, >=, <=, min, max.

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: UNICODE_STRING): BOOLEAN

Is Current greater than or equal than other?

See also <=, >, <, min, max.

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other <= Current)

in_range (lower: UNICODE_STRING, upper: UNICODE_STRING): BOOLEAN

Return True if Current is in range [lower..upper]

See also min, max, compare.

ensure

  • Result = (Current >= lower and Current <= upper)

min (other: UNICODE_STRING): UNICODE_STRING

Minimum of Current and other.

See also max, in_range.

require

  • other /= Void

ensure

  • Result <= Current and then Result <= other
  • compare(Result) = 0 or else other.compare(Result) = 0

max (other: UNICODE_STRING): UNICODE_STRING

Maximum of Current and other.

See also min, in_range.

require

  • other /= Void

ensure

  • Result >= Current and then Result >= other
  • compare(Result) = 0 or else other.compare(Result) = 0

valid_index (i: INTEGER): BOOLEAN

True when i is valid (i.e., inside actual bounds).

See also lower, upper, item.

ensure

  • definition: Result = (lower <= i and i <= upper)

Class invariant