indexing description: "Stacks (last-in, first-out dispensers), without commitment to a particular representation" names: stack, dispenser access: fixed, lifo, membership contents: generic deferred class interface STACK [G] feature -- Access has (v: G): BOOLEAN -- Does structure include v? -- (Reference or object equality, -- based on object_comparison.) -- (from CONTAINER) ensure -- from CONTAINER not_found_in_empty: Result implies not empty ensure -- from CONTAINER not_found_in_empty: Result implies not empty item: G -- Current item -- (from ACTIVE) require -- from ACTIVE readable: readable feature -- Measurement count: INTEGER -- Number of items -- (from FINITE) occurrences (v: G): INTEGER -- Number of times v appears in structure -- (Reference or object equality, -- based on object_comparison.) -- (from BAG) ensure -- from BAG non_negative_occurrences: Result >= 0 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 -- May new items be added? -- (from COLLECTION) full: BOOLEAN -- Is structure filled to capacity? -- (from BOX) object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) prunable: BOOLEAN -- May items be removed? -- (from COLLECTION) 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) extend (v: like item) -- Push v onto top. -- Was declared in STACK as synonym of extend, force and put. 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 item_pushed: item = v fill (other: LINEAR [G]) -- Fill with as many items of other as possible. -- Fill items with greatest index from other first. -- Items inserted with lowest index (from other) will -- always be on the top of stack. -- The representations of other and current structure -- need not be the same. require -- from COLLECTION other_not_void: other /= void; extendible force (v: like item) -- Push v onto top. -- Was declared in STACK as synonym of extend, force and put. ensure then item_pushed: item = v put (v: like item) -- Push v onto top. -- Was declared in STACK as synonym of extend, force and put. require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: has (v) ensure then item_pushed: item = v replace (v: like item) -- Replace top item by v. require -- from ACTIVE writable: writable ensure -- from ACTIVE item_replaced: item = v feature -- Removal remove -- Remove current item. -- (from ACTIVE) require -- from ACTIVE prunable: prunable; writable: writable wipe_out -- Remove all items. -- (from COLLECTION) require -- from COLLECTION prunable ensure -- from COLLECTION wiped_out: empty feature -- Conversion linear_representation: LINEAR [G] -- Representation as a linear structure -- (from CONTAINER) invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); -- 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; end -- class STACK