Section Header

    + name := AVL_TREE[E];
Definition of a mathematical set of comparable objects. All common
operations on mathematical sets are available.

Section Insert

    - parent_avl_constants:AVL_CONSTANTS :=

Section Public

    - debug_string:STRING <-

    + count:INTEGER;

Section Public

Adding and removing:


    - remove e:E <-

    - fast_remove e:E <-

Section SELF

    + root:AVL_TREE_NODE[E];

    + rebalance:BOOLEAN;

    + item_memory:E;

    - set_value_and_key n:AVL_TREE_NODE[E] <-

    - set_value n:AVL_TREE_NODE[E] <-

    - fast_do_insert n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - do_insert n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - left_grown n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - right_grown n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - fast_do_remove (n:AVL_TREE_NODE[E],e:E) :AVL_TREE_NODE[E] <-

    - do_remove (n:AVL_TREE_NODE[E],e:E) :AVL_TREE_NODE[E] <-

    - remove_right (n1, n2:AVL_TREE_NODE[E]) :AVL_TREE_NODE[E] <-

    - left_shrunk n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - right_shrunk n:AVL_TREE_NODE[E] :AVL_TREE_NODE[E] <-

    - exchange_and_discard (n1, n2:AVL_TREE_NODE[E]) <-

    - clear_nodes node:AVL_TREE_NODE[E] <-

    - node_height node:AVL_TREE_NODE[E] :INTEGER <-

Section Public

Looking and searching:


    - has e:E :BOOLEAN <-
        Is element `e' in the set?

    - fast_has e:E :BOOLEAN <-
        Is element `e' in the set?

Section SELF

Iterating internals:


    - build_map <-

    + map:FAST_ARRAY[AVL_TREE_NODE[E]];
        Elements in a row for iteration. See `build_map'.

    + map_dirty:BOOLEAN;
        True when the map needs to be built again for the iterators.
        See `build_map'.

Section SELF

    - new_node:AVL_TREE_NODE[E] <-

    - a_new_node:AVL_TREE_NODE[E] <-

    - discard_node n:AVL_TREE_NODE[E] <-

invariant

[
-? {map != NULL};
-? {(! map_dirty) -> (map.count = count)};
-? {(count > 0) -> ((root != NULL) && {root.count = count})};
]