+
Point of view
All features
class AVL_SET [E_ -> COMPARABLE]
require
ensure
-
added: has(e)
-
not_in_then_added: not old has(e) implies count = old count + 1
-
in_then_not_added: old has(e) implies count = old count
require
ensure
-
added: has(e)
-
not_in_then_added: not old has(e) implies count = old count + 1
-
in_then_not_added: old has(e) implies count = old count
require
- e /= Void
-
elements_are_not_expanded: Result = Void
ensure
- has(e) implies Result.is_equal(e)
require
ensure
- map_dirty
- count = old count - 1
- rebalance
ensure
-
definition: Result = count = 0
require
ensure
-
definition: Result = item(lower)
require
ensure
-
definition: Result = item(upper)
require
ensure
-
double_inclusion: Result = is_subset_of(other) and other.is_subset_of(Current)
-
commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
safe_equal (e1: E_, e2: E_):
BOOLEAN
effective function