indexing
description: "Terminal constructs with just one specimen, representing a language keyword or special symbol"
legal: "See notice at end of class."
status: "See notice at end of class."
date: "$Date: 2006-01-22 18:25:44 -0800 (Sun, 22 Jan 2006) $"
revision: "$Revision: 56675 $"
class interface
KEYWORD
create
make (s: STRING_8)
`s'
ensure
construct_name = s
lex_code = document.keyword_code (s)
feature
make (s: STRING_8)
`s'
ensure
construct_name = s
lex_code = document.keyword_code (s)
construct_make
CONSTRUCT
feature
child_cursor: TWO_WAY_TREE_CURSOR [CONSTRUCT]
TWO_WAY_TREE
require CURSOR_STRUCTURE
True
require TREE
True
ensure CURSOR_STRUCTURE
cursor_not_void: Result /= Void
construct_name: STRING_8
document: INPUT
CONSTRUCT
first: like child_item
LINKED_LIST
require CHAIN
not_empty: not is_leaf
first_child: like parent
TWO_WAY_TREE
generating_type: STRING_8
ANY
generator: STRING_8
ANY
i_th alias "[]" (i: INTEGER_32): like child_item assign put_i_th
`i'
CHAINinfix "@"
CHAIN
require TABLE
valid_key: valid_index (i)
child_index: INTEGER_32
LINKED_LIST
require LINEAR
True
require TREE
True
ensure TREE
valid_index: Result >= 0 and Result <= arity + 1
index_of (v: like child_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: CONSTRUCT
CELL
child_item: CONSTRUCT
LINKED_LIST
require TRAVERSABLE
not_off: not child_off
require ACTIVE
readable: child_readable
require TREE
readable: child_readable
last: like child_item
LINKED_LIST
require CHAIN
not_empty: not is_leaf
last_child: like parent
TWO_WAY_TREE
left_sibling: like Current
BI_LINKABLE
lex_code: INTEGER_32
sequential_occurrences (v: like child_item): INTEGER_32
`v'
object_comparison
LINEAR
require BAG
True
ensure BAG
non_negative_occurrences: Result >= 0
right_sibling: like Current
LINKABLE
sublist: like Current
split
TWO_WAY_LIST
token: TOKEN
TERMINAL
infix "@" (i: INTEGER_32): like child_item assign put_i_th
`i'
CHAINi_th
CHAIN
require TABLE
valid_key: valid_index (i)
feature
child_capacity: INTEGER_32
TREE
count: INTEGER_32
TREE
arity: INTEGER_32
LINKED_LIST
index_set: INTEGER_INTERVAL
CHAIN
require INDEXABLE
True
ensure INDEXABLE
not_void: Result /= Void
ensure then CHAIN
count_definition: Result.count = arity
occurrences (v: like child_item): INTEGER_32
`v'
object_comparison
CHAIN
require BAG
True
require LINEAR
True
ensure BAG
non_negative_occurrences: Result >= 0
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'
object_comparison
TREE
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: child_index = old child_index and other.child_index = old other.child_index
true_implies_same_size: Result implies arity = other.arity
node_is_equal (other: like Current): BOOLEAN
`other'
TREE
require TREE
other_not_void: other /= Void
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
child_after: BOOLEAN
LINKED_LIST
child_before: BOOLEAN
LINKED_LIST
changeable_comparison_criterion: BOOLEAN
object_comparison
CONTAINER
child_isfirst: BOOLEAN
TREE
require CHAIN
True
ensure CHAIN
valid_position: Result implies not is_leaf
ensure TREE
not_is_leaf: Result implies not is_leaf
child_islast: BOOLEAN
TWO_WAY_TREE
require CHAIN
True
require TREE
True
ensure CHAIN
valid_position: Result implies not is_leaf
ensure TREE
not_is_leaf: Result implies not is_leaf
child_readable: BOOLEAN
child_item
TREE
require ACTIVE
True
child_writable: BOOLEAN
child_item
TREE
require ACTIVE
True
committed: BOOLEAN
CONSTRUCT
conforms_to (other: ANY): BOOLEAN
`other'
ANY
require ANY
other_not_void: other /= Void
exhausted: BOOLEAN
LINEAR
ensure LINEAR
exhausted_when_off: child_off implies Result
child_extendible: BOOLEAN is True
DYNAMIC_CHAIN
extendible: BOOLEAN is True
DYNAMIC_TREE
has (v: CONSTRUCT): BOOLEAN
`v'
object_comparison
TREE
ensure CONTAINER
not_found_in_empty: Result implies not is_leaf
is_empty: BOOLEAN
TREE
is_inserted (v: CONSTRUCT): BOOLEAN
`v'put
extend
LINKED_LIST
is_leaf: BOOLEAN
TREE
require CONTAINER
True
is_optional: BOOLEAN
CONSTRUCT
is_root: BOOLEAN
TREE
is_sibling (other: like parent): BOOLEAN
`other'
TREE
require TREE
other_exists: other /= Void
ensure TREE
not_root: Result implies not is_root
other_not_root: Result implies not other.is_root
same_parent: Result = not is_root and other.parent = parent
object_comparison: BOOLEAN
equal`='
`='
CONTAINER
child_off: BOOLEAN
LINKED_LIST
require TRAVERSABLE
True
require TREE
True
parsed: BOOLEAN
CONSTRUCT
print_mode: CELL [BOOLEAN]
CONSTRUCT
prunable: BOOLEAN
DYNAMIC_CHAIN
require COLLECTION
True
readable: BOOLEAN is True
TREE
readable_child: BOOLEAN
TREE
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))
valid_cursor (p: CURSOR): BOOLEAN
`p'
LINKED_LIST
valid_cursor_index (i: INTEGER_32): BOOLEAN
`i'
TREE
require CHAIN
True
ensure CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= arity + 1))
ensure TREE
valid_cursor_index_definition: Result = (i >= 0) and (i <= child_capacity + 1)
valid_index (i: INTEGER_32): BOOLEAN
`i'
CHAIN
require TABLE
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 <= arity))
writable: BOOLEAN is True
TREE
writable_child: BOOLEAN
TREE
feature
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
set_optional
CONSTRUCT
ensure CONSTRUCT
optional_construct: is_optional
feature
child_back
TWO_WAY_LIST
require BILINEAR
not_before: not child_before
require TREE
True
child_finish
TWO_WAY_LIST
require LINEAR
True
require TREE
True
ensure then CHAIN
at_last: not is_leaf implies child_islast
ensure then LINKED_LIST
empty_convention: is_leaf implies child_before
ensure then TWO_WAY_LIST
not_after: not child_after
child_forth
TWO_WAY_LIST
require LINEAR
not_after: not child_after
require TREE
True
ensure then LIST
moved_forth: child_index = old child_index + 1
child_go_i_th (i: INTEGER_32)
`i'
LINKED_LIST
require CHAIN
valid_cursor_index: valid_cursor_index (i)
require TREE
True
ensure CHAIN
position_expected: child_index = i
ensure then TREE
position: child_index = i
child_go_to (p: CURSOR)
`p'
LINKED_LIST
require CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
require TREE
True
move (i: INTEGER_32)
`i'
`off'
TWO_WAY_LIST
require CHAIN
True
ensure CHAIN
too_far_right: (old child_index + i > arity) implies exhausted
too_far_left: (old child_index + i < 1) implies exhausted
expected_index: (not exhausted) implies (child_index = old child_index + i)
ensure then LINKED_LIST
moved_if_inbounds: ((old child_index + i) >= 0 and (old child_index + i) <= (arity + 1)) implies child_index = (old child_index + i)
before_set: (old child_index + i) <= 0 implies child_before
after_set: (old child_index + i) >= (arity + 1) implies child_after
search_child (v: like child_item)
item`v'
`v'
exhausted
object_comparison
BILINEAR
ensure LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, child_item)
item_found: (not exhausted and not object_comparison) implies v = child_item
child_start
LINKED_LIST
require TRAVERSABLE
True
require TREE
True
ensure then CHAIN
at_first: not is_leaf implies child_isfirst
ensure then LINKED_LIST
empty_convention: is_leaf implies child_after
feature
append (s: SEQUENCE [CONSTRUCT])
`s'
CHAIN
require SEQUENCE
argument_not_void: s /= Void
ensure SEQUENCE
new_count: arity >= old arity
extend (v: like item)
`v'
DYNAMIC_TREE
child_extend (v: like child_item)
`v'
TWO_WAY_LIST
require COLLECTION
extendible: child_extendible
require DYNAMIC_TREE
True
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
fill (other: TREE [CONSTRUCT])
`other'
`other'
TREE
force (v: like child_item)
`v'
SEQUENCE
require SEQUENCE
extendible: child_extendible
ensure then SEQUENCE
new_count: arity = old arity + 1
item_inserted: has (v)
twl_merge_left (other: like Current)
`other'
`other'
TWO_WAY_LIST
require DYNAMIC_CHAIN
extendible: child_extendible
not_before: not child_before
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: arity = old arity + old other.arity
new_index: child_index = old child_index + old other.arity
other_is_empty: other.is_leaf
twl_merge_right (other: like Current)
`other'
`other'
TWO_WAY_LIST
require DYNAMIC_CHAIN
extendible: child_extendible
not_after: not child_after
other_exists: other /= Void
not_current: other /= Current
ensure DYNAMIC_CHAIN
new_count: arity = old arity + old other.arity
same_index: child_index = old child_index
other_is_empty: other.is_leaf
merge_tree_after (other: like first_child)
`other'
`other'
TWO_WAY_TREE
require DYNAMIC_TREE
not_child_off: not child_off
other_exists: (other /= Void)
ensure DYNAMIC_TREE
other_is_leaf: other.is_leaf
merge_tree_before (other: like first_child)
`other'
`other'
TWO_WAY_TREE
require DYNAMIC_TREE
not_child_off: not child_off
other_exists: (other /= Void)
ensure DYNAMIC_TREE
other_is_leaf: other.is_leaf
prune (n: like first_child)
`n'
TWO_WAY_TREE
require TREE
is_child: n.parent = Current
ensure TREE
n_is_root: n.is_root
child_put (v: like child_item)
`v'
replace
CHAIN
require COLLECTION
extendible: child_extendible
require TREE
child_writable: child_writable
ensure COLLECTION
item_inserted: is_inserted (v)
ensure TREE
item_inserted: child_item = v
ensure then CHAIN
same_count: arity = old arity
put_child (n: like parent)
`n'
TWO_WAY_TREE
require TREE
non_void_argument: n /= Void
put_child_left (n: like parent)
`n'
TWO_WAY_TREE
require DYNAMIC_TREE
not_child_before: not child_before
non_void_argument: n /= Void
put_child_right (n: like parent)
`n'
TWO_WAY_TREE
require DYNAMIC_TREE
not_child_after: not child_after
non_void_argument: n /= Void
put_front (v: like child_item)
`v'
TWO_WAY_LIST
require DYNAMIC_CHAIN
True
ensure DYNAMIC_CHAIN
new_count: arity = old arity + 1
item_inserted: first = v
put_i_th (v: like child_item; i: INTEGER_32)
`v'`i'
CHAIN
require TABLE
valid_key: valid_index (i)
ensure then INDEXABLE
insertion_done: i_th (i) = v
child_put_left (v: like child_item)
`v'
TWO_WAY_LIST
require DYNAMIC_CHAIN
extendible: child_extendible
not_before: not child_before
require DYNAMIC_TREE
not_child_before: not child_before
ensure DYNAMIC_CHAIN
new_count: arity = old arity + 1
new_index: child_index = old child_index + 1
ensure then LINKED_LIST
previous_exists: previous /= Void
item_inserted: previous.item = v
child_put_right (v: like child_item)
`v'
TWO_WAY_LIST
require DYNAMIC_CHAIN
extendible: child_extendible
not_after: not child_after
require DYNAMIC_TREE
not_child_after: not child_after
ensure DYNAMIC_CHAIN
new_count: arity = old arity + 1
same_index: child_index = old child_index
ensure then LINKED_LIST
next_exists: next /= Void
item_inserted: not old child_before implies next.item = v
item_inserted_before: old child_before implies child.item = v
replace (v: like item)
`v'item
CELLput
CELL
require TREE
is_writable: writable
ensure TREE
item_inserted: item = v
ensure CELL
item_inserted: item = v
child_replace (v: like child_item)
`v'
LINKED_LIST
require ACTIVE
writable: child_writable
require TREE
child_writable: child_writable
ensure ACTIVE
item_replaced: child_item = v
ensure TREE
item_inserted: child_item = v
replace_child (n: like parent)
`n'
TWO_WAY_TREE
require TREE
writable_child: writable_child
ensure TREE
child_replaced: child = n
sprout
TREE
feature
twl_prune (v: like child_item)
`v'
exhausted
DYNAMIC_CHAIN
require COLLECTION
prunable: prunable
prune_all (v: like child_item)
`v'
object_comparison
exhausted
DYNAMIC_CHAIN
require COLLECTION
prunable: prunable
ensure COLLECTION
no_more_occurrences: not has (v)
ensure then DYNAMIC_CHAIN
is_exhausted: exhausted
remove_child
`after'
TWO_WAY_LIST
require ACTIVE
prunable: prunable
writable: child_writable
require DYNAMIC_TREE
child_not_off: not child_off
ensure then DYNAMIC_LIST
after_when_empty: is_leaf implies child_after
ensure DYNAMIC_TREE
new_arity: arity = old arity - 1
new_child_index: child_index = old child_index
remove_left_child
TWO_WAY_LIST
require DYNAMIC_CHAIN
left_exists: child_index > 1
require DYNAMIC_TREE
is_not_first: not child_isfirst
ensure DYNAMIC_CHAIN
new_count: arity = old arity - 1
new_index: child_index = old child_index - 1
ensure DYNAMIC_TREE
new_arity: arity = old arity - 1
new_child_index: child_index = old child_index - 1
remove_right_child
TWO_WAY_LIST
require DYNAMIC_CHAIN
right_exists: child_index < arity
require DYNAMIC_TREE
is_not_last: not child_islast
ensure DYNAMIC_CHAIN
new_count: arity = old arity - 1
same_index: child_index = old child_index
ensure DYNAMIC_TREE
new_arity: arity = old arity - 1
new_child_index: child_index = old child_index
remove_sublist
TWO_WAY_LIST
split (n: INTEGER_32)
`n'count`index'
sublist
TWO_WAY_LIST
require TWO_WAY_LIST
not_off: not child_off
valid_sublist: n >= 0
wipe_out
TWO_WAY_LIST
require COLLECTION
prunable: prunable
require TREE
True
ensure COLLECTION
wiped_out: is_leaf
ensure then DYNAMIC_LIST
is_before: child_before
ensure TREE
is_leaf: is_leaf
feature
commit
CONSTRUCT
parse
parsed
CONSTRUCT
unused_pre_action
CONSTRUCT
process
CONSTRUCT
semantics
`pre_action'in_action`post_action'
CONSTRUCT
swap (i: INTEGER_32)
`i'
CHAIN
require CHAIN
not_off: not child_off
valid_index: valid_index (i)
ensure CHAIN
swapped_to_item: child_item = old i_th (i)
swapped_from_item: i_th (i) = old child_item
feature
binary_representation: BINARY_TREE [CONSTRUCT]
TREE
ensure TREE
result_is_root: Result.is_root
result_has_no_right_child: not Result.has_right
fill_from_binary (b: BINARY_TREE [CONSTRUCT])
`b'
DYNAMIC_TREE
linear_representation: LINEAR [CONSTRUCT]
TREE
require CONTAINER
True
feature
copy (other: like Current)
`other'
TREE
require ANY
other_not_void: other /= Void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
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'aritychild_index
DYNAMIC_TREE
require TREE
not_child_off: not child_off
valid_sublist: 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
frozen default: like Current
ANY
frozen default_pointer: POINTER
`POINTER'
`p'default
`p'`POINTER'
ANY
default_rescue
ANY
frozen do_nothing
ANY
feature
child: like first_child
LINKED_LIST
forget_left
BI_LINKABLE
require TREE
True
ensure BI_LINKABLE
left_not_chained: left_sibling = Void or else (old left_sibling /= Void) implies ((old left_sibling).right_sibling = Void)
forget_right
BI_LINKABLE
require LINKABLE
True
require TREE
True
ensure LINKABLE
not_chained: right_sibling = Void
ensure then BI_LINKABLE
right_not_chained: (old right_sibling /= Void) implies ((old right_sibling).left_sibling = Void)
feature
do_all (action: PROCEDURE [ANY, TUPLE [CONSTRUCT]])
action
action
LINEAR
require TRAVERSABLE
action_exists: action /= Void
do_if (action: PROCEDURE [ANY, TUPLE [CONSTRUCT]]; test: FUNCTION [ANY, TUPLE [CONSTRUCT], BOOLEAN])
action`test'
action`test'
LINEAR
require TRAVERSABLE
action_exists: action /= Void
test_exits: test /= Void
for_all (test: FUNCTION [ANY, TUPLE [CONSTRUCT], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: test /= Void
ensure then LINEAR
empty: is_leaf implies Result
there_exists (test: FUNCTION [ANY, TUPLE [CONSTRUCT], BOOLEAN]): BOOLEAN
`test'
`test'
LINEAR
require TRAVERSABLE
test_exits: 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
print_name
CONSTRUCT
feature
operating_environment: OPERATING_ENVIRONMENT
ANY
invariant
TWO_WAY_TREE
off_constraint: (child = Void) implies child_off
DYNAMIC_TREE
extendible_definition: extendible
child_after_definition: child_after = (child_index = arity + 1)
TREE
tree_consistency: child_readable implies child.parent = Current
leaf_definition: is_leaf = (arity = 0)
child_off_definition: child_off = child_before or child_after
child_before_definition: child_before = (child_index = 0)
child_isfirst_definition: child_isfirst = (not is_leaf and child_index = 1)
child_islast_definition: child_islast = (not is_leaf and child_index = child_capacity)
child_after_definition: child_after = (child_index >= child_capacity + 1)
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
BI_LINKABLE
right_symmetry: (right_sibling /= Void) implies (right_sibling.left_sibling = Current)
left_symmetry: (left_sibling /= Void) implies (left_sibling.right_sibling = Current)
TWO_WAY_LIST
non_empty_list_has_two_endpoints: not is_leaf implies (first_child /= Void and last_child /= Void)
first_element_constraint: first_child /= Void implies first_child.left_sibling = Void
last_element_constraint: last_child /= Void implies last_child.right_sibling = Void
LINKED_LIST
prunable: prunable
empty_constraint: is_leaf implies ((first_child = Void) and (child = Void))
not_void_unless_empty: (child = Void) implies is_leaf
before_constraint: child_before implies (child = first_child)
after_constraint: child_after implies (child = last_child)
LIST
before_definition: child_before = (child_index = 0)
after_definition: child_after = (child_index = arity + 1)
CHAIN
non_negative_index: child_index >= 0
index_small_enough: child_index <= arity + 1
off_definition: child_off = ((child_index = 0) or (child_index = arity + 1))
isfirst_definition: child_isfirst = ((not is_leaf) and (child_index = 1))
islast_definition: child_islast = ((not is_leaf) and (child_index = arity))
item_corresponds_to_index: (not child_off) implies (child_item = i_th (child_index))
index_set_has_same_count: index_set.count = arity
ACTIVE
writable_constraint: child_writable implies child_readable
empty_constraint: is_leaf implies (not child_readable) and (not child_writable)
INDEXABLE
index_set_not_void: index_set /= Void
BILINEAR
not_both: not (child_after and child_before)
before_constraint: child_before implies child_off
LINEAR
after_constraint: child_after implies child_off
TRAVERSABLE
empty_constraint: is_leaf implies child_off
FINITE
empty_definition: is_leaf = (arity = 0)
non_negative_count: arity >= 0
DYNAMIC_CHAIN
extendible: child_extendible
indexing
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 KEYWORD