class HASHED_SET [E_ -> HASHABLE]

Features exported to SET

Direct parents

conformant parents

SET

Summary

creation features

exported features

Internal cache handling:

Counting:

Adding and removing:

To provide iterating facilities:

Mathematical operations:

Comparison:

Agents based features:

Details

make

Create an empty set. Internal storage capacity of the set is initialized using the Default_size value. Then, tuning of needed storage size is done automatically according to usage. If you are really sure that your set is always really bigger than Default_size, you may use with_capacity to save some execution time.

ensure

  • capacity = Default_size
  • is_empty

with_capacity (medium_size: INTEGER)

Create an empty set using medium_size as an appropriate value to help initialization of capacity. Thus, this feature may be used in place of make to save some execution time if one is sure that storage size will rapidly become really bigger than Default_size (if not sure, simply use make). Anyway, the initial medium_size value is just an indication and never a limit for the possible capacity. Keep in mind that the capacity tuning is done automatically according to usage.

require

  • medium_size > 0

ensure

  • is_empty
  • capacity >= medium_size

from_collection (model: COLLECTION[E_])

Add all items of model.

require

  • model /= Void

Default_size: INTEGER

Minimum size for storage in number of items.

buckets: NATIVE_ARRAY[HASHED_SET_NODE[E_]]

The buckets storage area is the primary hash table of capacity elements. To search some element, the first access is done in buckets using the remainder of the division of the key hash_code by capacity. In order to try to avoid clashes, capacity is always a prime number (selected using HASH_TABLE_SIZE).

cache_user: INTEGER

The last user's external index in range [1 .. count] (see item and valid_index for example) may be saved in cache_user otherwise -1 to indicate that the cache is not active. When the cache is active, the corresponding index in buckets is save in cache_buckets and the corresponding node in cache_node.

cache_node: HASHED_SET_NODE[E_]

Meaningful only when cache_user is not -1.

cache_buckets: INTEGER

Meaningful only when cache_user is not -1.

capacity: INTEGER

Of the buckets storage area.

count: INTEGER

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

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

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

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

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

  • capacity = old capacity
  • 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

  • capacity = old capacity
  • is_empty: count = 0

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

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)

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)

intersection (other: HASHED_SET [E_ -> HASHABLE])

Make the intersection of the Current set with other.

require

  • other /= Void

ensure

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

copy (other: HASHED_SET [E_ -> HASHABLE])

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

is_empty: BOOLEAN

Is the set empty?

ensure

  • Result = (count = 0)

frozen clear
This feature is obsolete: Now use `clear_count' or `clear_count_and_capacity' (july 17th 2004).
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: HASHED_SET [E_ -> HASHABLE])

Make the union of the Current set with other.

require

  • other /= Void

ensure

  • count <= old count + other.count

+ (other: HASHED_SET [E_ -> HASHABLE]): HASHED_SET [E_ -> HASHABLE]

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)

^ (other: HASHED_SET [E_ -> HASHABLE]): HASHED_SET [E_ -> HASHABLE]

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: HASHED_SET [E_ -> HASHABLE])

Make the set Current - other.

require

  • other /= Void

ensure

  • count <= old count

- (other: HASHED_SET [E_ -> HASHABLE]): HASHED_SET [E_ -> HASHABLE]

Return the set Current - other.

require

  • other /= Void

ensure

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

is_subset_of (other: HASHED_SET [E_ -> HASHABLE]): BOOLEAN

Is the Current set a subset of other?

require

  • other /= Void

ensure

  • Result implies count <= other.count

is_disjoint_from (other: HASHED_SET [E_ -> HASHABLE]): BOOLEAN

Is the Current set disjoint from other ?

require

  • other /= Void

ensure

  • Result = (Current ^ other).is_empty

is_equal (other: HASHED_SET [E_ -> HASHABLE]): 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)

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).

Class invariant