deferred class interface P_LIST[G] feature(s) from P_ONEWAY_TRAVERSABLE -- Iteration iterator: P_ITERATOR[G] -- Get a two-way iterator on this container. ensure done: Result /= Void; -- Result /= previous Result is_shallow_copy: is_protected: BOOLEAN -- Is an iterator inside the data structure? feature(s) from P_ONEWAY_TRAVERSABLE -- Lock status has_locked: BOOLEAN -- Does this container has one or more locked items? is_locked: BOOLEAN -- Is the current item locked? require meaningful: not is_empty ensure has_locked: Result = true implies has_locked feature(s) from P_ONEWAY_TRAVERSABLE -- General (from P_CONTAINER) is_writable: BOOLEAN -- Is the structure writable? 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? 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_SORTABLE -- Order relation has_order: BOOLEAN -- Does this container has an order relation defined? set_order (ord_rel: P_ORDER_RELATION[G]) -- Set the order relation which will be used -- when sorting. The relation stays the same when -- the container is reset. require valid: ord_rel /= Void ensure keep_reference: has_order feature(s) from P_SORTABLE -- Sorting sort -- Sort the container. require has_order: has_order; writable: is_writable ensure sorted: is_sorted is_sorted: BOOLEAN -- Is the container sorted? -- Time: O(target.count) require has_order: has_order ensure empty_sorted: is_empty implies Result feature(s) from P_SEARCHABLE -- Search value_search (x: G) -- Search items in the container which are of equal value (as defined -- by the is_equal routine) with 'x'. -- Time: O(count) 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 feature(s) from P_LIST -- Update add (it: G) -- Add item to the container. require writable: is_writable; not_void: not is_void(it) ensure keep_reference: item = it replace (it: G) -- Replace the current item. require writable: is_writable; not_empty: not is_empty; not_void: not is_void(it) ensure keep_reference: item = it insert (it: G) -- Insert item before the current item. require writable: is_writable; not_empty: not is_empty; not_void: not is_void(it) ensure keep_reference: item = it remove -- Remove the current item. require writable: is_writable; not_empty: not is_empty; unlocked: not is_locked feature(s) from P_LIST -- Duplication copy (other: like Current) -- GENERAL's copy. -- Time: O(other.count) require other_not_void: other /= Void ensure is_equal: is_equal(other) feature(s) from P_LIST -- Comparison is_equal (other: like Current): BOOLEAN -- GENERAL's equality relation (requires covariant arguments). -- Time: O(count) require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) is_equal_list (other: P_LIST[G]): BOOLEAN -- Compare two lists which can be of different dynamic type. -- Time: O(count) require valid: other /= Void feature(s) from P_LIST -- Conversion from_list (other: P_LIST[G]) -- Convert from another list. -- Note: The previous contents of this list is deleted. -- Time: O(other.count) require valid: other /= Void ensure done: is_equal_list(other); -- keep copy of items. keep_reference: from_array (other: ARRAY[G]) -- Convert from an ARRAY. -- Note: The previous contents of this list is deleted. -- Time: O(other.count) require valid: other /= Void; -- for_all other.item, other.item /= Void not_void: ensure done: other.count = count; -- keep copy of items. keep_reference: from_iterable (it: P_ONEWAY_ITERATOR[G]) -- Convert from a one way linear iterable container. -- Note: The previous contents of this list is deleted. -- Time: O("it.count") require valid: it /= Void; initialised: it.outside ensure keep_reference: -- keep copy of items. to_array: ARRAY[G] -- Convert list to ARRAY. -- Time: O(count) ensure done: is_empty = Result = Void; -- new array, same items. is_shallow_copy: feature(s) from P_LIST -- Concatenation append (other: P_LIST[G]) -- Append other container to current. -- Time: O(other.count) require valid: other /= Void ensure keep_reference: -- keep copy of items. append_iterable (it: P_ONEWAY_ITERATOR[G]) -- Append the items from a linear iterator. -- Time: O("it.count") require valid_iterator: it /= Void; initialised: it.outside ensure keep_reference: -- keep copy of items. feature(s) from P_LIST -- Search equality_search (x: G) -- Search items in the container which are equal (as defined -- by the = operator) with 'x'. -- Time: O(count) require readable: is_readable invariant empty: is_empty = count = 0; valid_protect_count: protcount >= 0; protection: is_protected implies not is_writable; end of deferred P_LIST[G]