Automatic generation produced by ISE Eiffel
note description: "[ Possibly circular sequences of items, without commitment to a particular representation ]" library: "Free implementation of ELKS library" legal: "See notice at end of class." status: "See notice at end of class." names: chain, sequence access: index, cursor, membership contents: generic date: "$Date: 2016-03-02 13:15:09 -0800 (Wed, 02 Mar 2016) $" revision: "$Revision: 98557 $" 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_32): INTEGER_32 -- Index of `i'-th occurrence of item identical to `v'. -- (Reference or object equality, -- based on object_comparison.) -- 0 if none. i_th alias "[]" (i: INTEGER_32): like item assign put_i_th -- Item at `i'-th position -- Was declared in CHAIN as synonym of at. at alias "@" (i: INTEGER_32): like item assign put_i_th -- Item at `i'-th position -- Was declared in CHAIN as synonym of i_th. feature -- Measurement occurrences (v: like item): INTEGER_32 -- Number of times `v' appears. -- (Reference or object equality, -- based on object_comparison.) Lower: INTEGER_32 = 1 -- Minimum index. 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_32) -- 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_32) -- 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_32): 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_32): 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) require writeable: writable replaceable: replaceable ensure same_count: count = old count is_inserted: is_inserted (v) put_i_th (v: like item; i: INTEGER_32) -- Put `v' at `i'-th position. append (s: SEQUENCE [G]) -- Append a copy of `s'. fill (other: CONTAINER [G]) -- Fill with as many items of `other' as possible. -- The representations of `other' and current structure -- need not be the same. feature -- Transformation swap (i: INTEGER_32) -- 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_32): 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)) note copyright: "Copyright (c) 1984-2016, Eiffel Software and others" license: "Eiffel Forum License v2 (see http://www.eiffel.com/licensing/forum.txt)" source: "[ Eiffel Software 5949 Hollister Ave., Goleta, CA 93117 USA Telephone 805-685-1006, Fax 805-685-6869 Website http://www.eiffel.com Customer support http://support.eiffel.com ]" end -- class CHAIN -- Generated by ISE Eiffel --
For more details: www.eiffel.com