class LAZY_STRING
Summary
A string made with the output of an agent function given at creation time. The agent function will be run only when actually required, for example accessing the elements of the string or iterating over it; the result of the agent function will be cached for further usage.
Direct parents
Inherit list: ABSTRACT_STRING
Class invariant
Overview
Creation features
{ANY}
Features
redefinitions
{ANY}
{ANY}
from SEARCHABLE
{ANY}
from HOARD
{ANY}
from HASHABLE
{ANY}
{RECYCLING_POOL}
  • recycle
    Do whatever needs to be done to free resources or recycle other objects when recycling this one
{STRING_HANDLER}
{}
{LAZY_STRING}
{ANY}
Testing:
{ANY}
Testing and Conversion:
{ANY}
Concatenation
{ANY}
Case conversion
{ANY}
Printing:
{ANY}
String replacing
{ANY}
Other features:
{ANY}
Splitting a STRING:
{ANY}
Other features here for ELKS compatibility:
{ANY}
{}
The states of the finite state automaton used in arg feature
{}
{}
{ANY}
  • in_range (lower: LAZY_STRING, upper: LAZY_STRING): BOOLEAN
    Return True if Current is in range [lower..upper]
    See also min, max, compare.
  • min (other: LAZY_STRING): LAZY_STRING
    Minimum of Current and other.
  • max (other: LAZY_STRING): LAZY_STRING
    Maximum of Current and other.
  • bounded_by (a_min: LAZY_STRING, a_max: LAZY_STRING): LAZY_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}
Maximum:
{}
Minimum:
{}
Bits:
{}
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
immutable: BOOLEAN
is True
constant attribute
{ANY}
Is the object immutable?
new_iterator: ITERATOR[CHARACTER]
effective function
{ANY}
ensure
  • Result /= Void
  • Result.generation = generation
lazy_out: ABSTRACT_STRING
effective function
{ANY}
A newly allocate "lazy" representation of current object.
Lazy means that actual representation is made only on demand when the string actually used; the actual content of the representation is made using running out query as an agent.
prefix "&": ABSTRACT_STRING
effective function
{ANY}
A newly allocate "lazy" representation of current object.
Lazy means that actual representation is made only on demand when the string actually used; the actual content of the representation is made using running out query as an agent.
copy (other: LAZY_STRING)
effective procedure
{ANY}
Update current object using fields of object attached to other, so as to yield equal objects.
Note: you can't copy object from a different dynamic type.
require
    • not immutable
    • same_dynamic_type(other)
    • not immutable
    • same_dynamic_type(other)
ensure
  • count = other.count
  • is_equal(other)
item (i: INTEGER_32): CHARACTER
effective function
{ANY}
Character at position i.
See also lower, upper, valid_index, put.
require
    • valid_index(i)
    • valid_index(i)
is_equal (other: ABSTRACT_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: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
Case insensitive is_equal.
require
  • other /= Void
occurrences (c: CHARACTER): INTEGER_32
effective function
{ANY}
Number of times character c appears in the string.
See also remove_all_occurrences, has.
ensure
  • Result >= 0
infix "&" (other: ABSTRACT_STRING): ABSTRACT_STRING
effective function
{ANY}
Current and other concatenating into a new object.
The actual effective type of Result chosen by the implementation, possibly based on heuristics.
require
  • other_exists: other /= Void
ensure
  • Result.out.is_equal(Current + other)
first: CHARACTER
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: CHARACTER
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): LAZY_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: lower <= start_index
  • valid_end_index: end_index <= upper
  • meaningful_interval: start_index <= end_index + 1
ensure
  • substring_count: Result.count = end_index - start_index + 1
intern: FIXED_STRING
effective function
{ANY}
A shared version of this string.
ensure
  • Result /= Void
  • Result.is_equal(Current)
  • Result.is_interned
  • interned.fast_has(Result.hash_code) and then interned.fast_reference_at(Result.hash_code).fast_has(Result)
to_external: POINTER
effective function
{ANY}
The address of a memory region containing the text of Current, useful to interact with the C language.
A NATIVELY_STORED_STRING implementation usually gives direct access to its internal storage (may be dangerous). Other non-natively stored heirs provide access to an Eiffel-owned buffer containing a copy of its content. 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
has (x: CHARACTER): BOOLEAN
effective function
{ANY}
Look for x using is_equal for comparison.
ensure
  • definition: Result = valid_index(first_index_of(x))
fast_has (x: CHARACTER): BOOLEAN
effective function
{ANY}
Look for x using basic = for comparison.
See also has, fast_index_of, index_of.
ensure
  • definition: Result = valid_index(fast_first_index_of(x))
