deferred class interface P_TREE[G]
feature(s) from P_CONTAINER
-- Status
count: INTEGER
-- Number of items in the container.
ensure
positive: Result >= 0
is_empty: BOOLEAN
-- Is the container empty?
is_readable: BOOLEAN
-- Is the container currently readable?
is_writable: BOOLEAN
-- Is the structure writable?
item: G
-- Current item.
require
readable: is_readable;
not_empty: not is_empty
feature(s) from P_CONTAINER
-- Update
reset
-- Remove all objects from the container.
require
writable: is_writable
ensure
done: is_empty
feature(s) from P_CONTAINER
-- Output
out: STRING
-- String representation.
ensure
is_copy: -- new string
feature(s) from P_CONTAINER
-- Utility
is_void (x: ANY): BOOLEAN
-- Void assertion for generic parameters.
feature(s) from P_ONEWAY_TRAVERSABLE
-- Iteration
linear_iterator: P_ONEWAY_ITERATOR[G]
-- Get a linear iterator on this container.
ensure
done: Result /= Void; -- Result /= previous Result
is_shallow_copy:
is_protected: BOOLEAN
-- Is an iterator inside the data structure?
feature(s) from P_ONEWAY_TRAVERSABLE
-- Lock status
has_locked: BOOLEAN
-- Does this container has one or more locked items?
is_locked: BOOLEAN
-- Is the current item locked?
require
meaningful: not is_empty
ensure
has_locked: Result = true implies has_locked
feature(s) from P_TREE
-- Linear iteration
preorder_iterator: P_ONEWAY_ITERATOR[G]
-- Linear preorder iterator.
ensure
valid: Result /= Void; -- new iterator provided for each call
is_shallow_copy:
postorder_iterator: P_ONEWAY_ITERATOR[G]
-- Linear postorder iterator.
ensure
valid: Result /= Void; -- new iterator provided for each call
is_shallow_copy:
levelorder_iterator: P_ONEWAY_ITERATOR[G]
-- Linear level order iterator.
ensure
valid: Result /= Void; -- new iterator provided for each call
is_shallow_copy:
feature(s) from P_TREE
-- Modification
add_left (new: G)
-- Add an item to the left of current item.
require
writable: is_writable;
has_item: not is_empty;
not_root: not is_root
ensure
count: count = old count + 1;
keep_reference: item = new
add_right (new: G)
-- Add an item to the right of current item.
require
writable: is_writable;
has_item: not is_empty;
not_root: not is_root
ensure
count: count = old count + 1;
keep_reference: item = new
add_root (new_root: G)
-- Add the root item.
require
writable: is_writable;
empty: is_empty
ensure
count: count = 1;
keep_reference: item = new_root;
root: is_root;
sole_root: is_top and is_bottom and is_left and is_right
add_child (new: G)
-- Add a first child to the current item.
-- Other children may be added with add_right/add_left
require
writable: is_writable;
has_item: not is_empty;
down: is_bottom
ensure
count: count = old count + 1;
keep_reference: item = new;
unique_child: is_left and is_right;
still_down: is_leaf
replace (x: G)
-- Replace current item.
require
writable: is_writable;
has_item: not is_empty
ensure
keep_reference: x = item
remove
-- Remove current item and its children.
-- The tree shall not have locked items.
require
writable: is_writable;
has_item: not is_empty;
unlocked: not has_locked
ensure
count: count = old count - 1;
moved: is_root
feature(s) from P_TREE
-- Cursor
is_left: BOOLEAN
-- Is the current item the first one?
require
meaningful: not is_empty
is_right: BOOLEAN
-- Is the current item the last one?
require
meaningful: not is_empty
is_top: BOOLEAN
-- Is root generation?
require
meaningful: not is_empty
is_bottom: BOOLEAN
-- Has the current item not got any children?
require
meaningful: not is_empty
left
-- Go backwards one slot.
require
meaningful: not is_empty;
not_left: not is_left
right
-- Go forward one item.
require
meaningful: not is_empty;
not_right: not is_right
up
-- Go one generation upwards.
require
meaningful: not is_empty;
not_up: not is_top
down
-- Go one generation downwards.
require
meaningful: not is_empty;
not_down: not is_bottom
ensure
position: is_left
leftmost
-- Go to the leftmost sibling.
require
meaningful: not is_empty
ensure
done: is_left
rightmost
-- Go to the rightmost sibling.
require
meaningful: not is_empty
ensure
done: is_right
root
-- Go to root node.
require
meaningful: not is_empty
ensure
done: is_root
feature(s) from P_TREE
-- Queries
depth: INTEGER
-- Number of level from the root. Root depth is 0.
require
has_item: not is_empty
ensure
positive: Result >= 0;
root_zero: is_root implies Result = 0
is_root: BOOLEAN
-- Is the current item the root?
require
has_item: not is_empty
ensure
done: Result = (is_top and is_left and is_right)
is_leaf: BOOLEAN
-- Is the current item a leaf (node that has no child)?
require
has_item: not is_empty
ensure
done: Result = is_bottom
feature(s) from P_TREE
-- Conversions.
subtree: like Current
-- Tree which has current node as root node.
require
not_empty: not is_empty
ensure
done: Result /= Void and not Result.is_empty; -- New tree, old items.
is_shallow_copy:
siblings_list: P_LIST[G]
-- List of siblings of current item, including current item.
require
not_empty: not is_empty
ensure
done: Result /= Void and then not Result.is_empty; -- List is a copy but contains real items.
is_shallow_copy:
invariant
empty: is_empty = count = 0;
valid_protect_count: protcount >= 0;
protection: is_protected implies not is_writable;
end of deferred P_TREE[G]