class interface P_HISTORY_LIST[G] creation make 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 this container writable? item: G -- Current item. require readable: is_readable; not_empty: not is_empty feature(s) from P_CONTAINER -- Update reset -- Reset 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_DISPENSER -- Update add (it: G) -- Add at the end of the list, remove first if too big. ensure done: count < maximum implies count = old count + 1; keep_reference: -- keep a copy of the item. remove -- This feature need not be used normally. require meaningful: not is_empty feature(s) from P_DISPENSER -- Conversion to_list: P_LIST[G] -- List of elements in container. ensure valid_result: Result /= Void; -- new list but old items. is_shallow_copy: feature(s) from P_SEQUENCE -- Update set_index (i: INTEGER) -- Set the current item to the one at position 'idx'. require not_empty: not is_empty; index_low: i >= 1; index_up: i <= count feature(s) from P_SEQUENCE -- Status index: INTEGER require not_empty: not is_empty ensure valid: Result >= 1 and Result <= count feature(s) from P_HISTORY_LIST -- 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) feature(s) from P_HISTORY_LIST -- Creation make feature(s) from P_HISTORY_LIST -- Properties maximum: INTEGER -- Max number of item in the container. set_maximum (max: INTEGER) -- Set the maximum number of item in the container. require positive: max > 0 invariant empty: is_empty = count = 0; max: maximum > 0; coherent_count: count = container.count; count: count <= maximum; end of P_HISTORY_LIST[G]