class STRING

Features exported to STRING_HANDLER

Resizable character STRINGs indexed from 1 to count.

Direct parents

conformant parents

ANY, COMPARABLE, HASHABLE, STORABLE, TRAVERSABLE

non-conformant parents

PLATFORM

Summary

creation features

exported features

Creation / Modification:

Testing:

Testing and Conversion:

Modification:

Printing:

Agents based features:

Other features:

Splitting a STRING:

Other features:

Interfacing with C string:

Other features here for ELKS compatibility:

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: 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 (c: CHARACTER, n: INTEGER)

Initialize string with n copies of c.

require

  • valid_count: n >= 0

ensure

  • count_set: count = n
  • filled: occurrences(c) = count

from_external (p: POINTER)

Internal storage is set using p (may be dangerous because the external C string p is not duplicated). Assume p has a null character at the end in order to compute the Eiffel count. This extra null character is not part of the Eiffel STRING. Also consider from_external_copy to choose the most appropriate.

require

  • p.is_not_null

ensure

  • capacity = count + 1
  • p = to_external

from_external_copy (p: POINTER)

Internal storage is set using a copy of p. Assume p has a null character at the end in order to compute the Eiffel count. This extra null character is not part of the Eiffel STRING. Also consider from_external to choose the most appropriate.

require

  • p.is_not_null

make_from_string (model: STRING)

(Here for ELKS compatibility.) Initialize from the characters of model. Useful in proper descendants of STRING.

require

  • model /= Void

ensure

  • count = model.count

storage: NATIVE_ARRAY [E_][CHARACTER]

The place where characters are stored.

count: INTEGER

String length which is also the maximum valid index.

See also is_empty, lower, upper.

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 COLLECTION hierarchy).

See also upper, valid_index, item.

upper: INTEGER

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

  • 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 (c: CHARACTER, n: INTEGER)

Initialize string with n copies of c.

require

  • valid_count: n >= 0

ensure

  • count_set: count = n
  • filled: occurrences(c) = count

is_empty: BOOLEAN

Has string length 0?

See also count.

ensure

  • definition: Result = (count = 0)

item (i: INTEGER): CHARACTER

Character at position i.

See also lower, upper, valid_index, put.

require

  • valid_index(i)

frozen @ (i: INTEGER): CHARACTER

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

See also item, put.

require

  • valid_index: valid_index(i)

ensure

  • definition: Result = item(i)

hash_code: INTEGER

The hash-code value of Current.

ensure

  • good_hash_value: Result >= 0

< (other: STRING): BOOLEAN

Is Current less than other?

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

require

  • other_exists: other /= Void

ensure

  • asymmetric: Result implies not (other < Current)

compare (other: 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: 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: STRING): BOOLEAN

Do both strings have the same character sequence?

See also same_as.

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: STRING): BOOLEAN

Case insensitive is_equal.

require

  • other /= Void

item_code (i: INTEGER): INTEGER

Code of character at position i.

See also item.

require

  • valid_index: valid_index(i)

ensure

  • definition: Result = item(i).code

index_of (c: CHARACTER, start_index: INTEGER): INTEGER

Index of first occurrence of c at or after start_index, 0 if none.

See also reverse_index_of, first_index_of, last_index_of, has.

require

  • valid_start_index: start_index >= 1 and start_index <= count + 1

ensure

  • Result /= 0 implies item(Result) = c

reverse_index_of (c: CHARACTER, start_index: INTEGER): INTEGER

Index of first occurrence of c 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

ensure

  • Result /= 0 implies item(Result) = c

first_index_of (c: CHARACTER): INTEGER

Index of first occurrence of c, 0 if none.

See also last_index_of, index_of, reverse_index_of.

ensure

  • definition: Result = index_of(c, 1)

last_index_of (c: CHARACTER): INTEGER

Index of last occurrence of c, 0 if none.

See also first_index_of, reverse_index_of, index_of.

ensure

  • definition: Result = reverse_index_of(c, upper)

has (c: CHARACTER): BOOLEAN

True if c is in the STRING.

See also index_of, occurrences, has_substring.

has_substring (other: STRING): BOOLEAN

True if Current contains other.

require

  • other_not_void: other /= Void

occurrences (c: CHARACTER): INTEGER

Number of times character c appears in the string.

See also remove_all_occurrences, has.

ensure

  • Result >= 0

has_suffix (s: STRING): BOOLEAN

True if suffix of Current is s.

require

  • s /= Void

has_prefix (p: STRING): BOOLEAN

True if prefix of Current is p.

require

  • p /= Void

