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})};
]