class interface DS_LINKED_QUEUE[G] creation make -- Create an empty queue. -- Use = as comparison criterion. ensure empty: is_empty make_equal -- Create an empty queue. -- Use equal as comparison criterion. ensure empty: is_empty feature(s) from DS_CONTAINER -- Measurement count: INTEGER -- Number of items in queue feature(s) from DS_CONTAINER -- Status report is_empty: BOOLEAN -- Is container empty? feature(s) from DS_CONTAINER -- Comparison is_equal (other: like Current): BOOLEAN -- Is current queue equal to other? require other_not_void: other /= Void ensure consistent: standard_is_equal(other) implies Result; symmetric: Result implies other.is_equal(Current) feature(s) from DS_CONTAINER -- Removal wipe_out -- Remove all items from queue. ensure wiped_out: is_empty feature(s) from DS_SEARCHABLE -- Status report has (v: G): BOOLEAN -- Does queue include v? -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) ensure not_empty: Result implies not is_empty same_items (v, u: G): BOOLEAN -- Are v and u considered equal? -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) same_equality_tester (other: DS_SEARCHABLE[G]): BOOLEAN -- Does container use the same comparison -- criterion as other? require other_not_void: other /= Void feature(s) from DS_SEARCHABLE -- Measurement occurrences (v: G): INTEGER -- Number of times v appears in queue -- (Use equality_tester's comparison criterion -- if not void, use = criterion otherwise.) ensure positive: Result >= 0; has: has(v) implies Result >= 1 feature(s) from DS_SEARCHABLE -- Access equality_tester: DS_EQUALITY_TESTER[G] -- Equality tester; -- A void equality tester means that = -- will be used as comparison criterion. feature(s) from DS_SEARCHABLE -- Setting set_equality_tester (a_tester: like equality_tester) -- Set equality_tester to a_tester. -- A void equality tester means that = -- will be used as comparison criterion. ensure equality_tester_set: equality_tester = a_tester feature(s) from DS_DISPENSER -- Status report extendible (n: INTEGER): BOOLEAN -- May queue be extended with n items? require positive_n: n >= 0 ensure definition: Result = true feature(s) from DS_DISPENSER -- Access item: G -- Item at front of queue require not_empty: not is_empty feature(s) from DS_DISPENSER -- Element change put (v: G) -- Add v to back of queue. require extendible: extendible(1) ensure one_more: count = old count + 1 force (v: G) -- Add v to back of queue. ensure one_more: count = old count + 1 extend (other: DS_LINEAR[G]) -- Add items of other to back of queue. -- Add other.first first, etc. require other_not_void: other /= Void; extendible: extendible(other.count) ensure new_count: count = old count + other.count append (other: DS_LINEAR[G]) -- Add items of other to back of queue. -- Add other.first first, etc. require other_not_void: other /= Void ensure new_count: count = old count + other.count feature(s) from DS_DISPENSER -- Removal remove -- Remove from item from queue. require not_empty: not is_empty ensure one_less: count = old count - 1 prune (n: INTEGER) -- Remove n items from queue. require valid_n: 0 <= n and n <= count ensure new_count: count = old count - n keep (n: INTEGER) -- Keep n items in queue. require valid_n: 0 <= n and n <= count ensure new_count: count = n feature(s) from DS_LINKED_QUEUE -- Duplication copy (other: like Current) -- Copy other to current queue. require other_not_void: other /= Void ensure is_equal: is_equal(other) invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; first_cell: is_empty = first_cell = Void; last_cell: is_empty = last_cell = Void; end of DS_LINKED_QUEUE[G]