class interface P_HASH_SET[G->HASHABLE] creation make -- Create set. feature(s) from P_CONTAINER -- Status count: INTEGER -- Number of items in the container. is_empty: BOOLEAN -- Is the container empty? is_readable: BOOLEAN -- Is the container currently readable? is_writable: BOOLEAN -- Is the container currently writable? item: G -- Current item. -- Time: O(1) require readable: is_readable; not_empty: not is_empty feature(s) from P_CONTAINER -- Update reset -- Create set. require writable: is_writable ensure done: is_empty feature(s) from P_CONTAINER -- Output out: STRING -- String representation. ensure is_copy: -- new string feature(s) from P_CONTAINER -- Utility is_void (x: ANY): BOOLEAN -- Void assertion for generic parameters. feature(s) from P_SEARCHABLE -- Search search (x: G) -- Search item in container (compare using is_equal). -- Time: O(1) require readable: is_readable ensure search_eq_has: found implies has(x); item_set: found implies item.is_equal(x) found: BOOLEAN -- Result of last search. -- Time: O(1), attribute found_count: INTEGER -- A set has only one copy of each item. require meaningful: found = true ensure set_count: Result = 1; meaningful: Result >= 1 feature(s) from P_SET -- Search has (it: G): BOOLEAN -- Is the item in the container (side-effect free search) -- Time: O(1) feature(s) from P_SET -- Update add (it: G) -- Add item to container. -- Time: O(1), amortised require writable: is_writable; not_void: not is_void(it); has_not: not has(it) ensure count: count = old count + 1; keep_reference: has(it) remove -- Remove current item. -- Time: 0(1), amortised require writable: is_writable; not_empty: not is_empty ensure count: count = old count - 1; -- not has(old item) done: done: -- not has(old item) feature(s) from P_SET -- Conversion to_list: P_LIST[G] -- Convert the hash set to a (linked) list. -- Time: O(count) ensure done: Result /= Void and then Result.count = count; -- new list, but real items is_shallow_copy: feature(s) from P_HASH_SET -- Creation make -- Create set. feature(s) from P_HASH_SET -- General copy (other: like Current) -- Copy set (same items). -- Time: 0(count) require other_not_void: other /= Void ensure is_equal: is_equal(other) is_equal (other: like Current): BOOLEAN -- Other container equal? -- Time: O(count) require other_not_void: other /= Void ensure done_count: Result implies count = other.count; -- Result implies (for_each item other.has(item)) done: consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) invariant empty: is_empty = count = 0; resize_up: count // hashsize <= Grow_entries + 1; resize_down: not is_empty and then hashsize > Default_hashsize implies count // hashsize >= Shrink_entries - 1; has_hashtable: hashtable /= Void; hashsize: hashsize = hashtable.count; current_item: not is_empty implies hashlist /= Void; empty: is_empty = hashlist = Void; end of P_HASH_SET[G->HASHABLE]