deferred class interface P_SEARCHABLE[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 search (x: K) -- Search 'x' in the container, and set the current item -- to one of the container's item which is equal to 'x' if -- successful. Equality as per is_equal. 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 invariant empty: is_empty = count = 0; end of deferred P_SEARCHABLE[G,K]