deferred class interface DS_STACK[G] feature(s) from DS_CONTAINER -- Measurement count: INTEGER -- Number of items in container 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 container 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 container. ensure wiped_out: is_empty feature(s) from DS_SEARCHABLE -- Status report has (v: G): BOOLEAN -- Does container 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 container -- (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 dispenser be extended with n items? require positive_n: n >= 0 feature(s) from DS_DISPENSER -- Access item: G -- Item accessible from dispenser require not_empty: not is_empty feature(s) from DS_DISPENSER -- Element change put (v: G) -- Push v on stack. require extendible: extendible(1) ensure pushed: item = v; one_more: count = old count + 1 force (v: G) -- Push v on stack. ensure pushed: item = v; one_more: count = old count + 1 extend (other: DS_LINEAR[G]) -- Add items of other to dispenser. -- 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 dispenser. -- 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 item from dispenser. require not_empty: not is_empty ensure one_less: count = old count - 1 prune (n: INTEGER) -- Remove n items from dispenser. require valid_n: 0 <= n and n <= count ensure new_count: count = old count - n keep (n: INTEGER) -- Keep n items in dispenser. require valid_n: 0 <= n and n <= count ensure new_count: count = n feature(s) from DS_STACK -- Element change replace (v: G) -- Replace top item by v. require not_empty: not is_empty ensure same_count: count = old count; replaced: item = v invariant positive_count: count >= 0; empty_definition: is_empty = count = 0; end of deferred DS_STACK[G]