Pylon: a foundation library ~ User's guide (Chapter 2) -- contents | previous | next
Concrete containers are the actual implementations of the abstract data structure hierarchy which was introduced in section (see section 1.2). These containers are presented through their flat-short forms after comments regarding the implementation of each container. The flat-short form presents the public interface of a class and is derived from its source code. Most Eiffel environments provide facilities to browse the class hierarchy and produce this form and other views of the system's classes.
Some feature comments include indications regarding complexity using the classical O(x) notation , which shows how a structure should behave, in either space or execution time. This is a function with a parameter, usually named N and referring to the number of items in the container. For instance, if a feature is `O(n)', it means that its execution time is such that there exists a constantA constant may be big, so an O(n) feature will be bound by K.n but if K is big, it may still be quite slow. K such that the function f(n)=K*n gives an upper bound on the execution time. `O(1)' is for a routine whose execution time is independent of the number of items. A complexity like this is normally amortised -- that is average, some less common cases may take much longer, for instance if a structure need to be resized. Other common complexities are O(n.log(n)) which is not too bad and O(n^2) which degrades quickly for big containers.
Iterators are used mainly by lists or through other structures converted to lists. This is the flat form of P_ITERATOR. Its ancestor P_ONEWAY_ITERATOR is similar without the `backwards' features. This is a deferred class, actual iterators are internal classes created by the library when requested from a traversable container.
In general, access to item can be considered constant and fast enough so that caching the item in a local variable is not necessary except when maximum performance is really essential.
deferred class interface P_ITERATOR [G] ancestors P_ITERATOR [G] P_ONEWAY_ITERATOR [G] P_MUTATOR indexing cluster: pylon, iteration; description: "Abstract two-way linear iterator"; interface: abstract, client; feature specification -- Iteration last -- Go to the last item of the container. require outside : outside; deferred ensure done : iterable implies (not outside); back -- Previous item. require inside : not outside; deferred feature specification -- Variant support backward_variant : INTEGER -- Backward variant for back-only loops. deferred feature specification -- Copy copy (other : like Current) -- Cannot copy iterator. require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); feature specification -- Access outside : BOOLEAN -- Is the iterator outside the container? deferred iterable : BOOLEAN -- Is the associated structure iterable (not empty)? deferred item : G -- Return the item at the current position. require inside : not outside; deferred feature specification -- Synchronization synchronize_container -- Set the current item of the target container to be -- the one currently pointed at by the iterator. -- THIS METHOD DOES CHANGE THE CONTAINER STATE. require inside : not outside; deferred ensure done : -- container current position changed feature specification -- Iteration first -- Go to first item of the container. require outside : outside; deferred ensure done : iterable implies (not outside); synchronize -- Set the iterator so that the iterator current item is -- the current item of the container. Do not change the -- container. require outside : outside; iterable : iterable; deferred ensure done : not outside; forth -- Next item. require inside : not outside; deferred stop -- Finish. require inside : not outside; deferred ensure done : outside; feature specification -- Iterator locking is_locked : BOOLEAN -- Is the current iterator locked? deferred lock -- Lock iterator: lock the current item into the container -- and leave the iterator. require inside : not outside; unlocked : not is_locked; deferred ensure locked : is_locked; outside : outside; unlock -- Unlock iterator require locked : is_locked; outside : outside; deferred ensure inside : not outside; not_locked : not is_locked; feature specification -- Variant support forward_variant : INTEGER -- Forward variant for forth-only loops. deferred invariant outside_locked : (not outside) implies (not is_locked); end interface -- class P_ITERATOR
The order relation is a deferred class which is inherited in order to create a customised sort criterion.
deferred class interface P_ORDER_RELATION [G] ancestors P_ORDER_RELATION [G] indexing cluster: pylon; description: "Order relation between two objects for sorting"; interface: abstract, inheritance; feature specification {PUBLIC_NONE, P_CONTAINER} -- Criterion ordered (first, second : G) : BOOLEAN -- Are first and second ordered? (true if first <= second) deferred ensure coherent : (Result = false) implies ordered (second, first); end interface -- class P_ORDER_RELATION :
Two types of lists are available: a classic (two-way) linked list with the class P_LINKED_LIST, implementing the P_LIST interface; and the sequence list, P_SEQUENCE_LIST implemented with an automatically resized array, and adding the features from P_SEQUENCE in addition to the list interface.
class interface P_LINKED_LIST [G] ancestors P_LINKED_LIST [G] P_LIST [G] P_TRAVERSABLE [G] P_ONEWAY_TRAVERSABLE [G] P_CONTAINER [G] P_SORTABLE [G] P_CONTAINER [G] P_SEARCHABLE [G, G] P_CONTAINER [G] indexing cluster: pylon, container; description: "Abstract linked structure"; interface: inheritance; creation make feature specification make reset -- Remove all objects from the container. require writable : is_writable; ensure done : is_empty; feature specification count : INTEGER -- Number of elements in the data structure. feature specification -- Iteration iterator : P_ITERATOR [G] -- Iterator on this list. ensure done : Result /= void; is_shallow_copy : -- Result /= previous Result feature specification -- Lock status is_locked : BOOLEAN -- Is current item locked? -- Time: O(1) require meaningful : not is_empty; ensure has_locked : (Result = true) implies has_locked; feature specification -- Access item : G -- Current item. -- Time: O(1) require readable : is_readable; not_empty : not is_empty; feature specification -- Action add (it : G) -- Add an item to the end of the list. -- Time: O(1) require writable : is_writable; not_void : not is_void (it); ensure keep_reference : item = it; replace (it : G) -- Replace the current item. -- Time: O(1) require writable : is_writable; not_empty : not is_empty; not_void : not is_void (it); ensure keep_reference : item = it; insert (it : G) -- Insert an item before the current item. -- Time: O(1) 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. -- Time: O(1) require writable : is_writable; not_empty : not is_empty; unlocked : not is_locked; feature specification -- Sorting sort -- Insertion sort. -- Time: O(count^2/4) comparisons; O(count) swaps require has_order : has_order; writable : is_writable; ensure sorted : is_sorted; feature specification -- Duplication copy (other : like Current) -- GENERAL's copy. -- Time: O(other.count) require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); feature specification -- 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; same_type : Result implies same_type (other); 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 specification -- 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_reference : -- keep copy of items. 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; not_void : -- for_all other.item, other.item /= Void ensure done : other.count = count; keep_reference : -- keep copy of items. 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); is_shallow_copy : -- new array, old items. feature specification -- 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 specification -- 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; 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 specification -- Sorting is_sorted : BOOLEAN -- Is the container sorted? -- Time: O(target.count) require has_order : has_order; ensure empty_sorted : is_empty implies Result; feature specification -- Iteration is_protected : BOOLEAN -- Is an iterator inside the data structure? feature specification -- Lock status has_locked : BOOLEAN -- Does this container has one or more locked items? feature specification -- General (from P_CONTAINER) is_writable : BOOLEAN -- Is the structure writable? feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. feature specification -- 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; invariant sym_current_first : (current_node = void) = (first_node = void); sym_first_last : (first_node = void) = (last_node = void); correct_bounds : (not is_empty) implies ((first_node.previous = void) and (last_node.next = void)); positive : count >= 0; valid_protect_count : protcount >= 0; protection : is_protected implies (not is_writable); empty : is_empty = (count = 0); end interface -- class P_LINKED_LIST
class interface P_SEQUENCE_LIST [G] ancestors P_SEQUENCE_LIST [G] P_LIST [G] P_TRAVERSABLE [G] P_ONEWAY_TRAVERSABLE [G] P_CONTAINER [G] P_SORTABLE [G] P_CONTAINER [G] P_SEARCHABLE [G, G] P_CONTAINER [G] P_SEQUENCE [G] P_CONTAINER [G] indexing cluster: pylon, container; description: "Concrete indexed list, implemented by an array"; comment: "Implemented with an ARRAY whose size is doubled (and reduced) automatically"; interface: client; creation make feature specification -- Creation make -- Remove all items. -- Time: O(1) reset -- Remove all items. -- Time: O(1) require writable : is_writable; ensure done : is_empty; feature specification -- Iteration iterator : P_ITERATOR [G] -- Get a two-way iterator on this container. ensure done : Result /= void; is_shallow_copy : -- Result /= previous Result feature specification -- Access set_index (i : INTEGER) -- Set current item to position 'i'. -- Time: O(1) require not_empty : not is_empty; index_low : i >= 1; index_up : i <= count; feature specification -- Status count : INTEGER -- Quantity of items in the list. item : G -- Get current item. -- Time: O(1) require readable : is_readable; not_empty : not is_empty; feature specification -- Update add (citem : G) -- Add item at the end of the list. -- Added item becomes current. -- Time: O(1) amortised require writable : is_writable; not_void : not is_void (citem); ensure in_container : container.item (count) = citem; count_ok : count = ((old count) + 1); keep_reference : item = citem; replace (citem : G) -- Replace current item. -- Time: O(1) require writable : is_writable; not_empty : not is_empty; not_void : not is_void (citem); ensure keep_reference : item = citem; insert (citem : G) -- Insert item at current position, and push all the following items. -- Time: O(count) require writable : is_writable; not_empty : not is_empty; not_void : not is_void (citem); ensure done : item = citem; count_ok : count = ((old count) + 1); keep_reference : item = citem; remove -- Remove current item. -- Time: O(count) amortised require writable : is_writable; not_empty : not is_empty; unlocked : not is_locked; ensure count_ok : count = ((old count) - 1); feature specification -- Lock status is_locked : BOOLEAN -- Is current item locked? -- Time: O(1) amortised [dictionary search] require meaningful : not is_empty; ensure has_locked : (Result = true) implies has_locked; feature specification -- Sorting sort -- Selection sort. -- Time: O(target.count^2) comparisons; O(target.count) swaps require has_order : has_order; writable : is_writable; ensure sorted : is_sorted; feature specification -- Duplication copy (other : like Current) -- GENERAL's copy. -- Time: O(other.count) require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); feature specification -- 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; same_type : Result implies same_type (other); 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 specification -- 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_reference : -- keep copy of items. 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; not_void : -- for_all other.item, other.item /= Void ensure done : other.count = count; keep_reference : -- keep copy of items. 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); is_shallow_copy : -- new array, old items. feature specification -- 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 specification -- 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; 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 specification -- Sorting is_sorted : BOOLEAN -- Is the container sorted? -- Time: O(target.count) require has_order : has_order; ensure empty_sorted : is_empty implies Result; feature specification -- Iteration is_protected : BOOLEAN -- Is an iterator inside the data structure? feature specification -- Lock status has_locked : BOOLEAN -- Does this container has one or more locked items? feature specification -- General (from P_CONTAINER) is_writable : BOOLEAN -- Is the structure writable? feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. feature specification -- 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; invariant valid_current : (not is_empty) implies ((current_item >= 1) and (current_item <= count)); good_container : container.lower = 1; big_container : (count /= 0) implies (container.upper >= count); small_container : (count /= 0) implies ((container.count // grow_factor) <= (default_size + count)); positive : count >= 0; valid_protect_count : protcount >= 0; protection : is_protected implies (not is_writable); empty : is_empty = (count = 0); end interface -- class P_SEQUENCE_LIST
Stacks and queues are the two dispenser type provided, both are based on a linked list.
class interface P_STACK [G] ancestors P_STACK [G] P_DISPENSER [G] P_CONTAINER [G] indexing cluster: pylon, container; description: "Basic stack (FIFO) -- implemented with a linked list"; interface: client; creation make feature specification make -- Create stack reset -- Create stack require writable : is_writable; ensure done : is_empty; feature specification -- from ANY copy (other : like Current) -- Update current object using fields ob object attached to `other' -- so as to yield equal objects. require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Is `other' attached to an object considered equal to `Current'? require other_not_void : other /= void; ensure consistent : standard_is_equal (other) implies Result; same_type : Result implies same_type (other); symmetric : Result implies other.is_equal (Current); feature specification -- from P_CONTAINER count : INTEGER -- Number of items in the container. ensure positive : Result >= 0; feature specification is_writable : BOOLEAN is ??? -- Is the container currently writable? feature specification item : G -- Current item. require readable : is_readable; not_empty : not is_empty; 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 specification -- Collection interface. to_list : P_LIST [G] -- Items in stack (bottom of stack first). ensure valid_result : Result /= void; is_shallow_copy : -- new list but old items. feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. invariant empty : is_empty = (count = 0); end interface -- class P_STACK
class interface P_QUEUE [G] ancestors P_QUEUE [G] P_DISPENSER [G] P_CONTAINER [G] indexing cluster: pylon, container; description: "Basic queue (LIFO) -- implemented with a linked list"; interface: client; creation make feature specification make -- Create stack reset -- Create stack require writable : is_writable; ensure done : is_empty; feature specification -- from ANY copy (other : like Current) -- Update current object using fields ob object attached to `other' -- so as to yield equal objects. require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Is `other' attached to an object considered equal to `Current'? require other_not_void : other /= void; ensure consistent : standard_is_equal (other) implies Result; same_type : Result implies same_type (other); symmetric : Result implies other.is_equal (Current); feature specification -- from P_CONTAINER count : INTEGER -- Number of items in the container. ensure positive : Result >= 0; feature specification is_writable : BOOLEAN is ??? -- Is the container currently writable? feature specification item : G -- Current item. require readable : is_readable; not_empty : not is_empty; 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 specification -- Collection interface. to_list : P_LIST [G] -- Items in stack (bottom of stack first). ensure valid_result : Result /= void; is_shallow_copy : -- new list but old items. feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. invariant empty : is_empty = (count = 0); end interface -- class P_QUEUE
The reference implementation of sets is P_HASH_SET which, as the name indicates, is implemented using a hash table. In consequence, an added constraint compared to the base P_SET is that the item type must inherit from HASHABLE.
Being based on a hash table means that search operations (or has) can be executed in constant time (assuming a good distribution of hash values). In order to maintain the average number of entries in the table under a constant, it is dynamically resized when it grows or shrinks so that some adding or removal operations may be slower when the hash table is rebuilt.
class interface P_HASH_SET [G -> HASHABLE] ancestors P_HASH_SET [G -> HASHABLE] P_SET [G] P_SEARCHABLE [G, G] P_CONTAINER [G] indexing cluster: pylon, container; description: "Set of hashable values "; interface: client; implementation: "Automatically resized hash table (indexed list of linked lists)"; warning: "Hash code must not change after item has been added to container"; creation make feature specification -- Creation make -- Create set. reset -- Create set. require writable : is_writable; ensure done : is_empty; feature specification count : INTEGER -- Number of items in the container. is_writable : BOOLEAN is ??? -- Is the container currently writable? feature specification item : G -- Current item. -- Time: O(1) require readable : is_readable; not_empty : not is_empty; feature specification -- Collection interface to_list : P_LIST [G] -- Convert the hash set to a (linked) list. -- Time: O(count) ensure done : (Result /= void) and then (Result.count = count); is_shallow_copy : -- new list, but real items feature specification search (x : G) -- Search item in container (compare using is_equal). -- Time: O(1) require readable : is_readable; ensure search_eq_has : found implies has (x); item_set : found implies item.is_equal (x); found : BOOLEAN -- Result of last search. -- Time: O(1), attribute feature specification has (it : G) : BOOLEAN -- Is the item in the container (side-effect free `search') -- Time: O(1) feature specification add (it : G) -- Add item to container. -- Time: O(1), amortised require writable : is_writable; not_void : not is_void (it); has_not : not has (it); ensure count : count = ((old count) + 1); keep_reference : has (it); remove -- Remove current item. -- Time: 0(1), amortised require writable : is_writable; not_empty : not is_empty; ensure count : count = ((old count) - 1); done : -- not has(old item) done : -- not has(old item) feature specification -- General copy (other : like Current) -- Copy set (same items). -- Time: 0(count) require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Other container equal? -- Time: O(count) require other_not_void : other /= void; ensure done_count : Result implies (count = other.count); done : -- Result implies (for_each item other.has(item)) consistent : standard_is_equal (other) implies Result; same_type : Result implies same_type (other); symmetric : Result implies other.is_equal (Current); feature specification -- Search found_count : INTEGER -- A set has only one copy of each item. require meaningful : found = true; ensure set_count : Result = 1; meaningful : Result >= 1; feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. invariant resize_up : (count // hashsize) <= (grow_entries + 1); resize_down : ((not is_empty) and then (hashsize > default_hashsize)) implies ((count // hashsize) >= (shrink_entries - 1)); has_hashtable : hashtable /= void; hashsize : hashsize = hashtable.count; current_item : (not is_empty) implies (hashlist /= void); empty : is_empty = (hashlist = void); positive : count >= 0; empty : is_empty = (count = 0); end interface -- class P_HASH_SET
A dictionary, or associative array, is a table with each item associated with a unique key (in the sense of is_equal). Therefore, is_key_writable is false for a key which is already in use.
The class P_DICTIONARY uses a hash-based set to implement the dictionary (each key and item pair is a unique node in the set).
class interface P_DICTIONARY [G, K -> HASHABLE] ancestors P_DICTIONARY [G, K -> HASHABLE] P_TABLE [G, K] P_CONTAINER [G] P_SEARCHABLE [G, K] P_CONTAINER [G] indexing cluster: pylon, container; description: "Table with one item per key"; interface: client; creation make feature specification make -- Initialise. reset -- Initialise. require writable : is_writable; ensure done : is_empty; feature specification key_search (k : K) -- Search key and set current item if successful. -- is_equal is used to compare keys. require readable : is_readable; found : BOOLEAN -- Result of key search. found_count : INTEGER is ??? -- Number of items found during the last search. feature specification -- from ANY copy (other : like Current) -- Copy. require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Equality. require other_not_void : other /= void; ensure consistent : standard_is_equal (other) implies Result; same_type : Result implies same_type (other); symmetric : Result implies other.is_equal (Current); feature specification -- from P_CONTAINER count : INTEGER -- Number of items/keys. ensure positive : Result >= 0; item : G -- Current item. require readable : is_readable; not_empty : not is_empty; key : K -- Current key. require readable : is_readable; not_empty : not is_empty; feature specification is_writable : BOOLEAN is ??? -- Is the container currently writable? is_key_writable (k : K) : BOOLEAN -- Is the key already used? require valid : not is_void (k); feature specification add (it : G; k : K) -- Add item and corresponding key. -- (key must be available). require writable : is_writable; not_void_key : not is_void (k); acceptable_key : is_key_writable (k); ensure keep_reference : -- keep copy of item and key. replace (it : G) -- Replace current item (key unchanged). require meaningful : not is_empty; writable : is_writable; ensure keep_reference : -- keep copy of item. remove -- Remove current item and associated key. require meaningful : not is_empty; writable : is_writable; feature specification -- Collection interface to_item_list : P_LIST [G] -- List of items. ensure done : Result.count = count; valid : Result /= void; is_shallow_copy : -- new list generated each time (but real items) to_key_list : P_LIST [K] -- List of keys. ensure done : Result.count = count; valid : Result /= void; is_shallow_copy : -- new list generated each time (but real keys) feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. invariant meaningful : found_count >= 1; empty : is_empty = (count = 0); end interface -- class P_DICTIONARY
A catalog is a table which can contain several items associated with a single key, so is_key_writable is always true.
The class P_CATALOG makes use of a dictionary where items are lists of items associated with the key for its implementation.
class interface P_CATALOG [G, K -> HASHABLE] ancestors P_CATALOG [G, K -> HASHABLE] P_TABLE [G, K] P_CONTAINER [G] P_SEARCHABLE [G, K] P_CONTAINER [G] indexing cluster: pylon, container; description: "Catalog (several items associated with a key)"; interface: client; creation make feature specification -- Creation make -- Initialise. reset -- Initialise. require writable : is_writable; ensure done : is_empty; feature specification -- from ANY copy (other : like Current) -- Copy from other catalog. require other_not_void : other /= void; type_identity : other.same_type (Current); ensure is_equal : is_equal (other); is_equal (other : like Current) : BOOLEAN -- Equality. require other_not_void : other /= void; ensure consistent : standard_is_equal (other) implies Result; same_type : Result implies same_type (other); symmetric : Result implies other.is_equal (Current); feature specification -- from P_CONTAINER count : INTEGER -- Number of keys in container. ensure positive : Result >= 0; is_writable : BOOLEAN is ??? -- Is the container currently writable? item : G -- Current item. require readable : is_readable; not_empty : not is_empty; feature specification -- Catalog item_list : P_LIST [G] -- List of items associated with a single key. require not_empty : not is_empty; ensure is_shallow_copy : -- list of real items in the list. feature specification -- from P_TABLE key_search (x : K) -- Search by key, compared using is_equal. require readable : is_readable; found : BOOLEAN -- Result of search. found_count : INTEGER -- Number of items found corresponding to key. require meaningful : found = true; ensure meaningful : Result >= 1; key : K -- Current key. require readable : is_readable; not_empty : not is_empty; feature specification is_key_writable (k : K) : BOOLEAN -- Is it possible to add item with corresponding key? -- (always true in catalog) require valid : not is_void (k); ensure catalog : Result = true; add (x : G; k : K) -- Add item with correspoding key. require writable : is_writable; not_void_key : not is_void (k); acceptable_key : is_key_writable (k); ensure keep_reference : -- keep copy of item and key. replace (x : G) -- Replace the first item in item list. require meaningful : not is_empty; writable : is_writable; ensure keep_reference : -- keep copy of item. remove -- Remove current key and associated item(s). require meaningful : not is_empty; writable : is_writable; feature specification to_key_list : P_LIST [K] -- List of keys in the container. ensure valid : Result /= void; is_shallow_copy : -- new list generated each time (but real keys) to_item_list : P_LIST [G] -- List of items in the containers (possibly more than keys). ensure valid : Result /= void; is_shallow_copy : -- new list generated each time (but real items) feature specification -- Status is_empty : BOOLEAN -- Is the container empty? is_readable : BOOLEAN -- Is the container currently readable? feature specification -- Output out : STRING -- String representation. ensure is_copy : -- new string not_void : Result /= void; feature specification -- Utility is_void (x : ANY) : BOOLEAN -- Void assertion for generic parameters. invariant empty : is_empty = (count = 0); end interface -- class P_CATALOG