is_boolean: BOOLEAN

Does Current represent a BOOLEAN? Valid BOOLEANs are "True" and "False".

to_boolean: BOOLEAN

Boolean value "True" yields True, "False" yields False (what a surprise).

require

  • represents_a_boolean: is_boolean

is_integer: BOOLEAN

Does 'Current' represent an INTEGER? Result is True if and only if the following two conditions hold:

1. In the following BNF grammar, the value of Current can be produced by "Integer_literal", if leading and trailing separators are ignored:

Integer_literal = [Sign] Integer Sign = "+" | "-" Integer = Digit | Digit Integer Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

2. The numerical value represented by Current is within the range that can be represented by an instance of type INTEGER.

to_integer: INTEGER

Current must look like an INTEGER.

require

  • is_integer

is_integer_64: BOOLEAN

Does 'Current' represent an INTEGER_64? Result is True if and only if the following two conditions hold:

1. In the following BNF grammar, the value of Current can be produced by "Integer_literal", if leading and trailing separators are ignored:

Integer_literal = [Sign] Integer Sign = "+" | "-" Integer = Digit | Digit Integer Digit = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

2. The numerical value represented by Current is within the range that can be represented by an instance of type INTEGER_64.

to_integer_64: INTEGER_64

Current must look like an INTEGER_64.

require

  • is_integer_64

is_double: BOOLEAN
This feature is obsolete: Now use `is_real / to_real' only. October 3rd 2004. No more DOUBLE type mark.
to_double: REAL
This feature is obsolete: Now use `is_real / to_real' only. October 3rd 2004. No more DOUBLE type mark.
is_real: BOOLEAN

Can contents be read as a REAL ? Fails for numbers where the base or "10 ^ exponent" are not in the range Minimum_real ... Maximum_real. Parsing is done positive. That means if Minimum_real.abs is not equal to Maximum_real it will not work correctly. Furthermore the arithmetric package used must support the value 'inf' for a number greater than Maximum_real. Result is True if and only if the following two conditions hold:

1. In the following BNF grammar, the value of Current can be produced by "Real_literal", if leading or trailing separators are ignored.

Real_literal = Mantissa [Exponent_part] Exponent_part = "E" Exponent

                | "e" Exponent
Exponent        = Integer_literal
Mantissa        = Decimal_literal
Decimal_literal = Integer_literal ["." Integer]
Integer_literal = [Sign] Integer
Sign            = "+" | "-"
Integer         = Digit | Digit Integer
Digit           = "0"|"1"|"2"|"3"|"4"|"5"|"6"|"7"|"8"|"9"

2. The numerical value represented by Current is within the range that can be represented by an instance of type REAL.

to_real: REAL

Conversion to the corresponding REAL value. The string must looks like a REAL (or like an INTEGER because the fractionnal part is optional). For an exact definition see 'is_real'. Note that this conversion might not be exact.

require

  • represents_a_real: is_real

is_number: BOOLEAN

Can contents be read as a NUMBER?

to_number: NUMBER

Current must looks like an INTEGER.

require

  • is_number

is_bit: BOOLEAN

True when the contents is a sequence of bits (i.e., mixed characters 0 and characters 1).

ensure

  • Result = (count = occurrences('0') + occurrences('1'))

to_hexadecimal

Convert Current bit sequence into the corresponding hexadecimal notation.

require

  • is_bit

binary_to_integer: INTEGER

Assume there is enougth space in the INTEGER to store the corresponding decimal value.

require

  • is_bit

resize (new_count: INTEGER)

Resize Current. When new_count is greater than count, new positions are initialized with the default value of type CHARACTER ('%U').

require

  • new_count >= 0

ensure

  • count = new_count
  • capacity >= old capacity

