deferred class interface P_SET[G] feature(s) from P_CONTAINER -- Status count: INTEGER -- Number of items in the container. ensure positive: Result >= 0 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. require readable: is_readable; not_empty: not is_empty feature(s) from P_CONTAINER -- Update reset -- Remove all objects from the container. 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 (it: G) -- Search using is_equal for comparisons. require readable: is_readable ensure search_eq_has: found implies has(it); item_set: found implies item.is_equal(it) found: BOOLEAN -- Result of the last search operation. 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 -- Does the container has a - unique - copy of the object? feature(s) from P_SET -- Update add (it: G) -- Add an item to the container. require writable: is_writable; not_void: not is_void(it); has_not: not has(it) ensure keep_reference: has(it) remove -- Remove the current item. require writable: is_writable; not_empty: not is_empty ensure done: -- not has(old item) feature(s) from P_SET -- Conversion to_list: P_LIST[G] -- Convert the set to a list. ensure done: Result /= Void and then Result.count = count; -- new list, but real items is_shallow_copy: invariant empty: is_empty = count = 0; end of deferred P_SET[G]