Automatic generation produced by ISE Eiffel
indexing description: "[ Possibly circular sequences of items, without commitment to a particular representation ]" status: "See notice at end of class" names: chain, sequence access: index, cursor, membership contents: generic date: "$Date: 2001-11-16 20:32:23 +0000 (Fri, 16 Nov 2001) $" revision: "$Revision: 51435 $" deferred class interface CHAIN [G] feature -- Access first: like item -- Item at first position require not_empty: not is_empty last: like item -- Item at last position require not_empty: not is_empty has (v: like item): BOOLEAN -- Does chain include v? -- (Reference or object equality, -- based on object_comparison.) index_of (v: like item; i: INTEGER): INTEGER -- Index of i-th occurrence of item identical to v. -- (Reference or object equality, -- based on object_comparison.) -- 0 if none. i_th (i: INTEGER): like item -- Item at i-th position -- Was declared in CHAIN as synonym of @. infix "@" (i: INTEGER): like item -- Item at i-th position -- Was declared in CHAIN as synonym of i_th. index: INTEGER -- Current cursor index feature -- Measurement occurrences (v: like item): INTEGER -- Number of times v appears. -- (Reference or object equality, -- based on object_comparison.) index_set: INTEGER_INTERVAL -- Range of acceptable indexes ensure then count_definition: Result.count = count feature -- Cursor movement start -- Move cursor to first position. -- (No effect if empty) ensure then at_first: not is_empty implies isfirst finish -- Move cursor to last position. -- (No effect if empty) ensure then at_last: not is_empty implies islast move (i: INTEGER) -- Move cursor i positions. The cursor -- may end up off if the absolute value of i -- is too big. ensure too_far_right: (old index + i > count) implies exhausted too_far_left: (old index + i < 1) implies exhausted expected_index: (not exhausted) implies (index = old index + i) go_i_th (i: INTEGER) -- Move cursor to i-th position. require valid_cursor_index: valid_cursor_index (i) ensure position_expected: index = i feature -- Status report valid_index (i: INTEGER): BOOLEAN -- Is i within allowable bounds? ensure then valid_index_definition: Result = ((i >= 1) and (i <= count)) isfirst: BOOLEAN -- Is cursor at first position? ensure valid_position: Result implies not is_empty islast: BOOLEAN -- Is cursor at last position? ensure valid_position: Result implies not is_empty off: BOOLEAN -- Is there no current item? valid_cursor_index (i: INTEGER): BOOLEAN -- Is i correctly bounded for cursor movement? ensure valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1)) feature -- Element change put (v: like item) -- Replace current item by v. -- (Synonym for replace) ensure then same_count: count = old count put_i_th (v: like item; i: INTEGER) -- Put v at i-th position. feature -- Transformation swap (i: INTEGER) -- Exchange item at i-th position with item -- at cursor position. require not_off: not off valid_index: valid_index (i) ensure swapped_to_item: item = old i_th (i) swapped_from_item: i_th (i) = old item feature -- Duplication duplicate (n: INTEGER): like Current -- Copy of sub-chain beginning at current position -- and having min (n, from_here) items, -- where from_here is the number of items -- at or to the right of current position. require not_off_unless_after: off implies after valid_subchain: n >= 0 invariant non_negative_index: index >= 0 index_small_enough: index <= count + 1 off_definition: off = ((index = 0) or (index = count + 1)) isfirst_definition: isfirst = ((not is_empty) and (index = 1)) islast_definition: islast = ((not is_empty) and (index = count)) item_corresponds_to_index: (not off) implies (item = i_th (index)) index_set_has_same_count: index_set.count = count indexing library: "[ EiffelBase: Library of reusable components for Eiffel. ]" status: "[ Copyright 1986-2001 Interactive Software Engineering (ISE). For ISE customers the original versions are an ISE product covered by the ISE Eiffel license and support agreements. ]" license: "[ EiffelBase may now be used by anyone as FREE SOFTWARE to develop any product, public-domain or commercial, without payment to ISE, under the terms of the ISE Free Eiffel Library License (IFELL) at http://eiffel.com/products/base/license.html. ]" source: "[ Interactive Software Engineering Inc. ISE Building 360 Storke Road, Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Electronic mail <info@eiffel.com> Customer support http://support.eiffel.com ]" info: "[ For latest info see award-winning pages: http://eiffel.com ]" end -- class CHAIN -- Generated by ISE Eiffel --
For more details: www.eiffel.com