indexing description: "Unbounded queues implemented as linked lists" names: linked_queue, dispenser, linked_list representation: linked access: fixed, fifo, membership contents: generic class interface LINKED_QUEUE [G] create make feature -- Initialization make feature -- Access has (v: like ll_item): BOOLEAN -- Does chain include v? -- (Reference or object equality, -- based on object_comparison.) -- (from CHAIN) ensure -- from CONTAINER not_found_in_empty: Result implies not empty item: G -- Oldest item require -- from ACTIVE readable: readable require else not empty occurrences (v: like ll_item): INTEGER -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from CHAIN) ensure -- from BAG non_negative_occurrences: Result >= 0 occurrences (v: like ll_item): INTEGER -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from CHAIN) ensure -- from BAG non_negative_occurrences: Result >= 0 feature -- Measurement count: INTEGER -- Number of items -- (from LINKED_LIST) feature -- Status report changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) empty: BOOLEAN -- Is structure empty? -- (from FINITE) Extendible: BOOLEAN is true -- May new items be added? (Answer: yes.) -- (from DYNAMIC_CHAIN) Full: BOOLEAN is false -- Is structured filled to capacity? (Answer: no.) -- (from LINKED_LIST) object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? (Answer: yes.) -- (from DYNAMIC_CHAIN) readable: BOOLEAN -- Is there a current item that may be read? -- (from DISPENSER) writable: BOOLEAN -- Is there a current item that may be modified? -- (from DISPENSER) feature -- Status setting compare_objects -- Ensure that future search operations will use equal -- rather than = for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion ensure -- from CONTAINER object_comparison compare_references -- Ensure that future search operations will use = -- rather than equal for comparing references. -- (from CONTAINER) require -- from CONTAINER changeable_comparison_criterion ensure -- from CONTAINER reference_comparison: not object_comparison feature -- Element change append (s: SEQUENCE [G]) -- Append a copy of s. -- (Synonym for fill) -- (from DISPENSER) require -- from SEQUENCE argument_not_void: s /= void ensure -- from SEQUENCE new_count: count >= old count extend (v: G) -- Add v as newest item. -- Was declared in LINKED_QUEUE as synonym of put, extend and force. require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: has (v) ensure then -- from BAG one_more_occurrence: occurrences (v) = old (occurrences (v)) + 1 ensure then (old empty) implies (item = v) fill (other: CONTAINER [G]) -- Fill with as many items of other as possible. -- The representations of other and current structure -- need not be the same. -- (from COLLECTION) require -- from COLLECTION other_not_void: other /= void; extendible require -- from COLLECTION other_not_void: other /= void; extendible force (v: G) -- Add v as newest item. -- Was declared in LINKED_QUEUE as synonym of put, extend and force. require -- from SEQUENCE extendible: extendible ensure then -- from SEQUENCE new_count: count = old count + 1; item_inserted: has (v) ensure then (old empty) implies (item = v) put (v: G) -- Add v as newest item. -- Was declared in LINKED_QUEUE as synonym of put, extend and force. require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: has (v) ensure then (old empty) implies (item = v) replace (v: like ll_item) -- Replace current item by v. -- (from LINKED_LIST) require -- from ACTIVE writable: writable ensure -- from ACTIVE item_replaced: item = v feature -- Removal remove -- Remove item to the left of cursor position. -- Do not move cursor. -- (from LINKED_LIST) require -- from DYNAMIC_CHAIN left_exists: index > 1 require else -- from DYNAMIC_LIST not_before: not before ensure -- from DYNAMIC_CHAIN new_count: count = old count - 1; wipe_out -- Remove all items. -- (from LINKED_LIST) require -- DYNAMIC_LIST precursor: True require -- from COLLECTION prunable ensure -- from COLLECTION wiped_out: empty feature -- Conversion linear_representation: ARRAYED_LIST [G] -- Representation as a linear structure -- (order is same as original order of insertion) feature -- Duplication duplicate (n: INTEGER): like Current -- New queue containing the n oldest items in current queue. -- If n is greater than count, identical to current queue. require -- from CHAIN not_off_unless_after: off implies after; valid_subchain: n >= 0 require else positive_argument: n > 0 invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); is_always_after: not empty implies after; -- from DISPENSER readable_definition: readable = not empty; writable_definition: writable = not empty; -- from ACTIVE writable_constraint: writable implies readable; empty_constraint: empty implies (not readable) and (not writable); -- from FINITE empty_definition: empty = (count = 0); non_negative_count: count >= 0; -- from LINKED_LIST prunable: prunable; -- from DYNAMIC_CHAIN extendible: extendible; end -- class LINKED_QUEUE