Section Header

    + name := AVL_SET[E];

Section Inherit

    + parent_set:Expanded SET[E];

    + parent_avl_tree:Expanded AVL_TREE[E];

Section Public

    - add e:E <-

    - fast_add e:E <-

    - clear_count <-

    - reference_at e:E :E <-

    - item index:INTEGER :E <-

Section Public

    - create:SELF <-

    - make <-

Invariant.

[
-? {lost_nodes != NULL};
-? {lost_nodes = common_lost_nodes.at generating_type};
];