+
Point of view
All features
class ITERATOR_WITH_VARIANT [X]
Summary
Acts like a Facade in order to add a loop variant facility on any kinds of ITERATOR[X].
Direct parents
Inherit list: ITERATOR
Insert list: PLATFORM
Class invariant
Overview
Creation features
{ANY}
  • make (iterator: ITERATOR[X])
Features
{ANY}
  • make (iterator: ITERATOR[X])
  • variant_value: INTEGER_32
  • item: X
    Returns the object at the current position in the sequence.
  • start
    Positions the iterator to the first object in the aggregate to be traversed.
  • next
    Positions the iterator to the next object in the sequence.
  • is_off: BOOLEAN
    Returns True when there are no more objects in the sequence.
Check that the underlying traversable has not changed
{ANY}
{}
{ANY}
Agent-based features:
{ANY}
Invariant on generation` dynamics
{}
Maximum:
{}
Minimum:
{}
Bits:
{}
make (iterator: ITERATOR[X])
effective procedure
{ANY}
require
  • iterator /= Void
ensure
variant_value: INTEGER_32
writable attribute
{ANY}
item: X
effective function
{ANY}
Returns the object at the current position in the sequence.
require
  • is_valid
  • not is_off
ensure
  • generation = old generation
  • is_valid
start
effective procedure
{ANY}
Positions the iterator to the first object in the aggregate to be traversed.
ensure
  • is_valid
next
effective procedure
{ANY}
Positions the iterator to the next object in the sequence.
require
  • is_valid
  • not is_off
ensure
  • generation = old generation
  • is_valid
is_off: BOOLEAN
effective function
{ANY}
Returns True when there are no more objects in the sequence.
require
  • is_valid
ensure
  • generation = old generation
  • is_valid
iterable_generation: INTEGER_32
effective function
{ANY}
generation: INTEGER_32
effective function
{ANY}
basic_iterator: ITERATOR[X]
writable attribute
{}
The true (fast) iterator.
is_valid: BOOLEAN
frozen
effective function
{ANY}
for_each (action: PROCEDURE[TUPLE[TUPLE 1[E_]]])
effective procedure
{ANY}
Apply action to every item of Current.
See also for_all, exists, aggregate.
for_all (test: FUNCTION[TUPLE[TUPLE 1[E_]]]): BOOLEAN
effective function
{ANY}
Do all items satisfy test?
See also for_each, exists, aggregate.
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.
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.
generation_for_invariant: INTEGER_32
writable attribute
{}
generation_only_grows: BOOLEAN
effective function
{}
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.