indexing
description: "Menu bar containing drop down menus. See EV_MENU."
status: "See notice at end of class"
keywords: "menu, bar, item, file, edit, help"
date: "$Date$"
revision: "$Revision$"
class interface
EV_MENU_BAR
create
frozen default_create
EV_ANY
ensure then EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state
feature
frozen default_create
EV_ANY
ensure then EV_ANY
is_coupled: implementation /= void
is_initialized: is_initialized
default_create_called_set: default_create_called
is_in_default_state: is_in_default_state
feature
cursor: EV_DYNAMIC_LIST_CURSOR [EV_MENU_ITEM]
EV_DYNAMIC_LIST
ensure then EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.cursor)
data: ANY
EV_ANY
first: like item
CHAIN
require CHAIN
not_empty: not is_empty
has (v: like item): BOOLEAN
v
object_comparison
CHAIN
ensure CONTAINER
not_found_in_empty: Result implies not is_empty
i_th (i: INTEGER): EV_MENU_ITEM
i
EV_DYNAMIC_LIST
require TABLE
valid_key: valid_index (k)
ensure then EV_DYNAMIC_LIST
bridge_ok: Result.is_equal (implementation.i_th (i))
index: INTEGER
EV_DYNAMIC_LIST
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.index
index_of (v: like item; i: INTEGER): INTEGER
iv
EV_DYNAMIC_LIST
require LINEAR
positive_occurrences: i > 0
ensure LINEAR
non_negative_result: Result >= 0
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.index_of (v, i)
item: EV_MENU_ITEM
EV_DYNAMIC_LIST
require TRAVERSABLE
not_off: not off
require ACTIVE
readable: readable
ensure then EV_DYNAMIC_LIST
not_void: Result /= void
bridge_ok: Result.is_equal (implementation.item)
item_by_data (some_data: ANY): like item
some_data
EV_ITEM_LIST
require EV_ITEM_LIST
not_destroyed: not is_destroyed
data_not_void: some_data /= void
ensure EV_ITEM_LIST
bridge_ok: Result = implementation.item_by_data (some_data)
last: like item
CHAIN
require CHAIN
not_empty: not is_empty
sequential_occurrences (v: EV_MENU_ITEM): INTEGER
v
object_comparison
LINEAR
ensure BAG
non_negative_occurrences: Result >= 0
infix "@" (i: INTEGER): like item
i
CHAINi_th
CHAIN
require TABLE
valid_key: valid_index (k)
feature
count: INTEGER
EV_DYNAMIC_LIST
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.count
index_set: INTEGER_INTERVAL
CHAIN
ensure INDEXABLE
not_void: Result /= void
ensure then CHAIN
count_definition: Result.count = count
occurrences (v: like item): INTEGER
v
object_comparison
CHAIN
ensure BAG
non_negative_occurrences: Result >= 0
occurrences (v: like item): INTEGER
v
object_comparison
CHAIN
ensure BAG
non_negative_occurrences: Result >= 0
feature
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
feature
after: BOOLEAN
LIST
before: BOOLEAN
LIST
exhausted: BOOLEAN
LINEAR
ensure LINEAR
exhausted_when_off: off implies Result
Extendible: BOOLEAN is True
DYNAMIC_CHAIN
Full: BOOLEAN is False
EV_DYNAMIC_LIST
is_empty: BOOLEAN
FINITE
is_inserted (v: EV_MENU_ITEM): BOOLEAN
v
COLLECTION
isfirst: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
islast: BOOLEAN
CHAIN
ensure CHAIN
valid_position: Result implies not is_empty
object_comparison: BOOLEAN
equal=
=
CONTAINER
off: BOOLEAN
CHAIN
parent: EV_WINDOW
Current
prunable: BOOLEAN
DYNAMIC_CHAIN
readable: BOOLEAN
SEQUENCE
valid_cursor (p: CURSOR): BOOLEAN
p
pEV_DYNAMIC_LIST_CURSOR
Current
EV_DYNAMIC_LIST
ensure then EV_DYNAMIC_LIST
bridge_ok: Result = implementation.valid_cursor (p)
valid_cursor_index (i: INTEGER): BOOLEAN
i
CHAIN
ensure CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))
valid_index (i: INTEGER): BOOLEAN
i
CHAIN
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
feature
compare_objects
equal
=
CONTAINER
require CONTAINER
changeable_comparison_criterion
ensure CONTAINER
object_comparison
compare_references
=
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
feature
back
EV_DYNAMIC_LIST
require BILINEAR
not_before: not before
finish
CHAIN
ensure then CHAIN
at_last: not is_empty implies islast
forth
EV_DYNAMIC_LIST
require LINEAR
not_after: not after
ensure then LIST
moved_forth: index = old index + 1
go_i_th (i: INTEGER)
i
EV_DYNAMIC_LIST
require CHAIN
valid_cursor_index: valid_cursor_index (i)
ensure CHAIN
position_expected: index = i
go_to (p: CURSOR)
p
EV_DYNAMIC_LIST
require CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER)
i
EV_DYNAMIC_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)
itemv
v
exhausted
object_comparison
BILINEAR
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
EV_DYNAMIC_LIST
ensure then CHAIN
at_first: not is_empty implies isfirst
ensure then EV_DYNAMIC_LIST
empty_implies_after: is_empty implies after
feature
append (s: SEQUENCE [EV_MENU_ITEM])
s
SEQUENCE
require SEQUENCE
argument_not_void: s /= void
ensure SEQUENCE
new_count: count >= old count
extend (v: like item)
v
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_is_last: v = last
count_increased: count = old count + 1
cursor_not_moved: (index = old index) or (after and old after)
fill (other: CONTAINER [EV_MENU_ITEM])
other
other
COLLECTION
require COLLECTION
other_not_void: other /= void
extendible
force (v: like item)
v
SEQUENCE
require SEQUENCE
extendible: extendible
ensure then SEQUENCE
new_count: count = old count + 1
item_inserted: has (v)
merge_left (other: like Current)
other
other
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_before: not before
other_exists: other /= void
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
ensure then DYNAMIC_LIST
other_empty: other.is_empty
merge_right (other: like Current)
other
other
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
extendible: extendible
not_after: not after
other_exists: other /= void
ensure DYNAMIC_CHAIN
new_count: count = old count + old other.count
same_index: index = old index
other_is_empty: other.is_empty
ensure then DYNAMIC_LIST
other_empty: other.is_empty
put (v: like item)
v
replace
CHAIN
require COLLECTION
extendible: extendible
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then SET
in_set_already: old has (v) implies (count = old count)
added_to_set: not old has (v) implies (count = old count + 1)
ensure then CHAIN
same_count: count = old count
put_front (v: like item)
v
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_is_first: v = first
count_increased: count = old count + 1
cursor_not_moved: (index = old index + 1) or (before and old before)
put_i_th (v: like item; i: INTEGER)
iv
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
valid_index: i > 0 and i <= count
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
item_replaced: v = i_th (i)
not_has_old_item: not has (old i_th (i))
old_item_parent_void: (old i_th (i)).parent = void
count_same: count = old count
cursor_not_moved: index = old index
put_left (v: like item)
v
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
not_before: not before
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_at_index_plus_one: v = i_th (index - 1)
count_increased: count = old count + 1
cursor_not_moved: index = old index + 1
put_right (v: like item)
v
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
extendible: extendible
not_after: not after
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
v_at_index_plus_one: v = i_th (index + 1)
count_increased: count = old count + 1
cursor_not_moved: index = old index
replace (v: like item)
v
EV_DYNAMIC_LIST
require EV_DYNAMIC_LIST
not_destroyed: not is_destroyed
writable: writable
v_not_void: v /= void
v_parent_void: v.parent = void
v_not_current: not same (v)
v_not_parent_of_current: not is_parent_recursive (v)
ensure EV_DYNAMIC_LIST
parent_is_current: v.parent = Current
item_replaced: v = item
not_has_old_item: not has (old item)
old_item_parent_void: (old item).parent = void
count_same: count = old count
cursor_not_moved: index = old index
set_data (some_data: like data)
some_datadata
EV_ANY
require EV_ANY
not_destroyed: not is_destroyed
ensure EV_ANY
data_assigned: data = some_data
swap (i: INTEGER)
i
EV_DYNAMIC_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
prune (v: like item)
v
v
EV_DYNAMIC_LIST
require COLLECTION
prunable: prunable
ensure then SET
removed_count_change: old has (v) implies (count = old count - 1)
not_removed_no_count_change: not old has (v) implies (count = old count)
item_deleted: not has (v)
ensure then EV_DYNAMIC_LIST
not_has_v: not has (v)
had_item_implies_parent_void: old has (v) implies v.parent = void
had_item_implies_count_decreased: old has (v) implies count = old count - 1
had_item_and_was_after_implies_index_decreased: (old after and old has (v)) implies index = old index - 1
prune_all (v: like item)
v
object_comparison
exhausted
DYNAMIC_CHAIN
require COLLECTION
prunable
ensure COLLECTION
no_more_occurrences: not has (v)
ensure then DYNAMIC_CHAIN
is_exhausted: exhausted
remove
after
EV_DYNAMIC_LIST
require ACTIVE
prunable: prunable
writable: writable
ensure then DYNAMIC_LIST
after_when_empty: is_empty implies after
ensure then EV_DYNAMIC_LIST
v_removed: not has (old item)
parent_void: (old item).parent = void
count_decreased: count = old count - 1
index_same: index = old index
remove_left
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
left_exists: index > 1
require else DYNAMIC_LIST
not_before: not before
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
new_index: index = old index - 1
ensure then EV_DYNAMIC_LIST
left_neighbor_removed: not has (old i_th (index - 1))
parent_void: (old i_th (index - 1)).parent = void
index_decreased: index = old index - 1
remove_right
EV_DYNAMIC_LIST
require DYNAMIC_CHAIN
right_exists: index < count
ensure DYNAMIC_CHAIN
new_count: count = old count - 1
same_index: index = old index
ensure then EV_DYNAMIC_LIST
right_neighbor_removed: not has (old i_th (index + 1))
parent_void: (old i_th (index + 1)).parent = void
index_same: index = old index
wipe_out
EV_DYNAMIC_LIST
require COLLECTION
prunable
ensure COLLECTION
wiped_out: is_empty
ensure then DYNAMIC_LIST
is_before: before
feature
linear_representation: LINEAR [EV_MENU_ITEM]
LINEAR
feature
copy (other: like Current)
other
EV_ANY
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
feature
Changeable_comparison_criterion: BOOLEAN is False
object_comparison
EV_ITEM_LIST
feature
destroy
Current
EV_ANY
ensure EV_ANY
is_destroyed: is_destroyed
feature
same (other: EV_ANY): BOOLEAN
otherCurrent
EV_DYNAMIC_LIST
feature
item_select_actions: EV_MENU_ITEM_SELECT_ACTION_SEQUENCE
EV_MENU_ITEM_LIST_ACTION_SEQUENCES
ensure EV_MENU_ITEM_LIST_ACTION_SEQUENCES
not_void: Result /= void
feature
do_all (action: PROCEDURE [ANY, TUPLE [EV_MENU_ITEM]])
action
action
LINEAR
require TRAVERSABLE
action_exists: action /= void
do_if (action: PROCEDURE [ANY, TUPLE [EV_MENU_ITEM]]; test: FUNCTION [ANY, TUPLE [EV_MENU_ITEM], BOOLEAN])
actiontest
actiontest
LINEAR
require TRAVERSABLE
action_exists: action /= void
test_exits: test /= void
for_all (test: FUNCTION [ANY, TUPLE [EV_MENU_ITEM], BOOLEAN]): BOOLEAN
test
LINEAR
require TRAVERSABLE
test_exits: test /= void
there_exists (test: FUNCTION [ANY, TUPLE [EV_MENU_ITEM], BOOLEAN]): BOOLEAN
test
LINEAR
require TRAVERSABLE
test_exits: test /= void
feature
is_destroyed: BOOLEAN
Current
EV_ANY
ensure EV_ANY
bridge_ok: Result = implementation.is_destroyed
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
EV_MENU_ITEM_LIST
item_select_actions_not_void: is_usable implies item_select_actions /= void
EV_ITEM_LIST
parent_of_items_is_current: is_usable implies parent_of_items_is_current
items_unique: is_usable implies items_unique
EV_ANY
is_initialized: is_initialized
is_coupled: implementation /= void and then implementation.interface = Current
default_create_called: default_create_called
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)
INDEXABLE
index_set_not_void: index_set /= void
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
FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0
DYNAMIC_CHAIN
extendible: extendible
end -- EV_MENU_BAR