GNU
|
Liberty Eiffel
|
Automated Tests
|
Wiki
|
Savannah project
|
Debian packages
|
Documentation
>
tutorial
>
ITERATOR_ON_RANDOM_GENERATOR
+
Point of view
All features
ANY
All features
class ITERATOR_ON_RANDOM_GENERATOR
Summary
top
Direct parents
Inherit list:
ITERATOR
Class invariant
top
generation_only_grows
Overview
top
Creation features
{
ANY
}
make
(c:
INTEGER_32
)
Features
{
ANY
}
count
:
INTEGER_32
Of the sequence.
item
:
INTEGER_32
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.
{}
seed
:
INTEGER_32
range
:
INTEGER_32
left
:
INTEGER_32
random_number_generator
:
MINIMAL_RANDOM_NUMBER_GENERATOR
make
(c:
INTEGER_32
)
Check that the underlying traversable has not changed
{
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
count
:
INTEGER_32
writable attribute
{
ANY
}
top
Of the sequence.
item
:
INTEGER_32
writable attribute
{
ANY
}
top
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
}
top
Positions the iterator to the first object in the aggregate to be traversed.
ensure
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
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
seed
:
INTEGER_32
is 5555
constant attribute
{}
top
range
:
INTEGER_32
is 256
constant attribute
{}
top
left
:
INTEGER_32
writable attribute
{}
top
random_number_generator
:
MINIMAL_RANDOM_NUMBER_GENERATOR
writable attribute
{}
top
make
(c:
INTEGER_32
)
effective procedure
{}
top
require
count
>= 0
iterable_generation
:
INTEGER_32
is 0
constant attribute
{
ANY
}
top
generation
:
INTEGER_32
is 0
constant 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