clear
This feature is obsolete: The new name is now `clear_count' (July 2004).
clear_count

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 is neither released nor shrunk).

See also clear_count_and_capacity.

ensure

  • is_empty: count = 0
  • capacity = old capacity

wipe_out

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 is neither released nor shrunk).

See also clear_count_and_capacity.

ensure

  • is_empty: count = 0
  • capacity = old capacity

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.

ensure

  • is_empty: count = 0
  • capacity = 0
  • storage.is_null

copy (other: STRING)

Copy other onto Current.

require

  • same_dynamic_type(other)

ensure

  • count = other.count
  • is_equal(other)

fill_with (c: CHARACTER)

Replace every character with c.

ensure

  • occurrences(c) = count

replace_all (old_character: CHARACTER, new_character: CHARACTER)

Replace all occurrences of the element old_character by new_character.

ensure

  • count = old count
  • old_character /= new_character implies occurrences(old_character) = 0

append (s: STRING)

Append a copy of 's' to Current.

See also add_last, add_first, prepend, '+'.

require

  • s_not_void: s /= Void

append_string (s: STRING)

Append a copy of 's' to Current.

See also add_last, add_first, prepend, '+'.

require

  • s_not_void: s /= Void

append_substring (s: STRING, start_index: INTEGER, end_index: INTEGER)

Append the substring from s from start_index to end_index to Current.

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

Prepend other to Current.

See also append.

require

  • other /= Void

ensure

  • (old other.twin + old Current.twin).is_equal(Current)

insert_string (s: 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: 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: STRING): STRING

Create a new STRING which is the concatenation of Current and other.

See also append.

require

  • other_exists: other /= Void

ensure

  • result_count: Result.count = count + other.count

put (c: CHARACTER, i: INTEGER)

Put c at index i.

See also item, lower, upper, swap.

require

  • valid_index: valid_index(i)

ensure

  • item(i) = c

swap (i1: INTEGER, i2: INTEGER)

Swap two characters.

See also item, put.

require

  • valid_index(i1)
  • valid_index(i2)

ensure

  • item(i1) = old item(i2)
  • item(i2) = old item(i1)

insert_character (c: CHARACTER, i: INTEGER)

Inserts c at index i, shifting characters from position 'i' to count rightwards.

require

  • valid_insertion_index: 1 <= i and i <= count + 1

ensure

  • item(i) = c

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.

See also remove_head, remove_between, remove_suffix, remove_prefix.

require

  • valid_removal_index: valid_index(i)

ensure

  • count = old count - 1

add_first (c: CHARACTER)

Add c at first position.

See also add_last.

ensure

  • count = 1 + old count
  • item(1) = c

precede (c: CHARACTER)

Add c at first position.

See also add_last.

ensure

  • count = 1 + old count
  • item(1) = c

add_last (c: CHARACTER)

Append c to string.

See also add_first.

ensure

  • count = 1 + old count
  • item(count) = c

append_character (c: CHARACTER)

Append c to string.

See also add_first.

ensure

  • count = 1 + old count
  • item(count) = c

extend (c: CHARACTER)

Append c to string.

See also add_first.

ensure

  • count = 1 + old count
  • item(count) = c

to_lower

Convert all characters to lower case.

See also to_upper, as_lower, as_upper.

to_upper

Convert all characters to upper case.

See also to_lower, as_upper, as_lower.

as_lower: STRING

New object with all letters in lower case.

See also as_upper, to_lower, to_upper.

as_upper: STRING

New object with all letters in upper case.

See also as_lower, to_upper, to_lower.

keep_head (n: INTEGER)

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

  • count = n.min(old count)

keep_tail (n: INTEGER)

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

  • count = n.min(old count)

remove_first (n: INTEGER)
This feature is obsolete: Now use `remove_head' instead (may 22th 2005).
remove_head (n: INTEGER)

Remove n first characters. If n >= count, remove all.

See also remove_tail, remove, remove_the_first.

require

  • n_non_negative: n >= 0

ensure

  • count = 0.max(old count - n)

remove_the_first

Remove the first item. See also remove_head.

Note: to be uniform with COLLECTION, this feature will be renamed as remove_first in 2006.

require

  • not is_empty

ensure

  • count = old count - 1

