indexing "Unbounded stacks implemented as linked lists" names: linked_stack, dispenser, linked_list representation: linked access: fixed, lifo, membership contents: generic class interface LINKED_STACK [G] create make -- Create an empty list. -- (from LINKED_LIST) feature {ANY} -- Initialization make -- Create an empty list. -- (from LINKED_LIST) 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 -- Item at the first position require -- from ACTIVE readable: readable 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: like item) -- Push v onto top. 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 -- from STACK 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. -- (from STACK) require -- from COLLECTION other_not_void: other /= void; extendible force (v: like item) -- Push v onto top. require -- from SEQUENCE extendible: extendible ensure then -- from SEQUENCE new_count: count = old count + 1; item_inserted: has (v) ensure then -- from STACK item_pushed: item = v put (v: like item) require -- from COLLECTION extendible: extendible ensure -- from COLLECTION item_inserted: has (v) ensure then -- from STACK item_pushed: 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 on top. require -- from ACTIVE prunable: prunable; writable: writable 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 reverse of original order of insertion) feature -- Duplication duplicate (n: INTEGER): like Current -- New stack containing the n latest items inserted -- in current stack. -- If n is greater than count, identical to current stack. 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); -- 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_STACK