index_of (element: CHARACTER, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Using is_equal for comparison, gives the index of the first occurrence of element at or after start_index.
Return upper + 1 if the search for element failed.
See also fast_index_of, reverse_index_of, first_index_of.
ensure
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies (create {SAFE_EQUAL}).test(element, item(Result))
reverse_index_of (element: CHARACTER, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Using is_equal for comparison, gives the index of the first occurrence of element at or before start_index.
Search is done in reverse direction, which means from the start_index down to the lower index . Answer lower -1 when the search fail.
See also fast_reverse_index_of, last_index_of, index_of.
require
  • valid_index(start_index)
ensure
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result).is_equal(element)
fast_index_of (element: CHARACTER, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Using basic = for comparison, gives the index of the first occurrence of element at or after start_index.
Answer upper + 1 when element when the search fail.
See also index_of, fast_reverse_index_of, fast_first_index_of.
ensure
  • Result.in_range(start_index, upper + 1)
  • valid_index(Result) implies element = item(Result)
fast_reverse_index_of (element: CHARACTER, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Using basic = comparison, gives the index of the first occurrence of element at or before start_index.
Search is done in reverse direction, which means from the start_index down to the lower index . Answer lower -1 when the search fail.
See also reverse_index_of, fast_index_of, fast_last_index_of.
require
  • valid_index(start_index)
ensure
  • Result.in_range(lower - 1, start_index)
  • valid_index(Result) implies item(Result) = element
count: INTEGER_32
effective function
{ANY}
Number of available items in the hoard.
See also is_empty
ensure
  • Result >= 0
hash_code: INTEGER_32
effective function
{ANY}
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
recycle
effective procedure
Do whatever needs to be done to free resources or recycle other objects when recycling this one
copy_slice_to_native (start_index: INTEGER_32, end_index: INTEGER_32, target: NATIVE_ARRAY[CHARACTER], target_offset: INTEGER_32)
effective procedure
require
  • start_index >= lower
  • end_index <= upper
  • start_index <= end_index
make (a_outter: FUNCTION[TUPLE, ABSTRACT_STRING])
effective procedure
{}
require
  • a_outter /= Void
ensure
substring_out (a_lazy_string: LAZY_STRING, start_index: INTEGER_32, end_index: INTEGER_32): ABSTRACT_STRING
effective function
{}
writable attribute
{}
lazy_out_memory: WEAK_REFERENCE[ABSTRACT_STRING]
writable attribute
{}
lazy_out_: ABSTRACT_STRING
effective function
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
print_on (file: OUTPUT_STREAM)
effective procedure
{ANY}
Default printing of current object on a file.
One may redefine fill_tagged_out_memory or out_in_tagged_out_memory to adapt the behavior of print_on.
require
    • file.is_connected
    • file.is_connected
is_empty: BOOLEAN
effective function
{ANY}
Has string length 0?
See also count.
ensure
  • definition: Result = count = 0
infix "@" (i: INTEGER_32): CHARACTER
frozen
effective function
{ANY}
The infix notation which is actually just a synonym for item.
See also item, put.
require ensure
  • definition: Result = item(i)
infix "^" (a_range: INTEGER_RANGE[INTEGER_32]): ABSTRACT_STRING
effective function
{ANY}
Substring of items in a_range .
require ensure
  • Result.count = a_range.count
  • has_substring(Result)
    This is the same of writing "substring_index(Result,lower)=a_range.lower"

infix "<" (other: ABSTRACT_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
infix "<=" (other: ABSTRACT_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: ABSTRACT_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: ABSTRACT_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
compare (other: ABSTRACT_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: ABSTRACT_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
item_code (i: INTEGER_32): INTEGER_32
effective function
{ANY}
Code of character at position i.
See also item.
require ensure
  • definition: Result = item(i).code
first_index_of (c: CHARACTER): INTEGER_32
effective function
{ANY}
Index of first occurrence of c, upper` + 1 if none. See also `last_index_of, index_of, reverse_index_of.
ensure
  • definition: Result = index_of(c, lower)
fast_first_index_of (c: CHARACTER): INTEGER_32
effective function
{ANY}
Index of first occurrence of c, upper` + 1 if none. See also `last_index_of, index_of, reverse_index_of.
ensure
  • definition: Result = fast_index_of(c, lower)
last_index_of (c: CHARACTER): INTEGER_32
effective function
{ANY}
Index of last occurrence of c, lower` - 1 if none. See also `first_index_of, reverse_index_of, index_of.
ensure
  • definition: Result = reverse_index_of(c, upper)
fast_last_index_of (c: CHARACTER): INTEGER_32
effective function
{ANY}
Index of last occurrence of c, lower` - 1 if none. See also `first_index_of, reverse_index_of, index_of.
ensure
  • definition: Result = fast_reverse_index_of(c, upper)
has_substring (other: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
True if Current contains other.
See also substring_index, has.
require
  • other_not_void: other /= Void
has_suffix (s: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
True if suffix of Current is s.
See also remove_suffix, has_prefix, has_substring.
require
  • s /= Void
has_prefix (p: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
True if prefix of Current is p.
See also remove_prefix, has_suffix, has_substring.
require
  • p /= Void
is_ascii: BOOLEAN
effective function
{ANY}
Is Current only made of (7 bit) ASCII characters?
ensure
is_boolean: BOOLEAN
effective function
{ANY}
Does Current represent a BOOLEAN?
Valid BOOLEANs are "True" and "False".
to_boolean: BOOLEAN
effective function
{ANY}
Boolean value "True" yields True, "False" yields False (what a surprise).
require
is_integer: BOOLEAN
effective function
{ANY}
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_32
effective function
{ANY}
Current must look like an INTEGER.
require
is_integer_64: BOOLEAN
effective function
{ANY}
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
effective function
{ANY}
Current must look like an INTEGER_64.
require
is_real: BOOLEAN
effective function
{ANY}
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 arithmetic 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_64
effective function
{ANY}
Conversion to the corresponding REAL value.
The string must looks like a REAL (or like an INTEGER because the fractional part is optional). For an exact definition see 'is_real'. Note that this conversion might not be exact.
require
is_number: BOOLEAN
effective function
{ANY}
Can contents be read as a NUMBER?
to_number: NUMBER
effective function
{ANY}
Current must looks like an INTEGER.
require
is_bit: BOOLEAN
effective function
{ANY}
True when the contents is a sequence of bits (i.e., mixed characters 0 and characters 1).
ensure
binary_to_integer: INTEGER_32
effective function
{ANY}
Assume there is enough space in the INTEGER to store the corresponding decimal value.
infix "+" (other: ABSTRACT_STRING): STRING
effective function
{ANY}
Create a new STRING which is the concatenation of Current and other.
See also append.
require
  • other_exists: other /= Void
ensure
infix "|" (other: ABSTRACT_STRING): ROPE
effective function
{ANY}
Current and other concatenated into a new ROPE, an ABSTRACT_STRING that can be efficiently concatenated.
require
  • other_exists: other /= Void
ensure
  • Result.out.is_equal(Current + other)
arg (an_index: INTEGER_32, a_value: ABSTRACT_STRING): ABSTRACT_STRING
effective function
{ANY}
A copy of Current with the placeholder "#(an_index)" is replaced (if present) with the content of a_value.
ensure
infix "#" (a_value: ABSTRACT_STRING): ABSTRACT_STRING
effective function
{ANY}
A copy of Current with a placeholder "#(n)" is replaced with the content of a_value.
A chain of # queries will progressively replace placeholder 1, 2 ...
For example a_string#"foo"#"bar"#"maman" is equivalent to a_string.arg(1,"foo").arg(2,"bar").arg(3,"maman")
See also arg.
as_lower: STRING
effective function
{ANY}
New object with all letters in lower case.
See also as_upper, to_lower, to_upper.
as_upper: STRING
effective function
{ANY}
New object with all letters in upper case.
See also as_lower, to_upper, to_lower.
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))
replacing (an_old: ABSTRACT_STRING, a_new: ABSTRACT_STRING): STRING
effective function
{ANY}
Current with all occurrences of an_old string replaced with a_new.
require ensure
  • Result /= Current
  • not Result.valid_index(Result.first_substring_index(an_old))
  • Result.first_substring_index(a_new) = first_substring_index(an_old)
replacing_in (an_old: ABSTRACT_STRING, a_new: ABSTRACT_STRING, buffer: STRING)
effective procedure
{ANY}
Current with all occurrences of an_old string replaced with a_new in buffer.
require
  • not an_old.is_empty
  • a_new /= Void
  • buffer /= Current
ensure
  • not buffer.valid_index(buffer.substring_index(an_old, old buffer.upper + buffer.lower))
  • buffer.substring_index(a_new, old buffer.upper + buffer.lower) = old buffer.upper + first_substring_index(an_old)
substring_index (other: ABSTRACT_STRING, start_index: INTEGER_32): INTEGER_32
effective function
{ANY}
Position of first occurrence of other at or after start_index.
If there is no occurrence Result will be an invalid index, usually 0 when lower is 1.
See also substring, first_substring_index.
require
  • other_not_void: other /= Void
  • valid_start_index: start_index >= lower and start_index <= upper + 1
first_substring_index (other: ABSTRACT_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[STRING]
effective function
{ANY}
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[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
same_string (other: ABSTRACT_STRING): BOOLEAN
effective function
{ANY}
(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
effective function
{ANY}
(Here for ELKS compatibility.)
New STRING having the same character sequence as Current. Useful in proper descendants of STRING.
string_buffer: STRING
once function
{}
Private, temporary once buffer.
split_buffer: ARRAY[STRING]
once function
{}
computed_hash_code: INTEGER_32
effective function
{}
once function
{}
Key: hash_code Item: interned string
always_print_state: INTEGER_32
is -1
constant attribute
{}
normal_state: INTEGER_32
is 0
constant attribute
{}
after_delimiter_state: INTEGER_32
is 1
constant attribute
{}
after_brace_state: INTEGER_32
is 2
constant attribute
{}
Please note that we picked the same values used in MESSAGE_FORMATTER.
It may also be written like "always_print_state, normal_state, after_delimiter_state, after_brace_state: INTEGER is unique" but I'm not sure that the compiler will actually choose sequential values necessary in the last if tense in the arg query
debug_string: STRING
writable attribute
{}
only used to display the content of the FIXED_STRING in the trace stack
in_range (lower: LAZY_STRING, upper: LAZY_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: LAZY_STRING): LAZY_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: LAZY_STRING): LAZY_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: LAZY_STRING, a_max: LAZY_STRING): LAZY_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}
next_generation
effective procedure
{}
ensure
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
Maximum_character_code: INTEGER_16
{}
Largest supported code for CHARACTER values.
ensure
  • meaningful: Result >= 127
Maximum_integer_8: INTEGER_8
is 127
constant attribute
{}
Largest supported value of type INTEGER_8.
Maximum_integer_16: INTEGER_16
is 32767
constant attribute
{}
Largest supported value of type INTEGER_16.
Maximum_integer: INTEGER_32
is 2147483647
constant attribute
{}
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_32: INTEGER_32
is 2147483647
constant attribute
{}
Largest supported value of type INTEGER/INTEGER_32.
Maximum_integer_64: INTEGER_64
is 9223372036854775807
constant attribute
{}
Largest supported value of type INTEGER_64.
Maximum_real_32: REAL_32
is {REAL_32 3.4028234663852885981170418348451692544e+38}
constant attribute
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL_32.
Maximum_real: REAL_64
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: 1.79769313486231570....e+308
Maximum_real_64: REAL_64
{}
Largest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: 1.79769313486231570....e+308
Maximum_real_80: REAL_EXTENDED
{}
Largest supported value of type REAL_80.
ensure
Minimum_character_code: INTEGER_16
{}
Smallest supported code for CHARACTER values.
ensure
  • meaningful: Result <= 0
Minimum_integer_8: INTEGER_8
is -128
constant attribute
{}
Smallest supported value of type INTEGER_8.
Minimum_integer_16: INTEGER_16
is -32768
constant attribute
{}
Smallest supported value of type INTEGER_16.
Minimum_integer: INTEGER_32
is -2147483648
constant attribute
{}
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_32: INTEGER_32
is -2147483648
constant attribute
{}
Smallest supported value of type INTEGER/INTEGER_32.
Minimum_integer_64: INTEGER_64
is -9223372036854775808
constant attribute
{}
Smallest supported value of type INTEGER_64.
Minimum_real_32: REAL_32
is {REAL_32 -3.40282346638528859811704183484516925440e+38}
constant attribute
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL_32.
Minimum_real: REAL_64
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: -1.79769313486231570....e+308
Minimum_real_64: REAL_64
{}
Smallest non-special (no NaNs nor infinity) supported value of type REAL.
Just to give an idea of this value: -1.79769313486231570....e+308
Minimum_real_80: REAL_64
{}
Smallest supported value of type REAL_80.
ensure
  • meaningful: Result <= 0.0
Boolean_bits: INTEGER_32
{}
Number of bits in a value of type BOOLEAN.
ensure
  • meaningful: Result >= 1
Character_bits: INTEGER_32
{}
Number of bits in a value of type CHARACTER.
ensure
Integer_bits: INTEGER_32
{}
Number of bits in a value of type INTEGER.
ensure
  • integer_definition: Result = 32
Real_bits: INTEGER_32
is 64
constant attribute
{}
Number of bits in a value of type REAL.
Pointer_bits: INTEGER_32
{}
Number of bits in a value of type POINTER.