class interface P_QUEUE[G] creation make -- Create stack 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 -- Create stack 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_DISPENSER -- Update add (it: G) -- Add an item to the dispenser (push). ensure keep_reference: -- keep a copy of the item. remove -- Remove an item from the dispenser and update -- the current item (pop). require meaningful: not is_empty feature(s) from P_DISPENSER -- Conversion to_list: P_LIST[G] -- Items in stack (bottom of stack first). ensure valid_result: Result /= Void; -- new list but old items. is_shallow_copy: feature(s) from P_STACK make -- Create stack feature(s) from P_STACK -- from ANY copy (other: like Current) require other_not_void: other /= Void ensure is_equal: is_equal(other) is_equal (other: like Current): BOOLEAN 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_QUEUE[G]