class UNICODE_STRING
Summary
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 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
Inherit list: COMPARABLE, HASHABLE, RECYCLABLE, SEARCHABLE, TRAVERSABLE
Insert list: UNICODE_STRING_HELPER
Class invariant
Overview
Creation features
{ANY}
Features
{UNICODE_STRING, UNICODE_STRING_HANDLER}
{ANY}
Creation / Modification:
{ANY}
Testing:
{ANY}
Testing and Conversion:
{ANY}
{}
Modification:
{ANY}
Printing:
{ANY}
Other features:
{ANY}
Splitting a STRING:
{ANY}
  • split: ARRAY[UNICODE_STRING]
    Split the string into an array of words.
  • split_in (words: COLLECTION[UNICODE_STRING])
    Same jobs as split but result is appended in words.
Other features:
{ANY}
{UNICODE_STRING, UNICODE_STRING_HANDLER}
{}
{}
{}
{RECYCLING_POOL}
  • recycle
    Do whatever needs to be done to free resources or recycle other objects when recycling this one
{ANY}
  • infix "<=" (other: UNICODE_STRING): BOOLEAN
    Is Current less than or equal other?
  • infix ">" (other: UNICODE_STRING): BOOLEAN
    Is Current strictly greater than other?
  • infix ">=" (other: UNICODE_STRING): BOOLEAN
    Is Current greater than or equal than other?
  • in_range (lower: UNICODE_STRING, upper: UNICODE_STRING): BOOLEAN
    Return True if Current is in range [lower..upper]
    See also min, max, compare.
  • min (other: UNICODE_STRING): UNICODE_STRING
    Minimum of Current and other.
  • max (other: UNICODE_STRING): UNICODE_STRING
    Maximum of Current and other.
  • bounded_by (a_min: UNICODE_STRING, a_max: UNICODE_STRING): UNICODE_STRING
    A value that is equal to Current if it is between the limits set by a_min and a_max.
{ANY}
Other features:
{ANY}
Agent-based features:
{ANY}
{ANY}
Agent-based features:
{ANY}
{}
Indexing:
{ANY}
{ANY}
The place where characters are stored.
WARNING: it's only storage area. Each Unicode value stored using 2 bytes (CHARACTER). Encoding used is UTF-16NE. low surrogates are stored in other way for direct access.
count: INTEGER_32
writable attribute
{ANY}
String length which is also the maximum valid index.
See also is_empty, lower, upper.
ensure
  • Result >= 0
capacity: INTEGER_32
writable attribute
{ANY}
Capacity of the storage area.
lower: INTEGER_32
is 1
constant attribute
{ANY}
Minimum index; actually, this is always 1 (this feature here to mimic the one of the COLLECTION hierarchy).
See also upper, valid_index, item.
upper: INTEGER_32
effective function
{ANY}
Maximum index; actually the same value as count (this feature is here to mimic the one of the COLLECTION hierarchy).
See also lower, valid_index, item.
ensure
make (needed_capacity: INTEGER_32)
effective procedure
{ANY}
Initialize the string to have at least needed_capacity characters of storage.
require
  • non_negative_size: needed_capacity >= 0
ensure
make_empty
effective procedure
{ANY}
Create an empty string.
make_filled (unicode: INTEGER_32, n: INTEGER_32)
effective procedure
{ANY}
Initialize string with n copies of unicode.
require ensure
is_empty: BOOLEAN
effective function
{ANY}
Has string length 0?
See also count.
ensure
  • definition: Result = count = 0
effective function
{ANY}
Get unicode at position i.
See also lower, upper, valid_index, put.
require
    • valid_index(i)
    • valid_index(i)
infix "@" (i: INTEGER_32): INTEGER_32
effective function
{ANY}
The infix notation which is actually just a synonym for item.
See also item, put.
require ensure
  • definition: Result = item(i)
