indexing
description: "A sequence of actions to be performed on call"
legal: "See notice at end of class."
instructions: "[
Use features inherited from LIST to add/remove actions.
An action is a procedure of ANY class that takes EVENT_DATA.
When call is called the actions in the list will be executed
in order stating at first.
An action may call abort which will cause call to stop executing
actions in the sequence. (Until the next call to call).
Descendants may redefine `initialize' to arrange for call to
be called by an event source.
Use block, pause, flush and resume to change the behavior
of call.
eg.
birthday_data: TUPLE [INTEGER, STRING] -- (age, name)
birthday_actions: ACTIONS_SEQUENCE [like birthday_data]
create birthday_actions.make ("birthday", <<"age","name">>)
send_card (age: INTEGER, name, from: STRING) is ...
buy_gift (age: INTEGER, name, gift, from: STRING) is ...
birthday_actions.extend (agent send_card (?, ?, "Sam")
birthday_actions.extend (agent buy_gift (?, ?, "Wine", "Sam")
birthday_actions.call ([35, "Julia"])
causes call to: send_card (35, "Julia", "Sam")
buy_gift (35, "Julia", "Wine", "Sam")
]"
status: "See notice at end of class."
keywords: "event, action"
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
ACTION_SEQUENCE [EVENT_DATA -> TUPLE create default_create end]
create
default_create
Normal_state
make
create {ACTION_SEQUENCE}
array_make (min_index, max_index: INTEGER_32)
`min_index'`max_index'
`min_index'`max_index'
ARRAY
require ARRAY
valid_bounds: min_index <= max_index + 1
ensure ARRAY
lower_set: lower = min_index
upper_set: upper = max_index
items_set: all_default
arrayed_list_make (n: INTEGER_32)
`n'
`n'
ARRAYED_LIST
require ARRAYED_LIST
valid_number_of_items: n >= 0
ensure ARRAYED_LIST
correct_position: before
is_empty: is_empty
make_filled (n: INTEGER_32)
`n'
`n'
ARRAYED_LIST
require ARRAYED_LIST
valid_number_of_items: n >= 0
ensure ARRAYED_LIST
correct_position: before
filled: full
feature
arrayed_list_make (n: INTEGER_32)
`n'
`n'
ARRAYED_LIST
require ARRAYED_LIST
valid_number_of_items: n >= 0
ensure ARRAYED_LIST
correct_position: before
is_empty: is_empty
make_filled (n: INTEGER_32)
`n'
`n'
ARRAYED_LIST
require ARRAYED_LIST
valid_number_of_items: n >= 0
ensure ARRAYED_LIST
correct_position: before
filled: full
make_from_array (a: ARRAY [PROCEDURE [ANY, EVENT_DATA]])
`a'
ARRAYED_LIST
require ARRAY
array_exists: a /= Void
ensure then ARRAYED_LIST
correct_position: before
filled: count = a.count
feature
cursor: ARRAYED_LIST_CURSOR
ARRAYED_LIST
ensure CURSOR_STRUCTURE
cursor_not_void: Result /= Void
first: like item
ARRAYED_LIST
require CHAIN
not_empty: not is_empty
generating_type: STRING_8
ANY
generator: STRING_8
ANY
has (v: like item): BOOLEAN
`v'
object_comparison
ARRAYED_LIST
require CONTAINER
True
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
i_th alias "[]" (i: INTEGER_32): like item assign put_i_th
`i'
ARRAYED_LISTinfix "@"
ARRAYED_LIST
require TABLE
valid_key: valid_index (i)
index: INTEGER_32
item
ARRAYED_LIST
index_of (v: like item; i: INTEGER_32): INTEGER_32
`i'`v'
object_comparison
CHAIN
require LINEAR
positive_occurrences: i > 0
ensure LINEAR
non_negative_result: Result >= 0
item: PROCEDURE [ANY, EVENT_DATA]
ARRAYED_LIST
require TRAVERSABLE
not_off: not off
require ACTIVE
readable: readable
require else ARRAYED_LIST
index_is_valid: valid_index (index)
last: like first
ARRAYED_LIST
require CHAIN
not_empty: not is_empty
name: STRING_8
ensure
equal_to_name_internal: equal (Result, name_internal)
sequential_occurrences (v: like item): INTEGER_32
`v'
object_comparison
LINEAR
require BAG
True
ensure BAG
non_negative_occurrences: Result >= 0
infix "@" (i: INTEGER_32): like item assign put_i_th
`i'
ARRAYED_LISTi_th
ARRAYED_LIST
require TABLE
valid_key: valid_index (i)
feature
count: INTEGER_32
ARRAYED_LIST
index_set: INTEGER_INTERVAL
CHAIN
require INDEXABLE
True
ensure INDEXABLE
not_void: Result /= Void
ensure then CHAIN
count_definition: Result.count = count
occurrences (v: like item): INTEGER_32
`v'
object_comparison
CHAIN
require BAG
True
require LINEAR
True
ensure BAG
non_negative_occurrences: Result >= 0
feature {ANY}
capacity: INTEGER_32
ARRAYcount
ARRAY
require BOUNDED
True
ensure then ARRAY
consistent_with_bounds: Result = upper - lower + 1
feature
frozen deep_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
shallow_implies_deep: standard_equal (some, other) implies Result
both_or_none_void: (some = Void) implies (Result = (other = Void))
same_type: (Result and (some /= Void)) implies some.same_type (other)
symmetric: Result implies deep_equal (other, some)
frozen equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.is_equal (other))
is_equal (other: like Current): BOOLEAN
`other'
LIST
require ANY
other_not_void: other /= Void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
ensure then LIST
indices_unchanged: index = old index and other.index = old other.index
true_implies_same_size: Result implies count = other.count
frozen standard_equal (some: ANY; other: like arg #1): BOOLEAN
`some'`other'
ANY
ensure ANY
definition: Result = (some = Void and other = Void) or else ((some /= Void and other /= Void) and then some.standard_is_equal (other))
frozen standard_is_equal (other: like Current): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
same_type: Result implies same_type (other)
symmetric: Result implies other.standard_is_equal (Current)
feature
after: BOOLEAN
LIST
require LINEAR
True
before: BOOLEAN
LIST
require BILINEAR
True
blocked_state: INTEGER_32 is 3
call_is_underway: BOOLEAN
call
ensure
Result = not is_aborted_stack.is_empty
changeable_comparison_criterion: BOOLEAN
object_comparison
CONTAINER
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
exhausted: BOOLEAN
LINEAR
ensure LINEAR
exhausted_when_off: off implies Result
extendible: BOOLEAN is True
DYNAMIC_CHAIN
full: BOOLEAN
ARRAYED_LIST
require BOX
True
is_empty: BOOLEAN
FINITE
is_inserted (v: PROCEDURE [ANY, EVENT_DATA]): BOOLEAN
`v'put
extend
ARRAYED_LIST
isfirst: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
islast: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
normal_state: INTEGER_32 is 1
object_comparison: BOOLEAN
equal`='
`='
CONTAINER
off: BOOLEAN
CHAIN
require TRAVERSABLE
True
paused_state: INTEGER_32 is 2
prunable: BOOLEAN
ARRAYED_LIST
require COLLECTION
True
readable: BOOLEAN
SEQUENCE
require ACTIVE
True
same_type (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
ensure ANY
definition: Result = (conforms_to (other) and other.conforms_to (Current))
state: INTEGER_32
Normal_statePaused_stateBlocked_state
valid_cursor (p: CURSOR): BOOLEAN
`p'
ARRAYED_LIST
valid_cursor_index (i: INTEGER_32): BOOLEAN
`i'
CHAIN
ensure CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))
valid_index (i: INTEGER_32): BOOLEAN
`i'
ARRAYED_LIST
require TABLE
True
require TO_SPECIAL
True
ensure then INDEXABLE
only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
ensure then CHAIN
valid_index_definition: Result = ((i >= 1) and (i <= count))
writable: BOOLEAN
SEQUENCE
require ACTIVE
True
feature
abort
call
require
call_is_underway: call_is_underway
ensure
is_aborted_set: is_aborted_stack.item
block
call
ensure
blocked_state: state = blocked_state
compare_objects
equal
`='
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
object_comparison
compare_references
`='
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion: changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
flush
call
ensure
call_buffer_empty: call_buffer.is_empty
pause
call
`is_blocked'
ensure
paused_state: state = paused_state
resume
blockpausecall
call
ensure
normal_state: state = normal_state
feature
back
ARRAYED_LIST
require BILINEAR
not_before: not before
finish
ARRAYED_LIST
require LINEAR
True
ensure then CHAIN
at_last: not is_empty implies islast
ensure then ARRAYED_LIST
before_when_empty: is_empty implies before
forth
ARRAYED_LIST
require LINEAR
not_after: not after
ensure then LIST
moved_forth: index = old index + 1
go_i_th (i: INTEGER_32)
`i'
ARRAYED_LIST
require CHAIN
valid_cursor_index: valid_cursor_index (i)
ensure CHAIN
position_expected: index = i
go_to (p: CURSOR)
`p'
ARRAYED_LIST
require CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER_32)
`i'
ARRAYED_LIST
ensure CHAIN
too_far_right: (old index + i > count) implies exhausted
too_far_left: (old index + i < 1) implies exhausted
expected_index: (not exhausted) implies (index = old index + i)
search (v: like item)
item`v'
`v'
exhausted
object_comparison
ARRAYED_LIST
require LINEAR
True
ensure LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, item)
item_found: (not exhausted and not object_comparison) implies v = item
start
ARRAYED_LIST
require TRAVERSABLE
True
ensure then CHAIN
at_first: not is_empty implies isfirst
ensure then ARRAYED_LIST
after_when_empty: is_empty implies after
feature
append (s: SEQUENCE [PROCEDURE [ANY, EVENT_DATA]])
`s'
ARRAYED_LIST
require SEQUENCE
argument_not_void: s /= Void
ensure SEQUENCE
new_count: count >= old count
extend (v: like item)
`v'
ARRAYED_LISTforce
ARRAYED_LIST
require COLLECTION
extendible: extendible
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
fill (other: CONTAINER [PROCEDURE [ANY, EVENT_DATA]])
`other'
`other'
CHAIN
require COLLECTION
other_not_void: other /= Void
extendible: extendible
force (v: like item)
`v'
ARRAYED_LISTextend
ARRAYED_LIST
require SEQUENCE
extendible: extendible
ensure then SEQUENCE
new_count: count = old count + 1
item_inserted: has (v)
merge_left (other: ARRAYED_LIST [PROCEDURE [ANY, EVENT_DATA]])
`other'
ARRAYED_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_before: not before
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: count = old count + old other.count
new_index: index = old index + old other.count
other_is_empty: other.is_empty
merge_right (other: ARRAYED_LIST [PROCEDURE [ANY, EVENT_DATA]])
`other'
ARRAYED_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_after: not after
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: count = old count + old other.count
same_index: index = old index
other_is_empty: other.is_empty
put_i_th (v: like i_th; i: INTEGER_32)
`i'`v'
ARRAY
require TABLE
valid_key: valid_index (i)
require TO_SPECIAL
valid_index: valid_index (i)
ensure then INDEXABLE
insertion_done: i_th (i) = v
ensure TO_SPECIAL
inserted: array_item (i) = v
put (v: like item)
`v'
replace
CHAIN
require COLLECTION
extendible: extendible
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then CHAIN
same_count: count = old count
put_front (v: like item)
`v'
ARRAYED_LIST
ensure DYNAMIC_CHAIN
new_count: count = old count + 1
item_inserted: first = v
put_left (v: like item)
`v'
ARRAYED_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_before: not before
ensure DYNAMIC_CHAIN
new_count: count = old count + 1
new_index: index = old index + 1
put_right (v: like item)
`v'
ARRAYED_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_after: not after
ensure DYNAMIC_CHAIN
new_count: count = old count + 1
same_index: index = old index
replace (v: like first)
`v'
ARRAYED_LIST
require ACTIVE
writable: writable
ensure ACTIVE
item_replaced: item = v
feature
prune (v: like item)
`v'
after`v'
ARRAYED_LIST
require COLLECTION
prunable: prunable
prune_all (v: like item)
`v'
object_comparison
ARRAYED_LIST
require COLLECTION
prunable: prunable
ensure COLLECTION
no_more_occurrences: not has (v)
ensure then DYNAMIC_CHAIN
is_exhausted: exhausted
ensure then ARRAYED_LIST
is_after: after
remove
after
ARRAYED_LIST
require ACTIVE
prunable: prunable
writable: writable
ensure then DYNAMIC_LIST
after_when_empty: is_empty implies after
ensure then ARRAYED_LIST
index: index = old index
remove_left
ARRAYED_LIST
require DYNAMIC_CHAIN
left_exists: index > 1
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
new_index: index = old index - 1
remove_right
ARRAYED_LIST
require DYNAMIC_CHAIN
right_exists: index < count
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
same_index: index = old index
wipe_out
ARRAYED_LIST
require COLLECTION
prunable: prunable
ensure COLLECTION
wiped_out: is_empty
ensure then DYNAMIC_LIST
is_before: before
feature
resize (new_capacity: INTEGER_32)
`n'
ARRAYED_LIST
require ARRAYED_LIST
new_capacity_large_enough: new_capacity >= capacity
ensure ARRAYED_LIST
capacity_set: capacity >= new_capacity
feature
swap (i: INTEGER_32)
`i'
ARRAYED_LIST
require CHAIN
not_off: not off
valid_index: valid_index (i)
ensure CHAIN
swapped_to_item: item = old i_th (i)
swapped_from_item: i_th (i) = old item
feature
linear_representation: LINEAR [PROCEDURE [ANY, EVENT_DATA]]
LINEAR
require CONTAINER
True
feature
copy (other: like Current)
`other'
clone
ARRAY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
ensure then ARRAY
equal_areas: area.is_equal (other.area)
frozen deep_copy (other: like Current)
copy`other'deep_twin
ANY
require ANY
other_not_void: other /= Void
ensure ANY
deep_equal: deep_equal (Current, other)
frozen deep_twin: like Current
ANY
ensure ANY
deep_equal: deep_equal (Current, Result)
duplicate (n: INTEGER_32): like Current
`n'countindex
ARRAYED_LIST
require CHAIN
not_off_unless_after: off implies after
valid_subchain: n >= 0
frozen standard_copy (other: like Current)
`other'
ANY
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_standard_equal: standard_is_equal (other)
frozen standard_twin: like Current
`other'
ANY
ensure ANY
standard_twin_not_void: Result /= Void
equal: standard_equal (Result, Current)
frozen twin: like Current
`Current'
twincopycopy
ANY
ensure ANY
twin_not_void: Result /= Void
is_equal: Result.is_equal (Current)
feature
call (event_data: EVENT_DATA)
`is_blocked'
`is_paused'resume
abort
ensure
is_aborted_stack_unchanged: old is_aborted_stack.is_equal (is_aborted_stack)
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
prune_when_called (an_action: like item)
`an_action'
require
has (an_action)
feature
empty_actions: ARRAYED_LIST [PROCEDURE [ANY, TUPLE]]
is_emptyis_empty
not_empty_actions: ARRAYED_LIST [PROCEDURE [ANY, TUPLE]]
is_emptyis_empty
feature
do_all (action: PROCEDURE [ANY, TUPLE [PROCEDURE [ANY, EVENT_DATA]]])
`action'
`action'
LINEAR
require TRAVERSABLE
action_exists: action /= Void
require ARRAY
action_not_void: action /= Void
do_if (action: PROCEDURE [ANY, TUPLE [PROCEDURE [ANY, EVENT_DATA]]]; test: FUNCTION [ANY, TUPLE [PROCEDURE [ANY, EVENT_DATA]], BOOLEAN])
`action'`test'
`action'`test'
LINEAR
require TRAVERSABLE
action_exists: action /= Void
test_exits: test /= Void
require ARRAY
action_not_void: action /= Void
test_not_void: test /= Void
for_all (test: FUNCTION [ANY, TUPLE [PROCEDURE [ANY, EVENT_DATA]], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: test /= Void
require ARRAY
test_not_void: test /= Void
ensure then LINEAR
empty: is_empty implies Result
there_exists (test: FUNCTION [ANY, TUPLE [PROCEDURE [ANY, EVENT_DATA]], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: test /= Void
require ARRAY
test_not_void: test /= Void
feature
io: STD_FILES
ANY
out: STRING_8
ANYtagged_out
ANY
print (some: ANY)
`some'
ANY
frozen tagged_out: STRING_8
ANYout
ANY
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
invariant
is_aborted_stack_not_void: is_aborted_stack /= Void
call_buffer_not_void: call_buffer /= Void
valid_state: state = normal_state or state = paused_state or state = blocked_state
call_buffer_consistent: state = normal_state implies call_buffer.is_empty
not_empty_actions_not_void: not_empty_actions /= Void
empty_actions_not_void: empty_actions /= Void
ARRAYED_LIST
prunable: prunable
starts_from_one: lower = 1
empty_means_storage_empty: is_empty implies all_default
ARRAY
area_exists: area /= Void
consistent_size: capacity = upper - lower + 1
non_negative_count: count >= 0
index_set_has_same_count: valid_index_set
RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
BOUNDED
valid_count: count <= capacity
full_definition: full = (count = capacity)
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
INDEXABLE
index_set_not_void: index_set /= Void
LIST
before_definition: before = (index = 0)
after_definition: after = (index = count + 1)
CHAIN
non_negative_index: index >= 0
index_small_enough: index <= count + 1
off_definition: off = ((index = 0) or (index = count + 1))
isfirst_definition: isfirst = ((not is_empty) and (index = 1))
islast_definition: islast = ((not is_empty) and (index = count))
item_corresponds_to_index: (not off) implies (item = i_th (index))
index_set_has_same_count: index_set.count = count
ACTIVE
writable_constraint: writable implies readable
empty_constraint: is_empty implies (not readable) and (not writable)
BILINEAR
not_both: not (after and before)
before_constraint: before implies off
LINEAR
after_constraint: after implies off
TRAVERSABLE
empty_constraint: is_empty implies off
DYNAMIC_CHAIN
extendible: extendible
indexing
library: "EiffelBase: Library of reusable components for Eiffel."
copyright: "Copyright (c) 1984-2006, Eiffel Software and others"
license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)"
source: "[
Eiffel Software
356 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Website http://www.eiffel.com
Customer support http://support.eiffel.com
]"
end ACTION_SEQUENCE