indexing
description: "[
Trees where each node has a fixed number of children
(The number of children is arbitrary but cannot be
changed once the node has been created
]"
names: fixed_tree, tree, fixed_list
representation: recursive, array
access: cursor, membership
contents: generic
date: "$Date$"
revision: "$Revision$"
class interface
FIXED_TREE [G]
create
make (n: INTEGER; v: G)
nv
require
valid_number_of_children: n >= 0
ensure
node_item: item = v
node_arity: arity = n
feature
make (n: INTEGER; v: G)
nv
require
valid_number_of_children: n >= 0
ensure
node_item: item = v
node_arity: arity = n
feature
child_item: like item
require TREE
readable: child_readable
child_cursor: CURSOR
FIXED_LIST
first_child: like parent
require CHAIN
not_empty: not is_leaf
require TREE
is_not_leaf: not is_leaf
child_index: INTEGER
FIXED_LIST
index_of (v: like child; i: INTEGER): INTEGER
iv
object_comparison
CHAIN
require LINEAR
positive_occurrences: i > 0
ensure LINEAR
non_negative_result: Result >= 0
item: G
CELL
child: FIXED_TREE [G]
FIXED_LIST
require TRAVERSABLE
not_off: not child_off
require ACTIVE
readable: fl_readable
require TREE
readable: readable_child
last_child: like first_child
FIXED_LIST
require CHAIN
not_empty: not is_leaf
require TREE
is_not_leaf: not is_leaf
left_sibling: like parent
require TREE
is_not_root: not is_root
ensure TREE
is_sibling: Result /= void implies is_sibling (Result)
right_is_current: (Result /= void) implies (Result.right_sibling = Current)
sequential_occurrences (v: FIXED_TREE [G]): INTEGER
v
object_comparison
LINEAR
ensure BAG
non_negative_occurrences: Result >= 0
parent: FIXED_TREE [G]
right_sibling: like parent
require TREE
is_not_root: not is_root
ensure TREE
is_sibling: Result /= void implies is_sibling (Result)
left_is_current: (Result /= void) implies (Result.left_sibling = Current)
infix "@" (i: INTEGER): FIXED_TREE [G]
i
ARRAYitem
ARRAY
require TABLE
valid_key: valid_index (k)
feature
area: SPECIAL [FIXED_TREE [G]]
TO_SPECIAL
feature
capacity: INTEGER
ARRAYcount
ARRAY
ensure then ARRAY
consistent_with_bounds: Result = upper - lower + 1
child_capacity: INTEGER
TREE
count: INTEGER
TREE
arity: INTEGER
FIXED_LIST
index_set: INTEGER_INTERVAL
CHAIN
ensure INDEXABLE
not_void: Result /= void
ensure then CHAIN
count_definition: Result.count = arity
occurrences (v: FIXED_TREE [G]): INTEGER
v
ARRAY
ensure BAG
non_negative_occurrences: Result >= 0
feature
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
feature
child_after: BOOLEAN
LIST
child_before: BOOLEAN
LIST
changeable_comparison_criterion: BOOLEAN
object_comparison
CONTAINER
fl_changeable_object_criterion: BOOLEAN
object_comparison
CONTAINER
child_contractable: BOOLEAN
ensure
Result = not child_off
child_isfirst: BOOLEAN
TREE
ensure CHAIN
valid_position: Result implies not is_leaf
ensure TREE
not_is_leaf: Result implies not is_leaf
child_islast: BOOLEAN
TREE
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
child_writable: BOOLEAN
child_item
TREE
exhausted: BOOLEAN
LINEAR
ensure LINEAR
exhausted_when_off: child_off implies Result
Full: BOOLEAN is True
has (v: G): BOOLEAN
v
object_comparison
TREE
ensure CONTAINER
not_found_in_empty: Result implies not is_leaf
is_empty: BOOLEAN
TREE
is_inserted (v: FIXED_TREE [G]): BOOLEAN
v
COLLECTION
is_leaf: BOOLEAN
TREE
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
fl_object_comparison: BOOLEAN
equal=
=
CONTAINER
child_off: BOOLEAN
CHAIN
prunable: BOOLEAN
FIXED_LIST
Readable: BOOLEAN is True
TREE
readable_child: BOOLEAN
TREE
Resizable: BOOLEAN is False
capacity
FIXED
valid_cursor (p: CURSOR): BOOLEAN
p
FIXED_LIST
valid_cursor_index (i: INTEGER): BOOLEAN
i
TREE
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): BOOLEAN
i
ARRAY
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
ensure CONTAINER
object_comparison
compare_references
=
equal
CONTAINER
require CONTAINER
changeable_comparison_criterion
ensure CONTAINER
reference_comparison: not object_comparison
feature
child_back
FIXED_LIST
require TREE
True
require BILINEAR
not_before: not child_before
child_finish
FIXED_LIST
ensure then CHAIN
at_last: not is_leaf implies child_islast
ensure then TREE
is_last_child: not is_leaf implies child_islast
child_forth
FIXED_LIST
require TREE
True
require LINEAR
not_after: not child_after
ensure then LIST
moved_forth: child_index = old child_index + 1
child_go_i_th (i: INTEGER)
i
FIXED_LIST
require CHAIN
valid_cursor_index: valid_cursor_index (i)
require else TREE
valid_cursor_index: valid_cursor_index (i)
ensure CHAIN
position_expected: child_index = i
ensure then TREE
position: child_index = i
child_go_to (p: CURSOR)
p
FIXED_LIST
require TREE
True
require CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER)
i
FIXED_LIST
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)
search_child (v: like child)
itemv
v
exhausted
object_comparison
BILINEAR
ensure LINEAR
object_found: (not exhausted and object_comparison) implies equal (v, child)
item_found: (not exhausted and not object_comparison) implies v = child
child_start
FIXED_LIST
ensure then CHAIN
at_first: not is_leaf implies child_isfirst
ensure then TREE
is_first_child: not is_leaf implies child_isfirst
feature
append (s: SEQUENCE [FIXED_TREE [G]])
s
SEQUENCE
require SEQUENCE
argument_not_void: s /= void
ensure SEQUENCE
new_count: arity >= old arity
child_put (v: like item)
v
FIXED_TREEchild_replace
require TREE
child_writable: child_writable
ensure TREE
item_inserted: child_item = v
child_replace (v: like item)
v
FIXED_TREEchild_put
require TREE
child_writable: child_writable
ensure TREE
item_inserted: child_item = v
extend (v: like child)
v
FIXED_LIST
require COLLECTION
extendible: fl_extendible
ensure COLLECTION
item_inserted: is_inserted (v)
ensure then BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
fill (other: TREE [G])
other
other
TREE
put (v: like item)
vitem
CELLreplace
CELL
require TREE
is_writable: writable
ensure TREE
item_inserted: item = v
ensure CELL
item_inserted: item = v
put_i_th (v: like array_item; i: INTEGER)
iv
ARRAY
require TABLE
valid_key: valid_index (k)
ensure then INDEXABLE
insertion_done: array_item (k) = v
put_child (n: like parent)
n
FIXED_TREEreplace_child
ensure then
child_replaced: n.parent = Current
put_left (v: like item)
v
require
is_not_root: not is_root
has_left_sibling: left_sibling /= void
ensure
item_put: left_sibling.item = v
put_left_sibling (other: like parent)
other
require
is_not_root: not is_root
has_left_sibling: left_sibling /= void
ensure
left_sibling_replaced: left_sibling = other
put_right (v: like item)
v
require
is_not_root: not is_root
has_right_sibling: right_sibling /= void
ensure
item_put: right_sibling.item = v
put_right_sibling (other: like parent)
other
require
is_not_root: not is_root
has_right_sibling: right_sibling /= void
ensure
right_sibling_replaced: right_sibling = other
replace (v: like item)
vitem
CELLput
CELL
require TREE
is_writable: writable
ensure TREE
item_inserted: item = v
ensure CELL
item_inserted: item = v
replace_child (n: like parent)
n
FIXED_TREEput_child
require TREE
writable_child: writable_child
was_root: n.is_root
ensure TREE
child_replaced: child = n
ensure then
child_replaced: n.parent = Current
sprout
TREE
feature
remove_child
ensure then
child_removed: child = void
feature
swap (i: INTEGER)
i
FIXED_LIST
require CHAIN
not_off: not child_off
valid_index: valid_index (i)
ensure CHAIN
swapped_to_item: child = old array_item (i)
swapped_from_item: array_item (i) = old child
feature
binary_representation: BINARY_TREE [G]
TREE
ensure TREE
result_is_root: Result.is_root
result_has_no_right_child: not Result.has_right
linear_representation: LINEAR [G]
TREE
feature
copy (other: like Current)
other
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)
duplicate (n: INTEGER): like Current
naritychild_index
require CHAIN
not_off_unless_after: child_off implies child_after
valid_subchain: n >= 0
require TREE
not_child_off: not child_off
valid_sublist: n >= 0
feature
prune (v: FIXED_TREE [G])
v
ARRAY
require COLLECTION
prunable: prunable
require TREE
is_child: n.parent = Current
ensure TREE
n_is_root: n.is_root
feature
do_all (action: PROCEDURE [ANY, TUPLE [FIXED_TREE [G]]])
action
action
LINEAR
require TRAVERSABLE
action_exists: action /= void
do_if (action: PROCEDURE [ANY, TUPLE [FIXED_TREE [G]]]; test: FUNCTION [ANY, TUPLE [FIXED_TREE [G]], BOOLEAN])
actiontest
actiontest
LINEAR
require TRAVERSABLE
action_exists: action /= void
test_exits: test /= void
for_all (test: FUNCTION [ANY, TUPLE [FIXED_TREE [G]], BOOLEAN]): BOOLEAN
test
LINEAR
require TRAVERSABLE
test_exits: test /= void
there_exists (test: FUNCTION [ANY, TUPLE [FIXED_TREE [G]], BOOLEAN]): BOOLEAN
test
LINEAR
require TRAVERSABLE
test_exits: test /= void
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
TREE
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)
child_consistency: child_readable implies child.parent = Current
FIXED_LIST
empty_means_storage_empty: is_leaf implies all_default
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 = array_item (child_index))
index_set_has_same_count: index_set.count = arity
ACTIVE
writable_constraint: fl_writable implies fl_readable
empty_constraint: is_leaf implies (not fl_readable) and (not fl_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
ARRAY
area_exists: area /= void
consistent_size: capacity = upper - lower + 1
non_negative_count: arity >= 0
index_set_has_same_count: valid_index_set
RESIZABLE
increase_by_at_least_one: minimal_increase >= 1
BOUNDED
valid_count: arity <= capacity
full_definition: fl_full = (arity = capacity)
FIXED
not_resizable: not resizable
indexing
library: "[
EiffelBase: Library of reusable components for Eiffel.
]"
status: "[
Copyright 1986-2001 Interactive Software Engineering (ISE).
For ISE customers the original versions are an ISE product
covered by the ISE Eiffel license and support agreements.
]"
license: "[
EiffelBase may now be used by anyone as FREE SOFTWARE to
develop any product, public-domain or commercial, without
payment to ISE, under the terms of the ISE Free Eiffel Library
License (IFELL) at http://eiffel.com/products/base/license.html.
]"
source: "[
Interactive Software Engineering Inc.
ISE Building
360 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Electronic mail <info@eiffel.com>
Customer support http://support.eiffel.com
]"
info: "[
For latest info see award-winning pages: http://eiffel.com
]"
end -- FIXED_TREE