class interface P_CATALOG[G,K->HASHABLE] creation make -- Initialise. feature(s) from P_CONTAINER -- Status count: INTEGER -- Number of keys in container. ensure positive: Result >= 0 is_empty: BOOLEAN -- Is the container empty? is_readable: BOOLEAN -- Is the container currently readable? is_writable: BOOLEAN -- Catalog is always writable. item: G -- Current item. require readable: is_readable; not_empty: not is_empty feature(s) from P_CONTAINER -- Update reset -- Initialise. 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 (x: K) -- Search by key, compared using is_equal. require readable: is_readable found: BOOLEAN -- Result of search. found_count: INTEGER -- Number of items found corresponding to key. 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 -- Is it possible to add item with corresponding key? -- (always true in catalog) require valid: not is_void(k) ensure catalog: Result = true feature(s) from P_TABLE -- Update add (x: G; k: K) -- Add item with correspoding 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 (x: G) -- Replace the first item in item list. require meaningful: not is_empty; writable: is_writable ensure keep_reference: -- keep copy of item. remove -- Remove current key and associated item(s). require meaningful: not is_empty; writable: is_writable feature(s) from P_TABLE -- Conversion to_key_list: P_LIST[K] -- List of keys in the container. ensure valid: Result /= Void; -- new list generated each time (but real keys) is_shallow_copy: to_item_list: P_LIST[G] -- List of items in the containers (possibly more than keys). ensure valid: Result /= Void; -- new list generated each time (but real items) is_shallow_copy: feature(s) from P_CATALOG -- Creation make -- Initialise. feature(s) from P_CATALOG -- from ANY copy (other: like Current) -- Copy from other catalog. require other_not_void: other /= Void ensure is_equal: is_equal(other) is_equal (other: like Current): BOOLEAN -- Equality. require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) feature(s) from P_CATALOG -- Catalog item_list: P_LIST[G] -- List of items associated with a single key. require not_empty: not is_empty ensure is_shallow_copy: -- list of real items in the list. invariant empty: is_empty = count = 0; end of P_CATALOG[G,K->HASHABLE]