class AVL_SET [E_ -> COMPARABLE]

Features exported to ANY

Direct parents

conformant parents

SET

non-conformant parents

AVL_TREE

Summary

creation features

exported features

Counting:

Adding and removing:

Looking and searching:

To provide iterating facilities:

Mathematical operations:

Comparison:

Agents based features:

Adding and removing:

Looking and searching:

Details

make

Creation of an empty SET.

ensure

  • is_empty

add (e: E_)

Add new item e to the set. The mathematical definition of adding in a set is followed, i.e. the element e is added only and only if it is not yet present in the set. As this add feature is actually using is_equal, you may consider to use fast_add for expanded objects as well while trying to get the very best performances.

require

  • e /= Void

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

fast_add (e: E_)

Same job as add, but uses basic = for comparison.

require

  • e /= Void

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

clear_count

Empty the current set (is_empty is True after that call). If possible, the actual implementation is supposed to keep its internal storage area in order to refill Current in an efficient way. See also clear_count_and_capacity to select the most appropriate.

ensure

  • is_empty: count = 0

clear_count_and_capacity

Empty the current set (is_empty is True after that call). If possible, the actual implementation is supposed to release its internal storage area for this memory to be used by other objects. See also clear_count to select the most appropriate.

ensure

  • is_empty: count = 0

reference_at (e: E_): E_

Non Void when e is in the set. In such a situation, Result is the object which is actually stored in the Current set (see ensure assertion).

require

  • e /= Void
  • not e.is_expanded_type

ensure

  • has(e) implies Result.is_equal(e)

item (index: INTEGER): E_

Return the item indexed by index.

require

  • valid_index(index)

ensure

  • has(Result)

deferred count: INTEGER

Cardinality of the set (i.e. actual count of stored elements).

is_empty: BOOLEAN

Is the set empty?

ensure

  • Result = (count = 0)

deferred remove (e: E_)

Remove item e from the set: the mathematical definition of removing from a set is followed.

require

  • e /= Void

ensure

  • removed: not has(e)
  • not_in_not_removed: not old has(e) implies count = old count
  • in_then_removed: old has(e) implies count = old count - 1

deferred fast_remove (e: E_)

Same job as remove, but uses basic = for comparison.

require

  • e /= Void

ensure

  • removed: not has(e)
  • not_in_not_removed: not old has(e) implies count = old count
  • in_then_removed: old has(e) implies count = old count - 1

frozen clear
This feature is obsolete: Now use `clear_count' or `clear_count_and_capacity' (july 17th 2004).
deferred has (e: E_): BOOLEAN

Is element e in the set? As this query is actually using is_equal, you may consider to use fast_has for expanded objects as well while trying to get the very best performances.

require

  • e /= Void

ensure

  • Result implies not is_empty

deferred fast_has (e: E_): BOOLEAN

Is element e actually stored in the set? Warning: this query is using basic = for comparison. See also has when dealing with reference types.

require

  • e /= Void

ensure

  • Result implies e = reference_at(e)

lower: INTEGER
upper: INTEGER

ensure

  • Result = count

valid_index (index: INTEGER): BOOLEAN

ensure

  • Result = index.in_range(lower, upper)

get_new_iterator: ITERATOR[E_]
union (other: AVL_SET [E_ -> COMPARABLE])

Make the union of the Current set with other.

require

  • other /= Void

ensure

  • count <= old count + other.count

+ (other: AVL_SET [E_ -> COMPARABLE]): AVL_SET [E_ -> COMPARABLE]

Return the union of the Current set with other.

require

  • other /= Void

ensure

  • Result.count <= count + other.count
  • Current.is_subset_of(Result) and then other.is_subset_of(Result)

intersection (other: AVL_SET [E_ -> COMPARABLE])

Make the intersection of the Current set with other.

require

  • other /= Void

ensure

  • count <= other.count.min(old count)

^ (other: AVL_SET [E_ -> COMPARABLE]): AVL_SET [E_ -> COMPARABLE]

Return the intersection of the Current set with other.

require

  • other /= Void

ensure

  • Result.count <= other.count.min(count)
  • Result.is_subset_of(Current) and then Result.is_subset_of(other)

minus (other: AVL_SET [E_ -> COMPARABLE])

Make the set Current - other.

require

  • other /= Void

ensure

  • count <= old count

- (other: AVL_SET [E_ -> COMPARABLE]): AVL_SET [E_ -> COMPARABLE]

Return the set Current - other.

require

  • other /= Void

ensure

  • Result.count <= count
  • Result.is_subset_of(Current)

is_subset_of (other: AVL_SET [E_ -> COMPARABLE]): BOOLEAN

Is the Current set a subset of other?

require

  • other /= Void

ensure

  • Result implies count <= other.count

is_disjoint_from (other: AVL_SET [E_ -> COMPARABLE]): BOOLEAN

Is the Current set disjoint from other ?

require

  • other /= Void

ensure

  • Result = (Current ^ other).is_empty

is_equal (other: AVL_SET [E_ -> COMPARABLE]): BOOLEAN

Is the Current set equal to other?

require

  • other /= Void

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)

copy (other: AVL_SET [E_ -> COMPARABLE])

Copy 'other' into the current set

require

  • same_dynamic_type(other)

ensure

  • is_equal(other)

from_collection (model: COLLECTION[E_])

Add all items of model.

require

  • model /= Void

do_all (action: ROUTINE[TUPLE[TUPLE 1[E_]]])

Apply action to every item of Current.

See also for_all, exists.

for_all (predicate: PREDICATE[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Do all items satisfy predicate?

See also do_all, exists.

exists (predicate: PREDICATE[TUPLE[TUPLE 1[E_]]]): BOOLEAN

Does at least one item satisfy predicate?

See also do_all, for_all.

test (e1: E, e2: E): BOOLEAN

In order to avoid run-time type errors, feature safe_equal calls is_equal only when e1 and e2 have exactly the same dynamic type. Furthermore, this feature avoids argument passing from some expanded type to the corresponding reference type (no automatic allocation of some reference type during the comparison).

safe_equal (e1: E, e2: E): BOOLEAN

In order to avoid run-time type errors, feature safe_equal calls is_equal only when e1 and e2 have exactly the same dynamic type. Furthermore, this feature avoids argument passing from some expanded type to the corresponding reference type (no automatic allocation of some reference type during the comparison).

debug_string: STRING
count: INTEGER
remove (e: E_)
fast_remove (e: E_)
has (e: E_): BOOLEAN

Is element e in the set?

fast_has (e: E_): BOOLEAN

Is element e in the set?

Class invariant