deferred class interface P_TABLE[G,K] 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 key_search (k: K) -- Search by key (using is_equal to compare keys). require readable: is_readable found: BOOLEAN -- Result of the last search operation. found_count: INTEGER -- Number of items found during the last search. require meaningful: found = true ensure meaningful: Result >= 1 feature(s) from P_TABLE -- Status key: K -- Current key. require readable: is_readable; not_empty: not is_empty is_key_writable (k: K): BOOLEAN -- Can data be added with this key? -- (e.g., support for Dictionaries) require valid: not is_void(k) feature(s) from P_TABLE -- Update add (it: G; k: K) -- Add a new item (with its key). require writable: is_writable; not_void_key: not is_void(k); acceptable_key: is_key_writable(k) ensure keep_reference: -- keep copy of item and key. replace (it: G) -- Replace current item (keep the current key). require meaningful: not is_empty; writable: is_writable ensure keep_reference: -- keep copy of item. remove -- Remove the current item (and its corresponding key -- if it is associated with no other items). require meaningful: not is_empty; writable: is_writable feature(s) from P_TABLE -- Conversion to_key_list: P_LIST[K] -- Return a list of keys in the table. ensure valid: Result /= Void; -- new list generated each time (but real keys) is_shallow_copy: to_item_list: P_LIST[G] -- Return a list of items in the table. ensure valid: Result /= Void; -- new list generated each time (but real items) is_shallow_copy: invariant empty: is_empty = count = 0; end of deferred P_TABLE[G,K]