deferred class interface DS_TABLE[G,K] feature(s) from DS_CONTAINER -- Measurement count: INTEGER -- Number of items in container feature(s) from DS_CONTAINER -- Status report is_empty: BOOLEAN -- Is container empty? feature(s) from DS_CONTAINER -- Comparison is_equal (other: like Current): BOOLEAN -- Is current container equal to other? require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) feature(s) from DS_CONTAINER -- Removal wipe_out -- Remove all items from container. ensure wiped_out: is_empty feature(s) from DS_TABLE -- Access infix "@" (k: K): G -- Item associated with k require has_k: has(k) feature(s) from DS_TABLE -- Access item (k: K): G -- Item associated with k require has_k: has(k) feature(s) from DS_TABLE -- Status report valid_key (k: K): BOOLEAN -- Is k a valid key? has (k: K): BOOLEAN -- Is there an item associated with k? ensure valid_key: Result implies valid_key(k) feature(s) from DS_TABLE -- Element change replace (v: G; k: K) -- Replace item associated with k by v. require has_k: has(k) ensure replaced: item(k) = v; same_count: count = old count put (v: G; k: K) -- Associate v with key k. require valid_key: valid_key(k) ensure inserted: has(k) and then item(k) = v; same_count: old has(k) implies count = old count; one_more: not old has(k) implies count = old count + 1 put_new (v: G; k: K) -- Associate v with key k. require valid_key: valid_key(k); new_item: not has(k) ensure one_more: count = old count + 1; inserted: has(k) and then item(k) = v swap (k, l: K) -- Exchange items associated with k and l. require valid_k: has(k); valid_l: has(l) ensure same_count: count = old count; new_k: item(k) = old item(l); new_l: item(l) = old item(k) feature(s) from DS_TABLE -- Removal remove (k: K) -- Remove item associated with k. require valid_key: valid_key(k) ensure same_count: not old has(k) implies count = old count; one_less: old has(k) implies count = old count - 1; removed: not has(k) invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; end of deferred DS_TABLE[G,K]