indexing
description: "Trees, without commitment to a particular representation"
names: tree
access: cursor, membership
representation: recursive
contents: generic
deferred class interface
TREE [G]
feature -- Access
child: like parent
-- Current child node
require
readable: readable_child
child_cursor: CURSOR
-- Current cursor position
child_index: INTEGER
-- Index of current child
ensure
valid_index: Result >= 0 and Result <= arity + 1
child_item: like item
-- Item in current child node
require
readable: child_readable
first_child: like parent
-- Leftmost child
require
is_not_leaf: not is_leaf
has (v: G): BOOLEAN
-- Does subtree include v?
-- (Reference or object equality,
-- based on object_comparison.)
ensure -- from CONTAINER
not_found_in_empty: Result implies not empty
is_sibling (other: like parent): BOOLEAN
-- Are current node and other siblings?
ensure
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
item: G
-- Item in current node
last_child: like first_child
-- Right most child
require
is_not_leaf: not is_leaf
left_sibling: like parent
-- Left neighbor (if any)
require
is_not_root: not is_root
ensure
is_sibling: is_sibling (Result);
right_is_current: (Result /= void) implies (Result.right_sibling = Current)
parent: TREE [G]
-- Parent of current node
right_sibling: like parent
-- Right neighbor (if any)
require
is_not_root: not is_root
ensure
is_sibling: is_sibling (Result);
left_is_current: (Result /= void) implies (Result.left_sibling = Current)
feature -- Measurement
arity: INTEGER
-- Number of children
count: INTEGER
-- Number of items
feature -- Status report
changeable_comparison_criterion: BOOLEAN
-- May object_comparison be changed?
-- (Answer: yes by default.)
-- (from CONTAINER)
child_after: BOOLEAN
-- Is there no valid child position to the right of cursor?
child_before: BOOLEAN
-- Is there no valid child position to the left of cursor?
child_isfirst: BOOLEAN
-- Is cursor under first child?
ensure
not_is_leaf: Result implies not is_leaf
child_islast: BOOLEAN
-- Is cursor under last child?
ensure
not_is_leaf: Result implies not is_leaf
child_off: BOOLEAN
-- Is there no current child?
child_readable: BOOLEAN
-- Is there a current child_item to be read?
child_writable: BOOLEAN
-- Is there a current child_item that may be modified?
empty: BOOLEAN
-- Is structure empty of items?
is_leaf: BOOLEAN
-- Are there no children?
is_root: BOOLEAN
-- Is there no parent?
object_comparison: BOOLEAN
-- Must search operations use equal rather than =
-- for comparing references? (Default: no, use =.)
-- (from CONTAINER)
Readable: BOOLEAN is true
readable_child: BOOLEAN
-- Is there a current child to be read?
valid_cursor_index (i: INTEGER): BOOLEAN
-- Is i correctly bounded for cursor movement?
ensure
valid_cursor_index_definition: Result = (i >= 0) and (i <= arity + 1)
Writable: BOOLEAN is true
-- Is there a current item that may be modified?
writable_child: BOOLEAN
-- Is there a current child that may be modified?
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 child.
child_finish
-- Move cursor to last child.
ensure then
is_last_child: not is_leaf implies child_islast
child_forth
-- Move cursor to next child.
child_go_i_th (i: INTEGER)
-- Move cursor to i-th child.
require else
valid_cursor_index: valid_cursor_index (i)
ensure then
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.
child_start
-- Move cursor to first child.
ensure then
is_first_child: not is_leaf implies child_isfirst
feature -- Element change
child_put (v: like item)
-- Put v at current child position.
-- Was declared in TREE as synonym of child_put and child_replace.
require
child_writable: child_writable
ensure
item_inserted: child_item = v
child_replace (v: like item)
-- Put v at current child position.
-- Was declared in TREE as synonym of child_put and child_replace.
require
child_writable: child_writable
ensure
item_inserted: child_item = v
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.
prune (n: like parent)
-- Remove n from the children
require
is_child: n.parent = Current
ensure
n_is_root: n.is_root
put (v: like item)
-- Replace element at cursor position by v.
-- Was declared in TREE as synonym of put and replace.
require
is_writable: writable
ensure
item_inserted: item = v
replace (v: like item)
-- Replace element at cursor position by v.
-- Was declared in TREE as synonym of put and replace.
require
is_writable: writable
ensure
item_inserted: item = v
replace_child (n: like parent)
-- Put n at current child position.
require
writable_child: writable_child;
was_root: n.is_root
ensure
child_replaced: child = n
sprout
-- Make current node a root.
feature -- Conversion
binary_representation: BINARY_TREE [G]
-- Convert to binary tree representation:
-- first child becomes left child,
-- right sibling becomes right child.
ensure
result_is_root: Result.is_root;
result_has_no_right_child: not Result.has_right
linear_representation: LINEAR [G]
-- Representation as a linear structure
feature -- Duplication
duplicate (n: INTEGER): like Current
-- Copy of sub-tree beginning at cursor position and
-- having min (n, arity - child_index + 1)
-- children.
require
not_child_off: not child_off;
valid_sublist: n >= 0
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (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 = arity);
child_after_definition: child_after = (child_index >= arity + 1);
child_consistency: child_readable implies child.parent = Current;
end -- class TREE