GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
libraries
>
ITERATOR_ON_BIJECTIVE_DICTIONARY_KEYS
+
Point of view
All features
ANY
All features
class ITERATOR_ON_BIJECTIVE_DICTIONARY_KEYS [V_, K_]
Summary
top
Please do not use this class directly. Look at
ITERATOR
.
Direct parents
Inherit list:
ITERATOR
Class invariant
top
generation_only_grows
Overview
top
Creation features
{
ANY
}
make
(d: BIJECTIVE_DICTIONARY[V_, K_])
Features
{}
bijective_dictionary
: BIJECTIVE_DICTIONARY[V_, K_]
The one to be traversed.
item_index
:
INTEGER_32
{
ANY
}
make
(d: BIJECTIVE_DICTIONARY[V_, K_])
start
Positions the iterator to the first object in the aggregate to be traversed.
is_off
:
BOOLEAN
Returns True when there are no more objects in the sequence.
item
: K_
Returns the object at the current position in the sequence.
next
Positions the iterator to the next object in the sequence.
{
ANY
}
iterable_generation
:
INTEGER_32
generation
:
INTEGER_32
{
ANY
}
is_valid
:
BOOLEAN
Agent-based features:
{
ANY
}
for_each
(action:
PROCEDURE
[
TUPLE
[TUPLE 1[E_]]])
Apply
action
to every item of
Current
.
for_all
(test:
FUNCTION
[
TUPLE
[TUPLE 1[E_]]]):
BOOLEAN
Do all items satisfy
test
?
exists
(test:
FUNCTION
[
TUPLE
[TUPLE 1[E_]]]):
BOOLEAN
Does at least one item satisfy
test
?
aggregate
(action:
FUNCTION
[
TUPLE
[TUPLE 2[E_, E_], E_]], initial: E_): E_
Aggregate all the elements starting from the initial value.
Invariant on
generation` dynamics
{}
generation_for_invariant
:
INTEGER_32
generation_only_grows
:
BOOLEAN
bijective_dictionary
: BIJECTIVE_DICTIONARY[V_, K_]
writable attribute
{}
top
The one to be traversed.
item_index
:
INTEGER_32
writable attribute
{}
top
make
(d: BIJECTIVE_DICTIONARY[V_, K_])
effective procedure
{
ANY
}
top
require
d /= Void
ensure
bijective_dictionary
= d
start
effective procedure
{
ANY
}
top
Positions the iterator to the first object in the aggregate to be traversed.
ensure
is_valid
is_off
:
BOOLEAN
effective function
{
ANY
}
top
Returns True when there are no more objects in the sequence.
require
is_valid
ensure
generation = old generation
is_valid
item
: K_
effective function
{
ANY
}
top
Returns the object at the current position in the sequence.
require
is_valid
not is_off
ensure
generation = old generation
is_valid
next
effective procedure
{
ANY
}
top
Positions the iterator to the next object in the sequence.
require
is_valid
not is_off
ensure
generation = old generation
is_valid
iterable_generation
:
INTEGER_32
effective function
{
ANY
}
top
generation
:
INTEGER_32
writable attribute
{
ANY
}
top
is_valid
:
BOOLEAN
frozen
effective function
{
ANY
}
top
for_each
(action:
PROCEDURE
[
TUPLE
[TUPLE 1[E_]]])
effective procedure
{
ANY
}
top
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
}
top
Do all items satisfy
test
?
See also
for_each
,
exists
,
aggregate
.
exists
(test:
FUNCTION
[
TUPLE
[TUPLE 1[E_]]]):
BOOLEAN
effective function
{
ANY
}
top
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
}
top
Aggregate all the elements starting from the initial value.
See also
for_each
,
for_all
,
exists
.
generation_for_invariant
:
INTEGER_32
writable attribute
{}
top
generation_only_grows
:
BOOLEAN
effective function
{}
top