deferred class AVL_TREE [E_ -> COMPARABLE]

All features

Definition of a mathematical set of comparable objects. All common operations on mathematical sets are available.

Direct parents

non-conformant parents

AVL_CONSTANTS

Known children

non-conformant children

AVL_DICTIONARY, AVL_SET

Summary

exported features

Adding and removing:

Looking and searching:

Iterating internals:

Details

debug_string: STRING
count: INTEGER
remove (e: E_)
fast_remove (e: E_)
root: AVL_TREE_NODE[E_]
rebalance: BOOLEAN
item_memory: E_
deferred set_value_and_key (n: AVL_TREE_NODE[E_])
deferred set_value (n: AVL_TREE_NODE[E_])
fast_do_insert (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > old node_height(n))

do_insert (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > old node_height(n))

left_grown (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - node_height(n.left) + 1 = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > 1 + old node_height(n.right).max(node_height(n.left) - 1))

right_grown (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - 1 - node_height(n.left) = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) > 1 + old node_height(n.left).max(node_height(n.right) - 1))

fast_do_remove (n: AVL_TREE_NODE[E_], e: E_): AVL_TREE_NODE[E_]

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n))

do_remove (n: AVL_TREE_NODE[E_], e: E_): AVL_TREE_NODE[E_]

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n))

remove_right (n1: AVL_TREE_NODE[E_], n2: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • n1 /= Void
  • n2 /= Void

ensure

  • Result = Void or else Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < old node_height(n2))

left_shrunk (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) - node_height(n.left) - 1 = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < 1 + old node_height(n.right).max(node_height(n.left) + 1))

right_shrunk (n: AVL_TREE_NODE[E_]): AVL_TREE_NODE[E_]

require

  • rebalance
  • n /= Void
  • node_height(n.right) + 1 - node_height(n.left) = n.balance

ensure

  • Result /= Void
  • Result.balance = node_height(Result.right) - node_height(Result.left)
  • rebalance = (node_height(Result) < 1 + old node_height(n.left).max(node_height(n.right) + 1))

deferred exchange_and_discard (n1: AVL_TREE_NODE[E_], n2: AVL_TREE_NODE[E_])

require

  • n1 /= Void
  • n2 /= Void

ensure

  • map_dirty
  • count = old count - 1
  • rebalance

clear_nodes (node: AVL_TREE_NODE[E_])
node_height (node: AVL_TREE_NODE[E_]): INTEGER
has (e: E_): BOOLEAN

Is element e in the set?

fast_has (e: E_): BOOLEAN

Is element e in the set?

build_map

require

  • build_needed: map_dirty

ensure

  • build_done: not map_dirty

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.

new_node: AVL_TREE_NODE[E_]
deferred a_new_node: AVL_TREE_NODE[E_]
deferred discard_node (n: AVL_TREE_NODE[E_])

require

  • n /= Void

lost_nodes: WEAK_REFERENCE[AVL_TREE_NODE[E_]]
balanced: INTEGER
imbalanced_left: INTEGER
imbalanced_right: INTEGER

Class invariant