indexing description: "Infinite sequences, indexed by integers" names: countable_sequence, infinite_sequence access: cursor, membership contents: generic deferred class interface COUNTABLE_SEQUENCE [G] feature -- Access has (v: like item): BOOLEAN -- Does structure include an occurrence of v? -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) ensure -- from CONTAINER not_found_in_empty: Result implies not empty i_th (i: INTEGER): G -- Item of rank i require -- from COUNTABLE positive_argument: i > 0 index: INTEGER -- Index of current position index_of (v: like item; i: INTEGER): INTEGER -- Index of i-th occurrence of v. -- 0 if none. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) require -- from LINEAR positive_occurrences: i > 0 ensure -- from LINEAR non_negative_result: Result >= 0 item: G -- Item at current position require -- from ACTIVE readable: readable require -- from TRAVERSABLE not_off: not off occurrences (v: G): INTEGER -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) -- (from LINEAR) ensure -- from BAG non_negative_occurrences: Result >= 0 search (v: like item) -- Move to first position (at or after current -- position) where item and v are equal. -- (Reference or object equality, -- based on object_comparison.) -- If no such position ensure that exhausted will be true. -- (from LINEAR) ensure -- from LINEAR object_found: (not exhausted and object_comparison) implies equal (v, item); item_found: (not exhausted and not object_comparison) implies v = item feature -- Status report After: BOOLEAN is false -- Is current position past last item? (Answer: no.) changeable_comparison_criterion: BOOLEAN -- May object_comparison be changed? -- (Answer: yes by default.) -- (from CONTAINER) Empty: BOOLEAN is false -- Is structure empty? (Answer: no.) -- (from INFINITE) exhausted: BOOLEAN -- Has structure been completely explored? -- (from LINEAR) ensure -- from LINEAR exhausted_when_off: off implies Result Extendible: BOOLEAN is false -- May items be added? (Answer: no.) Full: BOOLEAN is true -- The structure is complete -- (from INFINITE) object_comparison: BOOLEAN -- Must search operations use equal rather than = -- for comparing references? (Default: no, use =.) -- (from CONTAINER) off: BOOLEAN -- Is there no current item? -- (from LINEAR) Prunable: BOOLEAN is false -- May items be removed? (Answer: no.) Readable: BOOLEAN is true -- Is there a current item that may be read? -- (Answer: yes.) Writable: BOOLEAN is false -- Is there a current item that may be written? -- (Answer: no.) 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 -- Cursor movement forth -- Move to next position. require -- from LINEAR not_after: not after start -- Move to first position. invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); -- from INFINITE never_empty: not empty; always_full: full; -- from ACTIVE writable_constraint: writable implies readable; empty_constraint: empty implies (not readable) and (not writable); -- from LINEAR after_constraint: after implies off; -- from TRAVERSABLE empty_constraint: empty implies off; end -- class COUNTABLE_SEQUENCE