class interface P_DICTIONARY[G,K->HASHABLE] creation make -- Initialise. feature(s) from P_CONTAINER -- Status count: INTEGER -- Number of items/keys. 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 -- 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 (k: K) -- Search key and set current item if successful. -- is_equal is used to compare keys. require readable: is_readable found: BOOLEAN -- Result of key search. found_count: INTEGER -- Number of items for found key (always 1 for dictionary). 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 the key already used? require valid: not is_void(k) feature(s) from P_TABLE -- Update add (it: G; k: K) -- Add item and corresponding key. -- (key must be available). 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 (key unchanged). require meaningful: not is_empty; writable: is_writable ensure keep_reference: -- keep copy of item. remove -- Remove current item and associated key. require meaningful: not is_empty; writable: is_writable feature(s) from P_TABLE -- Conversion to_key_list: P_LIST[K] -- List of keys. ensure done: Result.count = count; valid: Result /= Void; -- new list generated each time (but real keys) is_shallow_copy: to_item_list: P_LIST[G] -- List of items. ensure done: Result.count = count; valid: Result /= Void; -- new list generated each time (but real items) is_shallow_copy: feature(s) from P_DICTIONARY make -- Initialise. feature(s) from P_DICTIONARY -- from ANY copy (other: like Current) -- Copy. 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) invariant empty: is_empty = count = 0; end of P_DICTIONARY[G,K->HASHABLE]