indexing
description: "Objects that are able to iterate over linear structures"
status: "See notice at end of class"
names: iterators, iteration, linear_iterators, linear_iteration
date: "$Date$"
revision: "$Revision$"
class interface
LINEAR_ITERATOR [G]
create
set (s: like target)
s
require ITERATOR
target_exists: s /= void
ensure ITERATOR
target = s
target /= void
feature
set (s: like target)
s
require ITERATOR
target_exists: s /= void
ensure ITERATOR
target = s
target /= void
feature
item: G
target
require
traversable_exists: target /= void
item_tuple: TUPLE [G]
target
target: LINEAR [G]
feature
invariant_value: BOOLEAN
target
ITERATOR
feature
exhausted: BOOLEAN
target
forth
target
off: BOOLEAN
target
start
target
feature
internal_item_tuple: TUPLE [G]
target
feature
continue_for (action: PROCEDURE [ANY, TUPLE [G]]; n, k: INTEGER)
actionk
n
require
valid_repetition: n >= 0
valid_skip: k >= 1
continue_search (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]; b: BOOLEAN)
target
testb
target
ensure then
found: not exhausted = (b = test.item (item_tuple))
continue_until (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
target
require
invariant_satisfied: invariant_value
ensure then
achieved: not exhausted implies test.item (item_tuple)
continue_while (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
target
require else
invariant_satisfied: invariant_value
ensure then
finished: not exhausted implies not test.item (item_tuple)
do_all (action: PROCEDURE [ANY, TUPLE [G]])
actiontarget
ITERATOR
require ITERATOR
action_exists: action /= void
do_for (action: PROCEDURE [ANY, TUPLE [G]]; i, n, k: INTEGER)
actionk
ni
require
valid_start: i >= 1
valid_repetition: n >= 0
valid_skip: k >= 1
do_if (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontargettest
ITERATOR
require ITERATOR
action_exists: action /= void
test_exists: test /= void
do_until (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
require ITERATOR
action_exists: action /= void
test_exists: test /= void
ensure then
achieved: not exhausted implies test.item (item_tuple)
do_while (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
starttarget
require ITERATOR
action_exists: action /= void
test_exists: test /= void
ensure then
finished: not exhausted implies not test.item (item_tuple)
for_all (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]): BOOLEAN
test
target
require ITERATOR
test_exists: test /= void
search (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]; b: BOOLEAN)
targettest
b
there_exists (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]): BOOLEAN
test
target
require ITERATOR
test_exists: test /= void
until_continue (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
require
invariant_satisfied: invariant_value
ensure
achieved: exhausted or else test.item (item_tuple)
invariant_satisfied: invariant_value
until_do (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
test
require ITERATOR
action_exists: action /= void
test_exists: test /= void
ensure then
achieved: not exhausted implies test.item (item_tuple)
while_continue (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
ensure
finished: not exhausted implies not test.item (item_tuple)
while_do (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
actiontarget
test
test
require ITERATOR
action_exists: action /= void
test_exists: test /= void
ensure then
finished: not exhausted implies not test.item (item_tuple)
invariant
target_exists: target /= void
item_tuple_exists: item_tuple /= void
internal_item_tuple_exists: internal_item_tuple /= void
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
ITERATOR
traversable_exists: target /= void
end -- LINEAR_ITERATOR