remove_last (n: INTEGER)
This feature is obsolete: Now use `remove_tail' instead (may 22th 2005).
remove_tail (n: INTEGER)

Remove n last characters. If n >= count, remove all.

See also remove_head, remove, remove_the_last.

require

  • n_non_negative: n >= 0

ensure

  • count = 0.max(old count - n)

remove_the_last

Remove the last item. See also remove_tail.

Note: to be uniform with COLLECTION, this feature will be renamed as remove_last in 2006.

require

  • not is_empty

ensure

  • count = old count - 1

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

Remove the suffix s of current string.

See also remove_prefix, remove_tail, remove.

require

  • has_suffix(s)

ensure

  • (old Current.twin).is_equal(Current + old s.twin)

remove_prefix (s: STRING)

Remove the prefix s of current string.

See also remove_suffix, remove_head, remove.

require

  • has_prefix(s)

ensure

  • (old s.twin + Current).is_equal(old Current.twin)

left_adjust

Remove leading blanks.

See also remove_head, first.

ensure

  • stripped: is_empty or else first /= ' '

right_adjust

Remove trailing blanks.

See also remove_tail, last.

ensure

  • stripped: is_empty or else 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_][CHARACTER]])

Apply action to every item of Current.

See also for_all, exists.

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

Do all items satisfy test?

See also do_all, exists.

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

Does at least one item satisfy test?

See also for_all, do_all.

first: CHARACTER

Access to the very first character.

See also last, item.

require

  • not is_empty

ensure

  • definition: Result = item(lower)

last: CHARACTER

Access to the very last character.

See also first, item.

require

  • not is_empty

ensure

  • definition: Result = item(upper)

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

New string consisting of items [start_index.. end_index].

See also substring_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 (c: CHARACTER, n: INTEGER)

Extend Current with n times character c.

require

  • n >= 0

ensure

  • count = n + old count

precede_multiple (c: CHARACTER, n: INTEGER)

Prepend n times character c to Current.

require

  • n >= 0

ensure

  • count = n + old count

extend_to_count (c: CHARACTER, needed_count: INTEGER)

Extend Current with c until needed_count is reached. Do nothing if needed_count is already greater or equal to count.

require

  • needed_count >= 0

ensure

  • count >= needed_count

precede_to_count (c: CHARACTER, needed_count: INTEGER)

Prepend c to Current until needed_count is reached. Do nothing if needed_count is already greater or equal to count.

require

  • needed_count >= 0

ensure

  • count >= needed_count

reverse

Reverse the string.

remove_all_occurrences (ch: CHARACTER)

Remove all occurrences of ch.

See also occurrences, remove.

ensure

  • count = old count - old occurrences(ch)

substring_index (other: STRING, start_index: INTEGER): INTEGER

Position of first occurrence of other at or after start 0 if none.

See also substring, first_substring_index.

require

  • other_not_void: other /= Void
  • valid_start_index: start_index >= 1 and start_index <= count + 1

first_substring_index (other: STRING): INTEGER

Position of first occurrence of other at or after 1, 0 if none.

See also substring_index.

require

  • other_not_void: other /= Void

ensure

  • definition: Result = substring_index(other, 1)

split: ARRAY [E_][STRING]

Split the string into an array of words. Uses is_separator of CHARACTER 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 [E_][STRING])

Same jobs as split but result is appended in words.

See also split.

require

  • words /= Void

ensure

  • words.count >= old words.count

extend_unless (ch: CHARACTER)

Extend Current (using extend) with ch unless ch is already the last character.

ensure

  • last = ch
  • count >= old count

get_new_iterator: ITERATOR [E_][CHARACTER]
to_external: POINTER

Gives C access to the internal storage (may be dangerous). To be compatible with C, a null character is added at the end of the internal storage. This extra null character is not part of the Eiffel STRING.

ensure

  • count = old count
  • Result.is_not_null

from_external (p: POINTER)

Internal storage is set using p (may be dangerous because the external C string p is not duplicated). Assume p has a null character at the end in order to compute the Eiffel count. This extra null character is not part of the Eiffel STRING. Also consider from_external_copy to choose the most appropriate.

require

  • p.is_not_null

ensure

  • capacity = count + 1
  • p = to_external

from_external_copy (p: POINTER)

Internal storage is set using a copy of p. Assume p has a null character at the end in order to compute the Eiffel count. This extra null character is not part of the Eiffel STRING. Also consider from_external to choose the most appropriate.

require

  • p.is_not_null

from_c (p: POINTER)
This feature is obsolete: Now use `from_external_copy' instead (8th juen 2005).
make_from_string (model: STRING)

(Here for ELKS compatibility.) Initialize from the characters of model. Useful in proper descendants of STRING.

require

  • model /= Void

ensure

  • count = model.count

same_string (other: STRING): BOOLEAN

(Here for ELKS compatibility.) Do Current and other have the same character sequence? Useful in proper descendants of STRING.

require

  • other_not_void: other /= Void

string: STRING

(Here for ELKS compatibility.) New STRING having the same character sequence as Current. Useful in proper descendants of STRING.

set_count (new_count: INTEGER)

require

  • new_count <= capacity

ensure

  • count = new_count

set_storage (new_storage: NATIVE_ARRAY [E_][CHARACTER], new_capacity: INTEGER)

require

  • count <= new_capacity

ensure

  • storage = new_storage
  • capacity = new_capacity

deferred is_equal (other: 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: 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: 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: STRING): BOOLEAN

Is Current strictly greater than other?

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

require

  • other_exists: other /= Void

ensure

  • definition: Result = (other < Current)

>= (other: 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: STRING, upper: 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: STRING): 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: STRING): 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