indexing
description: "Trees implemented using a two way linked list representation"
names: two_way_tree, tree, two_way_list
representation: recursive, linked
access: cursor, membership
contents: generic
class interface
TWO_WAY_TREE [G]
create
make (v: like item)
-- Create single node with item v.
feature -- Initialization
make (v: like item)
-- Create single node with item v.
feature -- Access
child_cursor: CURSOR
-- Current cursor position
-- (from LINKED_LIST)
first: like child_item
-- Item at first position
-- (from LINKED_LIST)
require -- from CHAIN
not_empty: not is_leaf
first_child: like parent
-- Leftmost child
has (v: G): BOOLEAN
-- Does subtree include v?
-- (Reference or object equality,
-- based on object_comparison.)
-- (from TREE)
ensure -- from CONTAINER
not_found_in_empty: Result implies not is_leaf
i_th (i: INTEGER): like child_item
-- Item at i-th position
-- Was declared in CHAIN as synonym of i_th and @.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
child_index: INTEGER
-- Index of current position
-- (from LINKED_LIST)
ensure -- from TREE
valid_index: Result >= 0 and Result <= arity + 1
index_of (v: like child_item; i: INTEGER): INTEGER
-- Index of i-th occurrence of item identical to v.
-- (Reference or object equality,
-- based on object_comparison.)
-- 0 if none.
-- (from CHAIN)
require -- from LINEAR
positive_occurrences: i > 0
ensure -- from LINEAR
non_negative_result: Result >= 0
is_sibling (other: like parent): BOOLEAN
-- Are current node and other siblings?
-- (from TREE)
ensure -- from 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
child_item: G
-- Current item
-- (from LINKED_LIST)
require -- from ACTIVE
readable: child_readable
require -- from TRAVERSABLE
not_off: not child_off
require -- from TREE
readable: child_readable
item: G
-- Content of cell.
-- (from CELL)
last: like child_item
-- Item at last position
-- (from LINKED_LIST)
require -- from CHAIN
not_empty: not is_leaf
last_child: like parent
left_sibling: like Current
-- Left neighbor
-- (from BI_LINKABLE)
sequential_occurrences (v: G): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from LINEAR)
ensure -- from BAG
non_negative_occurrences: Result >= 0
occurrences (v: like child_item): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
ensure -- from BAG
non_negative_occurrences: Result >= 0
occurrences (v: like child_item): INTEGER
-- Number of times v appears.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from CHAIN)
ensure -- from BAG
non_negative_occurrences: Result >= 0
parent: TWO_WAY_TREE [G]
-- Parent node
right_sibling: like Current
-- Right neighbor
-- (from LINKABLE)
sublist: like Current
-- Result produced by last split
-- (from TWO_WAY_LIST)
infix "@" (i: INTEGER): like child_item
-- Item at i-th position
-- Was declared in CHAIN as synonym of i_th and @.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
feature -- Measurement
count: INTEGER
-- Number of items
-- (from TREE)
arity: INTEGER
-- Number of items
-- (from LINKED_LIST)
feature -- Status report
child_after: BOOLEAN
-- Is there no valid cursor position to the right of cursor?
-- (from LINKED_LIST)
child_before: BOOLEAN
-- Is there no valid cursor position to the left of cursor?
-- (from LINKED_LIST)
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: yes by default.)
-- (from CONTAINER)
child_isfirst: BOOLEAN
-- Is cursor under first child?
-- (from TREE)
ensure -- from TREE
not_is_leaf: Result implies not is_leaf
ensure -- from CHAIN
valid_position: Result implies not is_leaf
ensure -- from TREE
not_is_leaf: Result implies not is_leaf
child_islast: BOOLEAN
-- Is cursor under last child?
-- (from TREE)
ensure -- from TREE
not_is_leaf: Result implies not is_leaf
ensure -- from CHAIN
valid_position: Result implies not is_leaf
ensure -- from TREE
not_is_leaf: Result implies not is_leaf
child_readable: BOOLEAN
-- Is there a current child_item to be read?
-- (from TREE)
child_writable: BOOLEAN
-- Is there a current child_item that may be modified?
-- (from TREE)
empty: BOOLEAN
-- Is structure empty of items?
-- (from TREE)
exhausted: BOOLEAN
-- Has structure been completely explored?
-- (from LINEAR)
ensure -- from LINEAR
exhausted_when_off: child_off implies Result
Extendible: BOOLEAN is true
-- May new items be added?
-- (from DYNAMIC_TREE)
Child_extendible: BOOLEAN is true
-- May new items be added? (Answer: yes.)
-- (from DYNAMIC_CHAIN)
is_leaf: BOOLEAN
-- Are there no children?
-- (from TREE)
is_root: BOOLEAN
-- Is there no parent?
-- (from TREE)
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
child_off: BOOLEAN
-- Is there no current item?
-- (from LINKED_LIST)
prunable: BOOLEAN
-- May items be removed? (Answer: yes.)
-- (from DYNAMIC_CHAIN)
Readable: BOOLEAN is true
-- (from TREE)
readable_child: BOOLEAN
-- Is there a current child to be read?
-- (from TREE)
valid_cursor (p: CURSOR): BOOLEAN
-- Can the cursor be moved to position p?
-- (from LINKED_LIST)
valid_cursor_index (i: INTEGER): BOOLEAN
-- Is i correctly bounded for cursor movement?
-- (from TREE)
ensure -- from TREE
valid_cursor_index_definition: Result = (i >= 0) and (i <= arity + 1)
ensure -- from CHAIN
valid_cursor_index_definition: Result = ((i >= 0) and (i <= arity + 1))
ensure -- from TREE
valid_cursor_index_definition: Result = (i >= 0) and (i <= arity + 1)
valid_index (i: INTEGER): BOOLEAN
-- Is i within allowable bounds?
-- (from CHAIN)
ensure then -- from CHAIN
valid_index_definition: Result = ((i >= 1) and (i <= arity))
Writable: BOOLEAN is true
-- Is there a current item that may be modified?
-- (from TREE)
writable_child: BOOLEAN
-- Is there a current child that may be modified?
-- (from TREE)
feature -- Status setting
compare_objects
-- Ensure that future search operations will use equal
-- rather than = for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
object_comparison
compare_references
-- Ensure that future search operations will use =
-- rather than equal for comparing references.
-- (from CONTAINER)
require -- from CONTAINER
changeable_comparison_criterion
ensure -- from CONTAINER
reference_comparison: not object_comparison
feature -- Cursor movement
child_back
-- Move cursor to previous position, if any.
-- (from TWO_WAY_LIST)
require -- from BILINEAR
not_before: not child_before
ensure then -- from BILINEAR
moved_back: child_index = old child_index - 1
child_finish
-- Move cursor to last position.
-- (Go before if empty)
-- (from TWO_WAY_LIST)
ensure then -- from CHAIN
at_last: not is_leaf implies child_islast
ensure then -- from LINKED_LIST
empty_convention: is_leaf implies child_before
ensure then -- from TWO_WAY_LIST
not_after: not child_after
ensure then -- from TREE
is_last_child: not is_leaf implies child_islast
ensure then -- from TWO_WAY_LIST
not_after: not child_after
child_forth
-- Move cursor to next position, if any.
-- (from TWO_WAY_LIST)
require -- LIST
precursor: True
require -- from LINEAR
not_after: not child_after
ensure then -- from LIST
moved_forth: child_index = old child_index + 1
child_go_i_th (i: INTEGER)
-- Move cursor to i-th position.
-- (from LINKED_LIST)
require -- from CHAIN
valid_cursor_index: valid_cursor_index (i)
require else -- from TREE
valid_cursor_index: valid_cursor_index (i)
ensure -- from CHAIN
position_expected: child_index = i
ensure then -- from TREE
position: child_index = i;
is_before: (i = 0) implies child_before;
is_after: (i = arity + 1) implies child_after
child_go_to (p: CURSOR)
-- Move cursor to position p.
-- (from LINKED_LIST)
require -- from CURSOR_STRUCTURE
cursor_position_valid: valid_cursor (p)
move (i: INTEGER)
-- Move cursor i positions. The cursor
-- may end up off if the offset is to big.
-- (from TWO_WAY_LIST)
ensure -- from 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 -- from 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)
-- Move to first position (at or after current
-- position) where item and v are equal.
-- If structure does not include v ensure that
-- exhausted will be true.
-- (Reference or object equality,
-- based on object_comparison.)
-- (from BILINEAR)
ensure -- from 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
-- Move cursor to first position.
-- (from LINKED_LIST)
ensure then -- from CHAIN
at_first: not is_leaf implies child_isfirst
ensure then -- from LINKED_LIST
empty_convention: is_leaf implies child_after
ensure then -- from TREE
is_first_child: not is_leaf implies child_isfirst
ensure then -- from LINKED_LIST
empty_convention: is_leaf implies child_after
feature -- Element change
append (s: SEQUENCE [G])
-- Append a copy of s.
-- (from SEQUENCE)
require -- from SEQUENCE
argument_not_void: s /= void
ensure -- from SEQUENCE
new_count: arity >= old arity
extend (v: like item)
-- Add v as new child.
-- (from DYNAMIC_TREE)
child_extend (v: like child_item)
-- Add v to end.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from COLLECTION
extendible: child_extendible
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from BAG
one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1
fill (other: TREE [G])
-- Fill with as many items of other as possible.
-- The representations of other and current node
-- need not be the same.
-- (from TREE)
force (v: like child_item)
-- Add v to end.
-- (from SEQUENCE)
require -- from SEQUENCE
extendible: child_extendible
ensure then -- from SEQUENCE
new_count: arity = old arity + 1;
item_inserted: has (v)
twl_merge_left (other: like Current)
-- Merge other into current structure before cursor
-- position. Do not move cursor. Empty other.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: child_extendible;
not_off: not child_before;
other_exists: other /= void
ensure -- from 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)
-- Merge other into current structure after cursor
-- position. Do not move cursor. Empty other.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: child_extendible;
not_off: not child_after;
other_exists: other /= void
ensure -- from 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)
-- Merge children of other into current structure
-- after cursor position. Do not move cursor.
-- Make other a leaf.
require -- from DYNAMIC_TREE
not_child_off: not child_off;
other_exists: (other /= void)
ensure -- from DYNAMIC_TREE
other_is_leaf: other.is_leaf
merge_tree_before (other: like first_child)
-- Merge children of other into current structure
-- after cursor position. Do not move cursor.
-- Make other a leaf.
require -- from DYNAMIC_TREE
not_child_off: not child_off;
other_exists: (other /= void)
ensure -- from DYNAMIC_TREE
other_is_leaf: other.is_leaf
prune (n: like first_child)
require -- from TREE
is_child: n.parent = Current
ensure -- from TREE
n_is_root: n.is_root
put (v: like item)
-- Make v the cell's item.
-- Was declared in CELL as synonym of put and replace.
-- (from CELL)
require -- CELL
precursor: True
require -- from TREE
is_writable: writable
ensure -- from CELL
item_inserted: item = v
ensure -- from TREE
item_inserted: item = v
ensure -- from CELL
item_inserted: item = v
child_put (v: like child_item)
-- Replace current item by v.
-- (Synonym for replace)
-- (from CHAIN)
require -- from COLLECTION
extendible: child_extendible
require -- from TREE
child_writable: child_writable
ensure -- from COLLECTION
item_inserted: has (v)
ensure then -- from CHAIN
same_count: arity = old arity
ensure -- from TREE
item_inserted: child_item = v
ensure then -- from CHAIN
same_count: arity = old arity
put_child (n: like parent)
-- Add n to the list of children.
-- Do not move child cursor.
require else -- from DYNAMIC_TREE
non_void_argument: n /= void
put_child_left (n: like parent)
-- Add n to the left of cursor position.
-- Do not move cursor.
require -- from DYNAMIC_TREE
not_child_before: not child_before;
non_void_argument: n /= void
put_child_right (n: like parent)
-- Add n to the right of cursor position.
-- Do not move cursor.
require -- from DYNAMIC_TREE
not_child_after: not child_after;
non_void_argument: n /= void
put_front (v: like child_item)
-- Add v to beginning.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
ensure -- from DYNAMIC_CHAIN
new_count: arity = old arity + 1;
item_inserted: first = v
put_i_th (v: like child_item; i: INTEGER)
-- Put v at i-th position.
-- (from CHAIN)
require -- from TABLE
valid_key: valid_index (k)
ensure then -- from INDEXABLE
insertion_done: i_th (k) = v
child_put_left (v: like child_item)
-- Add v to the left of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: child_extendible;
not_before: not child_before
require -- from DYNAMIC_TREE
not_child_before: not child_before
ensure -- from DYNAMIC_CHAIN
new_count: arity = old arity + 1;
new_index: child_index = old child_index + 1
child_put_right (v: like child_item)
-- Add v to the right of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
extendible: child_extendible;
not_after: not child_after
require -- from DYNAMIC_TREE
not_child_after: not child_after
ensure -- from DYNAMIC_CHAIN
new_count: arity = old arity + 1;
same_index: child_index = old child_index
ensure then -- from LINKED_LIST
item_inserted_before: old child_before implies child.item = v
replace (v: like item)
-- Make v the cell's item.
-- Was declared in CELL as synonym of put and replace.
-- (from CELL)
require -- CELL
precursor: True
require -- from TREE
is_writable: writable
ensure -- from CELL
item_inserted: item = v
ensure -- from TREE
item_inserted: item = v
ensure -- from CELL
item_inserted: item = v
child_replace (v: like child_item)
-- Replace current item by v.
-- (from LINKED_LIST)
require -- from ACTIVE
writable: child_writable
require -- from TREE
child_writable: child_writable
ensure -- from ACTIVE
item_replaced: child_item = v
ensure -- from TREE
item_inserted: child_item = v
replace_child (n: like parent)
-- Replace current child by n.
require -- from TREE
writable_child: writable_child;
was_root: n.is_root
ensure -- from TREE
child_replaced: child = n
sprout
-- Make current node a root.
-- (from TREE)
feature -- Removal
twl_prune (v: like child_item)
-- Remove first occurrence of v, if any,
-- after cursor position.
-- If found, move cursor to right neighbor;
-- if not, make structure exhausted.
-- (from DYNAMIC_CHAIN)
require -- from COLLECTION
prunable: prunable
prune_all (v: like child_item)
-- Remove all occurrences of v.
-- (Reference or object equality,
-- based on object_comparison.)
-- Leave structure exhausted.
-- (from DYNAMIC_CHAIN)
require -- DYNAMIC_CHAIN
precursor: True
require -- from COLLECTION
prunable
ensure then -- from DYNAMIC_CHAIN
is_exhausted: exhausted
ensure -- from COLLECTION
no_more_occurrences: not has (v)
ensure then -- from DYNAMIC_CHAIN
is_exhausted: exhausted
remove_child
-- Remove current item.
-- Move cursor to right neighbor
-- (or after if no right neighbor).
-- (from TWO_WAY_LIST)
require -- from ACTIVE
prunable: prunable;
writable: child_writable
require -- from DYNAMIC_TREE
child_not_off: not child_off
ensure then -- from DYNAMIC_LIST
after_when_empty: is_leaf implies child_after
ensure -- from DYNAMIC_TREE
new_arity: arity = old arity - 1;
new_child_index: child_index = old child_index
remove_left_child
-- Remove item to the left of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
left_exists: child_index > 1
require else -- from DYNAMIC_LIST
not_before: not child_before
require -- from DYNAMIC_TREE
is_not_first: not child_isfirst
ensure -- from DYNAMIC_CHAIN
new_count: arity = old arity - 1;
new_index: child_index = old child_index - 1
ensure -- from DYNAMIC_TREE
new_arity: arity = old arity - 1;
new_child_index: child_index = old child_index - 1
remove_right_child
-- Remove item to the right of cursor position.
-- Do not move cursor.
-- (from TWO_WAY_LIST)
require -- from DYNAMIC_CHAIN
right_exists: child_index < arity
require -- from DYNAMIC_TREE
is_not_last: not child_islast
ensure -- from DYNAMIC_CHAIN
new_count: arity = old arity - 1;
same_index: child_index = old child_index
ensure -- from DYNAMIC_TREE
new_arity: arity = old arity - 1;
new_child_index: child_index = old child_index
remove_sublist
-- (from TWO_WAY_LIST)
split (n: INTEGER)
-- Remove from current list
-- min (n, count - index - 1) items
-- starting at cursor position.
-- Move cursor right one position.
-- Make extracted sublist accessible
-- through attribute sublist.
-- (from TWO_WAY_LIST)
require -- from TWO_WAY_LIST
not_off: not child_off;
valid_sublist: n >= 0
wipe_out
-- Remove all items.
-- (from TWO_WAY_LIST)
require -- from COLLECTION
prunable
ensure -- from COLLECTION
wiped_out: is_leaf
ensure then -- from DYNAMIC_LIST
is_before: child_before
feature -- Transformation
swap (i: INTEGER)
-- Exchange item at i-th position with item
-- at cursor position.
-- (from CHAIN)
require -- from CHAIN
not_off: not child_off;
valid_index: valid_index (i)
ensure -- from CHAIN
swapped_to_item: child_item = old i_th (i);
swapped_from_item: i_th (i) = old child_item
feature -- Conversion
binary_representation: BINARY_TREE [G]
-- Convert to binary tree representation:
-- first child becomes left child,
-- right sibling becomes right child.
-- (from TREE)
ensure -- from TREE
result_is_root: Result.is_root;
result_has_no_right_child: not Result.has_right
fill_from_binary (b: BINARY_TREE [G])
-- Fill from a binary tree representation.
-- Left child becomes first child.
-- Right child becomes right sibling.
-- Any right child of b is ignored.
-- (from DYNAMIC_TREE)
linear_representation: LINEAR [G]
-- Representation as a linear structure
-- (from TREE)
feature -- Duplication
duplicate (n: INTEGER): like Current
-- Copy of sub-tree beginning at cursor position and
-- having min (n, arity - child_index + 1)
-- children
-- (from DYNAMIC_TREE)
require -- from TREE
not_child_off: not child_off;
valid_sublist: n >= 0
feature -- Implementation
child: like first_child
-- Element at cursor position
-- (from LINKED_LIST)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
off_constraint: (child = void) implies child_off;
-- from DYNAMIC_TREE
extendible_definition: extendible;
child_after_definition: child_after = (child_index = arity + 1);
-- from 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 = arity);
child_after_definition: child_after = (child_index >= arity + 1);
child_consistency: child_readable implies child.parent = Current;
-- from BI_LINKABLE
right_symmetry: (right_sibling /= void) implies (right_sibling.left_sibling = Current);
left_symmetry: (left_sibling /= void) implies (left_sibling.right_sibling = Current);
-- from 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);
-- from LIST
before_definition: child_before = (child_index = 0);
after_definition: child_after = (child_index = arity + 1);
-- from 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));
-- from ACTIVE
writable_constraint: child_writable implies child_readable;
empty_constraint: is_leaf implies (not child_readable) and (not child_writable);
-- from BILINEAR
not_both: not (child_after and child_before);
empty_property: is_leaf implies (child_after or child_before);
before_constraint: child_before implies child_off;
-- from LINEAR
after_constraint: child_after implies child_off;
-- from TRAVERSABLE
empty_constraint: is_leaf implies child_off;
-- from FINITE
empty_definition: is_leaf = (arity = 0);
non_negative_count: arity >= 0;
-- from DYNAMIC_CHAIN
extendible: child_extendible;
end -- class TWO_WAY_TREE