hash_code: INTEGER_32
effective function
{ANY}
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
infix "<" (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
Is Current less than other?
See also >, <=, >=, min, max.
require
  • other_exists: other /= Void
ensure
  • asymmetric: Result implies not other < Current
compare (other: UNICODE_STRING): INTEGER_32
effective function
{ANY}
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_32
effective function
{ANY}
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
effective function
{ANY}
Do both strings have the same character sequence?
See also same_as.
require
    • other /= Void
    • other /= Void
ensure
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
  • Result implies hash_code = other.hash_code
  • trichotomy: Result = not Current < other and not other < Current
same_as (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
Case insensitive is_equal.
require
  • other /= Void
index_of (unicode: INTEGER_32, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at or after start_index, 0 if none.
require ensure
  • Result /= 0 implies item(Result) = unicode
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies (create {SAFE_EQUAL}).test(unicode, item(Result))
fast_index_of (unicode: INTEGER_32, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at or after start_index, 0 if none.
require ensure
  • Result /= 0 implies item(Result) = unicode
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies unicode = item(Result)
reverse_index_of (unicode: INTEGER_32, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at or before start_index, 0 if none.
The search is done in reverse direction, which means from the start_index down to the first character.
See also index_of, last_index_of, first_index_of. require
  valid_start_index: start_index >= 0 and start_index <= count
  valid_unicode_value: valid_unicode(unicode)
require
  • valid_index(start_index)
ensure
  • Result /= 0 implies item(Result) = unicode
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result).is_equal(unicode)
fast_reverse_index_of (unicode: INTEGER_32, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at or before start_index, 0 if none.
The search is done in reverse direction, which means from the start_index down to the first character.
See also index_of, last_index_of, first_index_of. require
  valid_start_index: start_index >= 0 and start_index <= count
  valid_unicode_value: valid_unicode(unicode)
require
  • valid_index(start_index)
ensure
  • Result /= 0 implies item(Result) = unicode
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result) = unicode
first_index_of (unicode: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at index 1 or after index 1.
ensure
  • definition: Result = index_of(unicode, lower)
fast_first_index_of (unicode: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of first occurrence of unicode at index 1 or after index 1.
ensure
  • definition: Result = fast_index_of(unicode, lower)
last_index_of (unicode: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of last occurrence of unicode, 0 if none.
ensure
  • definition: Result = reverse_index_of(unicode, upper)
fast_last_index_of (unicode: INTEGER_32): INTEGER_32
effective function
{ANY}
Index of last occurrence of unicode, 0 if none.
ensure
  • definition: Result = fast_reverse_index_of(unicode, upper)
has (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
True if unicode is in the STRING.
require ensure
  • definition: Result = valid_index(first_index_of(unicode))
fast_has (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
True if unicode is in the STRING.
require ensure
  • definition: Result = valid_index(fast_first_index_of(unicode))
has_substring (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
True if Current contains other.
See also substring_index, has.
require
  • other_not_void: other /= Void
occurrences (unicode: INTEGER_32): INTEGER_32
effective function
{ANY}
Number of times character unicode appears in the string.
require ensure
  • Result >= 0
has_suffix (s: UNICODE_STRING): BOOLEAN
effective function
{ANY}
True if suffix of Current is s.
require
  • s /= Void
has_prefix (p: UNICODE_STRING): BOOLEAN
effective function
{ANY}
True if prefix of Current is p.
require
  • p /= Void
is_ascii: BOOLEAN
effective function
{ANY}
True if all unicode value is in range 0..127
to_utf8: STRING
effective function
{ANY}
New string is created, current unicode string is encoded with UTF-8 format.
See also: utf8_encode_in and as_utf8 to save memory.
as_utf8: STRING
effective function
{ANY}
Encode the string in UTF-8.
Always returns the same once object.
See also: to_utf8, utf8_encode_in.
utf8_encode_in (s: STRING)
effective procedure
{ANY}
Append the string in UTF-8 to s.
See also: to_utf8, as_utf8.
require
  • s /= Void
utf16be_encode_in (s: STRING)
effective procedure
{ANY}
Append the string in UTF-16BE to s
require
  • s /= Void
utf8_decode_from (s: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
Use s as UTF-8 format encoded unicode string Return False if decoding process failed
require
  • s /= Void
from_utf8 (s: ABSTRACT_STRING)
effective procedure
{}
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
resize (new_count: INTEGER_32)
effective procedure
{ANY}
Resize Current.
When new_count is greater than count, new positions are initialized with unicode 0.
require
  • new_count >= 0
ensure
clear_count
effective procedure
{ANY}
Discard all characters so that is_empty is True after that call.
The internal capacity is not changed by this call (i.e. the internal storage memory neither released nor shrunk).
See also clear_count_and_capacity.
ensure
wipe_out
effective procedure
{ANY}
Discard all characters so that is_empty is True after that call.
The internal capacity is not changed by this call (i.e. the internal storage memory neither released nor shrunk).
See also clear_count_and_capacity.
ensure
clear_count_and_capacity
effective procedure
{ANY}
Discard all characters (is_empty is True after that call).
The internal capacity may also be reduced after this call.
See also clear_count.
ensure
copy (other: UNICODE_STRING)
effective procedure
{ANY}
Copy other onto Current.
See also copy_substring.
require
    • not immutable
    • same_dynamic_type(other)
    • not immutable
    • same_dynamic_type(other)
ensure
copy_substring (s: UNICODE_STRING, start_index: INTEGER_32, end_index: INTEGER_32)
effective procedure
{ANY}
Copy the substring from s from start_index to end_index to Current.
See also copy.
require
  • string_not_void: s /= Void
  • valid_start_index: 1 <= start_index
  • valid_end_index: end_index <= s.count
  • meaningful_interval: start_index <= end_index + 1
fill_with (unicode: INTEGER_32)
effective procedure
{ANY}
Replace every unicode with the new value.
require ensure
replace_all (old_code: INTEGER_32, new_code: INTEGER_32)
effective procedure
{ANY}
Replace all occurrences of the element old_code by new_code.
require ensure
append (s: UNICODE_STRING)
effective procedure
{ANY}
Append a copy of 's' to Current.
See also add_last, add_first, prepend, '+'.
require
  • s_not_void: s /= Void
append_string (s: UNICODE_STRING)
effective procedure
{ANY}
Append a copy of 's' to Current.
See also add_last, add_first, prepend, '+'.
require
  • s_not_void: s /= Void
append_substring (s: UNICODE_STRING, start_index: INTEGER_32, end_index: INTEGER_32)
effective procedure
{ANY}
Append the substring from s from start_index to end_index to Current.
|*** DUMB IMPLEMENTATION
require
  • string_not_void: s /= Void
  • valid_start_index: 1 <= start_index
  • valid_end_index: end_index <= s.count
  • meaningful_interval: start_index <= end_index + 1
prepend (other: UNICODE_STRING)
effective procedure
{ANY}
Prepend other to Current.
See also append.
require
  • other /= Void
ensure
insert_string (s: UNICODE_STRING, i: INTEGER_32)
effective procedure
{ANY}
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_32, end_index: INTEGER_32)
effective procedure
{ANY}
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): UNICODE_STRING
effective function
{ANY}
Create a new UNICODE_STRING which is the concatenation of Current and other.
See also append.
require
  • other_exists: other /= Void
ensure
put (unicode: INTEGER_32, i: INTEGER_32)
effective procedure
{ANY}
Put unicode at position i.
See also item, lower, upper, swap.
require ensure
swap (i1: INTEGER_32, i2: INTEGER_32)
effective procedure
{ANY}
Swap two characters.
See also item, put.
require ensure
insert_character (unicode: INTEGER_32, i: INTEGER_32)
effective procedure
{ANY}
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
shrink (min_index: INTEGER_32, max_index: INTEGER_32)
effective procedure
{ANY}
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_32)
effective procedure
{ANY}
Remove character at position i.
require ensure
add_first (unicode: INTEGER_32)
effective procedure
{ANY}
Add unicode at first position.
See also add_last.
require ensure
precede (unicode: INTEGER_32)
effective procedure
{ANY}
Add unicode at first position.
See also add_last.
require ensure
add_last (unicode: INTEGER_32)
effective procedure
{ANY}
Append unicode to string.
See also add_first.
require ensure
append_character (unicode: INTEGER_32)
effective procedure
{ANY}
Append unicode to string.
See also add_first.
require ensure
extend (unicode: INTEGER_32)
effective procedure
{ANY}
Append unicode to string.
See also add_first.
require ensure
to_lower
effective procedure
{ANY}
Convert all characters to lower case.
See also to_upper, as_lower, as_upper.
to_upper
effective procedure
{ANY}
Convert all characters to upper case.
See also to_lower, as_upper, as_lower.
as_lower: UNICODE_STRING
effective function
{ANY}
New object with all letters in lower case.
See also as_upper, to_lower, to_upper.
as_upper: UNICODE_STRING
effective function
{ANY}
New object with all letters in upper case.
See also as_lower, to_upper, to_lower.
keep_head (n: INTEGER_32)
effective procedure
{ANY}
Remove all characters except for the first n.
Do nothing if n >= count.
See also keep_tail, remove_head, remove_tail.
require
  • n_non_negative: n >= 0
ensure
keep_tail (n: INTEGER_32)
effective procedure
{ANY}
Remove all characters except for the last n.
Do nothing if n >= count.
See also keep_head, remove_tail, remove_head.
require
  • n_non_negative: n >= 0
ensure
remove_first
effective procedure
{ANY}
Remove the first item.
require ensure
remove_head (n: INTEGER_32)
effective procedure
{ANY}
Remove n first characters.
If n >= count, remove all.
See also remove_tail, remove, remove_the_first.
require
  • n_non_negative: n >= 0
ensure
remove_last
effective procedure
{ANY}
Remove the last item.
require ensure
remove_tail (n: INTEGER_32)
effective procedure
{ANY}
Remove n last characters.
If n >= count, remove all.
See also remove_head, remove, remove_the_last.
require
  • n_non_negative: n >= 0
ensure
remove_substring (start_index: INTEGER_32, end_index: INTEGER_32)
effective procedure
{ANY}
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
remove_between (start_index: INTEGER_32, end_index: INTEGER_32)
effective procedure
{ANY}
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
remove_suffix (s: UNICODE_STRING)
effective procedure
{ANY}
Remove the suffix s of current string.
require ensure
remove_prefix (s: UNICODE_STRING)
effective procedure
{ANY}
Remove the prefix s of current string.
require ensure
left_adjust
effective procedure
{ANY}
Remove leading blanks.
See also remove_head, first.
ensure
right_adjust
effective procedure
{ANY}
Remove trailing blanks.
See also remove_tail, last.
ensure
out_in_tagged_out_memory
effective procedure
{ANY}
Append terse printable representation of current object in tagged_out_memory.
require
    • locked: tagged_out_locked
    • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • 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
effective procedure
{ANY}
Append a viewable information in tagged_out_memory in order to affect the behavior of out, tagged_out, etc.
require
    • locked: tagged_out_locked
    • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
first: INTEGER_32
effective function
{ANY}
Access to the very first character.
See also last, item.
require
    • not is_empty
    • not is_empty
ensure
  • definition: Result = item(lower)
last: INTEGER_32
effective function
{ANY}
Access to the very last character.
See also first, item.
require
    • not is_empty
    • not is_empty
ensure
  • definition: Result = item(upper)
substring (start_index: INTEGER_32, end_index: INTEGER_32): UNICODE_STRING
effective function
{ANY}
New string consisting of items [start_index.. end_index].
See also substring_index and copy_substring to save memory.
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_32, n: INTEGER_32)
effective procedure
{ANY}
Extend Current with n times character unicode.
require ensure
precede_multiple (unicode: INTEGER_32, n: INTEGER_32)
effective procedure
{ANY}
Prepend n times character unicode to Current.
require ensure
extend_to_count (unicode: INTEGER_32, needed_count: INTEGER_32)
effective procedure
{ANY}
Extend Current with unicode until needed_count is reached.
Do nothing if needed_count is already greater or equal to count.
require ensure
precede_to_count (unicode: INTEGER_32, needed_count: INTEGER_32)
effective procedure
{ANY}
Prepend unicode to Current until needed_count is reached.
Do nothing if needed_count is already greater or equal to count.
require ensure
reverse
effective procedure
{ANY}
Reverse the string.
remove_all_occurrences (unicode: INTEGER_32)
effective procedure
{ANY}
Remove all occurrences of unicode.
See also occurrences, remove.
require ensure
substring_index (other: UNICODE_STRING, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
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_32
effective function
{ANY}
Position of first occurrence of other at or after 1, 0 if none.
See also substring_index.
require
  • other_not_void: other /= Void
ensure
split: ARRAY[UNICODE_STRING]
effective function
{ANY}
Split the string into an array of words.
Uses is_separator to find words. Gives Void or a non empty array.
See also split_in.
ensure
  • Result /= Void implies not Result.is_empty
split_in (words: COLLECTION[UNICODE_STRING])
effective procedure
{ANY}
Same jobs as split but result is appended in words.
See also split.
require
  • words /= Void
ensure
  • words.count >= old words.count
extend_unless (unicode: INTEGER_32)
effective procedure
{ANY}
Extend Current (using extend) with unicode unless unicode ch is already the last character.
require ensure
new_iterator: ITERATOR[INTEGER_32]
effective function
{ANY}
ensure
  • Result /= Void
  • Result.generation = generation
valid_unicode (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
is_space (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
is_separator (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
is_combining (unicode: INTEGER_32): BOOLEAN
effective function
{ANY}
low_surrogate_indexes: FAST_ARRAY[INTEGER_32]
writable attribute
user indexes (starting at 1)
low_surrogate_values: FAST_ARRAY[INTEGER_16]
writable attribute
low surrogate value is stored without 0xDC00 part and endianness dependant !
set_count (new_count: INTEGER_32)
effective procedure
require
string_buffer: UNICODE_STRING
once function
{}
Private, temporary once buffer.
tmp_buffer: STRING
once function
{}
Private, temporary once buffer.
split_buffer: ARRAY[UNICODE_STRING]
once function
{}
low_surrogate_value (index: INTEGER_32): INTEGER_16
effective function
{}
require
  • storage.item(index) & 0xF800 = 0xD800
ensure
  • Result.in_range(0, 1023)
low_surrogate_index (index: INTEGER_32): INTEGER_32
effective function
{}
require ensure
low_surrogate_position (index: INTEGER_32): INTEGER_32
effective function
{}
return position to use in low_surrogate* arrays relative to character at index in the string (return the good answer if the corresponding character is not surrogate)
ensure
valid_surrogates: BOOLEAN
effective function
{}
manifest_initialize (c: INTEGER_32, s: NATIVE_ARRAY[INTEGER_16], ls_cap: INTEGER_32, lsv: NATIVE_ARRAY[INTEGER_16], lsi: NATIVE_ARRAY[INTEGER_32])
effective procedure
{}
This function is a compiler-hook automatically called when a manifest unicode string (i.e. U"foo") is used in the Eiffel source code.
debug_utf8: STRING
writable attribute
{}
set_debug_utf8
effective procedure
{}
next_generation
effective procedure
{}
ensure
  • generation > old generation
recycle
effective procedure
Do whatever needs to be done to free resources or recycle other objects when recycling this one
infix "<=" (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
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)
infix ">" (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
Is Current strictly greater than other?
See also <, >=, <=, min, max.
require
  • other_exists: other /= Void
ensure
  • definition: Result = other < Current
infix ">=" (other: UNICODE_STRING): BOOLEAN
effective function
{ANY}
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
effective function
{ANY}
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
effective function
{ANY}
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
effective function
{ANY}
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
bounded_by (a_min: UNICODE_STRING, a_max: UNICODE_STRING): UNICODE_STRING
effective function
{ANY}
A value that is equal to Current if it is between the limits set by a_min and a_max.
Otherwise it's a_min if Current is smaller or a_max if Current is greater It's a shortcut for Current.min(a_max).max(a_min) also known as "clamp" in the widespread C library Glib
ensure
  • correctness: Result.in_range(a_min, a_max)
enumerate: ENUMERATE[E_]
effective function
{ANY}
get_new_iterator: ITERATOR[E_]
frozen
effective function
{ANY}
This feature is obsolete: Use `new_iterator' instead. This historical SmartEiffel feature is badly named.
for_each (action: PROCEDURE[TUPLE[TUPLE 1[E_]]])
effective procedure
{ANY}
Apply action to every item of Current.
See also for_all, exists, aggregate.
require
  • action /= Void
for_all (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN
effective function
{ANY}
Do all items satisfy test?
See also for_each, exists, aggregate.
require
  • test /= Void
exists (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN
effective function
{ANY}
Does at least one item satisfy test?
See also for_each, for_all, aggregate.
require
  • test /= Void
aggregate (action: FUNCTION[TUPLE[TUPLE 2[E_, E_], E_]], initial: E_): E_
effective function
{ANY}
Aggregate all the elements starting from the initial value.
See also for_each, for_all, exists.
require
  • action /= Void
generation: INTEGER_32
writable attribute
{ANY}
do_all (action: ROUTINE[TUPLE[TUPLE 1[E_]]])
frozen
effective procedure
{ANY}
Apply action to every item of Current.
This feature is obsolete: Use `for_each` instead. This feature is not secure because it accepts a FUNCTION, the result of which is lost.
_inline_agent1 (a: ROUTINE[TUPLE[TUPLE 1[E_]]], e: E_)
frozen
effective procedure
{}
valid_index (i: INTEGER_32): BOOLEAN
effective function
{ANY}
True when i is valid (i.e., inside actual bounds).
See also lower, upper, item.
ensure
utf8_character_in (character: INTEGER_32, s: STRING)
effective procedure
{ANY}
require
  • character >= 0
  • s /= Void