-- Automatic generation produced by ISE Eiffel --

class interface
     COLUMN [G]

create

     make
                 -- Create an empty list.
                 -- (from LINKED_LIST)
           ensure -- from LINKED_LIST
                 is_before: before

feature -- Initialization

     make
                 -- Create an empty list.
                 -- (from LINKED_LIST)
           ensure -- from LINKED_LIST
                 is_before: before
     
feature -- Access

     add (a_item: G)
                 -- Add 'a_item' to the column,
                 -- 'a_item' becomes the top
           require
                 no_void_item: a_item /= void
           ensure
                 new_count: count = old count + 1

     cursor: CURSOR
                 -- Current cursor position
                 -- (from LINKED_LIST)

     first: like item
                 -- Item at first position
                 -- (from LINKED_LIST)
           require -- from CHAIN
                 not_empty: not is_empty

     has (v: like 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 is_empty

     i_th (i: INTEGER): like item
                 -- Item at i-th position
                 -- Was declared in CHAIN as synonym of @.
                 -- (from CHAIN)
           require -- from TABLE
                 valid_key: valid_index (k)

     index: INTEGER
                 -- Index of current position
                 -- (from LINKED_LIST)

     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.
                 -- (from CHAIN)
           require -- from LINEAR
                 positive_occurrences: i > 0
           ensure -- from LINEAR
                 non_negative_result: Result >= 0

     item: G
                 -- Current item
                 -- (from LINKED_LIST)
           require -- from TRAVERSABLE
                 not_off: not off
           require -- from ACTIVE
                 readable: readable

     last: like item
                 -- Item at last position
                 -- (from LINKED_LIST)
           require -- from CHAIN
                 not_empty: not is_empty

     sequential_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

     one_from_top: G
                 -- The item under the top of the column
           ensure
                 result_is_valid: count > 1 implies Result /= void

     remove_top
                 -- Remove the top of the column.
           require
                 not_empty: not empty
           ensure
                 new_count: old count = count + 1

     the_top: G
                 -- The top of the column
           require
                 not_empty: not empty
           ensure
                 same_count: old count = count

     infix "@" (i: INTEGER): like item
                 -- Item at i-th position
                 -- Was declared in CHAIN as synonym of i_th.
                 -- (from CHAIN)
           require -- from TABLE
                 valid_key: valid_index (k)
     
feature -- Measurement

     count: INTEGER
                 -- Number of items
                 -- (from LINKED_LIST)

     index_set: INTEGER_INTERVAL
                 -- Range of acceptable indexes
                 -- (from CHAIN)
           ensure -- from INDEXABLE
                 not_void: Result /= void
           ensure then -- from CHAIN
                 Result.count = count

     occurrences (v: like 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 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 -- Status report

     after: BOOLEAN
                 -- Is there no valid cursor position to the right of cursor?
                 -- (from LINKED_LIST)

     before: BOOLEAN
                 -- Is there no valid cursor position to the left of cursor?
                 -- (from LINKED_LIST)

     changeable_comparison_criterion: BOOLEAN
                 -- May object_comparison be changed?
                 -- (Answer: yes by default.)
                 -- (from CONTAINER)

     exhausted: BOOLEAN
                 -- Has structure been completely explored?
                 -- (from LINEAR)
           ensure -- from LINEAR
                 exhausted_when_off: off implies Result

     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)

     is_empty: BOOLEAN
                 -- Is structure empty?
                 -- (from FINITE)

     isfirst: BOOLEAN
                 -- Is cursor at first position?
                 -- (from LINKED_LIST)
           ensure -- from CHAIN
                 valid_position: Result implies not is_empty

     islast: BOOLEAN
                 -- Is cursor at last position?
                 -- (from LINKED_LIST)
           ensure -- from CHAIN
                 valid_position: Result implies not is_empty

     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 LINKED_LIST)

     prunable: BOOLEAN
                 -- May items be removed? (Answer: yes.)
                 -- (from DYNAMIC_CHAIN)

     readable: BOOLEAN
                 -- Is there a current item that may be read?
                 -- (from LINKED_LIST)

     valid_cursor (p: CURSOR): BOOLEAN
                 -- Can the cursor be moved to position p?
                 -- (from LINKED_LIST)

     valid_cursor_index (i: INTEGER): BOOLEAN
                 -- Is i correctly bounded for cursor movement?
                 -- (from CHAIN)
           ensure -- from CHAIN
                 valid_cursor_index_definition: Result = ((i >= 0) and (i <= count + 1))

     valid_index (i: INTEGER): BOOLEAN
                 -- Is i within allowable bounds?
                 -- (from CHAIN)
           ensure then -- from INDEXABLE
                 only_if_in_index_set: Result implies ((i >= index_set.lower) and (i <= index_set.upper))
           ensure then -- from CHAIN
                 valid_index_definition: Result = ((i >= 1) and (i <= count))

     writable: BOOLEAN
                 -- Is there a current item that may be modified?
                 -- (from SEQUENCE)
     
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

     back
                 -- Move to previous item.
                 -- (from LINKED_LIST)
           require -- from BILINEAR
                 not_before: not before

     finish
                 -- Move cursor to last position.
                 -- (Go before if empty)
                 -- (from LINKED_LIST)
           ensure then -- from CHAIN
                 at_last: not is_empty implies islast
           ensure then -- from LINKED_LIST
                 empty_convention: is_empty implies before

     forth
                 -- Move cursor to next position.
                 -- (from LINKED_LIST)
           require -- from LINEAR
                 not_after: not after
           ensure then -- from LIST
                 moved_forth: index = old index + 1

     go_i_th (i: INTEGER)
                 -- Move cursor to i-th position.
                 -- (from LINKED_LIST)
           require -- from CHAIN
                 valid_cursor_index: valid_cursor_index (i)
           ensure -- from CHAIN
                 position_expected: index = i

     go_to (p: CURSOR)
                 -- Move cursor to position p.
                 -- (from LINKED_LIST)
           require -- from CURSOR_STRUCTURE
                 cursor_position_valid: valid_cursor (p)

     move (i: INTEGER)
                 -- Move cursor i positions. The cursor
                 -- may end up off if the offset is too big.
                 -- (from LINKED_LIST)
           ensure -- from CHAIN
                 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)
           ensure then -- from LINKED_LIST
                 moved_if_inbounds: ((old index + i) >= 0 and (old index + i) <= (count + 1)) implies index = (old index + i)
                 before_set: (old index + i) <= 0 implies before
                 after_set: (old index + i) >= (count + 1) implies after

     search (v: like item)
                 -- Move to first position (at or after current
                 -- position) where item and v are equal.
                 -- If structure does not include v ensure that
                 -- exhausted will be true.
                 -- (Reference or object equality,
                 -- based on object_comparison.)
                 -- (from BILINEAR)
           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

     start
                 -- Move cursor to first position.
                 -- (from LINKED_LIST)
           ensure then -- from CHAIN
                 at_first: not is_empty implies isfirst
           ensure then -- from LINKED_LIST
                 empty_convention: is_empty implies after
     
feature -- Element change

     append (s: SEQUENCE [G])
                 -- Append a copy of s.
                 -- (from SEQUENCE)
           require -- from SEQUENCE
                 argument_not_void: s /= void
           ensure -- from SEQUENCE
                 new_count: count >= old count

     extend (v: like item)
                 -- Add v to end.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           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

     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.
                 -- (from COLLECTION)
           require -- from COLLECTION
                 other_not_void: other /= void
                 extendible

     force (v: like item)
                 -- Add v to end.
                 -- (from SEQUENCE)
           require -- from SEQUENCE
                 extendible: extendible
           ensure then -- from SEQUENCE
                 new_count: count = old count + 1
                 item_inserted: has (v)

     merge_left (other: like Current)
                 -- Merge other into current structure before cursor
                 -- position. Do not move cursor. Empty other.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 extendible: extendible
                 not_off: not before
                 other_exists: other /= void
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count + old other.count
                 new_index: index = old index + old other.count
                 other_is_empty: other.is_empty

     merge_right (other: like Current)
                 -- Merge other into current structure after cursor
                 -- position. Do not move cursor. Empty other.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 extendible: extendible
                 not_off: not after
                 other_exists: other /= void
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count + old other.count
                 same_index: index = old index
                 other_is_empty: other.is_empty

     put (v: like item)
                 -- Replace current item by v.
                 -- (Synonym for replace)
                 -- (from CHAIN)
           require -- from COLLECTION
                 extendible: extendible
           ensure -- from COLLECTION
                 item_inserted: has (v)
           ensure then -- from CHAIN
                 same_count: count = old count

     put_front (v: like item)
                 -- Add v to beginning.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count + 1
                 item_inserted: first = v

     put_i_th (v: like item; i: INTEGER)
                 -- Put v at i-th position.
                 -- (from CHAIN)
           require -- from TABLE
                 valid_key: valid_index (k)
           ensure then -- from INDEXABLE
                 insertion_done: i_th (k) = v

     put_left (v: like item)
                 -- Add v to the left of cursor position.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 extendible: extendible
                 not_before: not before
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count + 1
                 new_index: index = old index + 1
           ensure then -- from LINKED_LIST
                 previous_exists: previous /= void
                 item_inserted: previous.item = v

     put_right (v: like item)
                 -- Add v to the right of cursor position.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 extendible: extendible
                 not_after: not after
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count + 1
                 same_index: index = old index
           ensure then -- from LINKED_LIST
                 next_exists: next /= void
                 item_inserted: not old before implies next.item = v
                 item_inserted_before: old before implies active.item = v

     replace (v: like item)
                 -- Replace current item by v.
                 -- (from LINKED_LIST)
           require -- from ACTIVE
                 writable: writable
           ensure -- from ACTIVE
                 item_replaced: item = v
     
feature -- Removal

     prune (v: like item)
                 -- Remove first occurrence of v, if any,
                 -- after cursor position.
                 -- If found, move cursor to right neighbor;
                 -- if not, make structure exhausted.
                 -- (from DYNAMIC_CHAIN)
           require -- from COLLECTION
                 prunable: prunable

     prune_all (v: like item)
                 -- Remove all occurrences of v.
                 -- (Reference or object equality,
                 -- based on object_comparison.)
                 -- Leave structure exhausted.
                 -- (from DYNAMIC_CHAIN)
           require -- from COLLECTION
                 prunable
           ensure -- from COLLECTION
                 no_more_occurrences: not has (v)
           ensure then -- from DYNAMIC_CHAIN
                 is_exhausted: exhausted

     remove
                 -- Remove current item.
                 -- Move cursor to right neighbor
                 -- (or after if no right neighbor).
                 -- (from LINKED_LIST)
           require -- from ACTIVE
                 prunable: prunable
                 writable: writable
           ensure then -- from DYNAMIC_LIST
                 after_when_empty: is_empty implies after

     remove_left
                 -- Remove item to the left of cursor position.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 left_exists: index > 1
           require else -- from DYNAMIC_LIST
                 not_before: not before
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count - 1
                 new_index: index = old index - 1

     remove_right
                 -- Remove item to the right of cursor position.
                 -- Do not move cursor.
                 -- (from LINKED_LIST)
           require -- from DYNAMIC_CHAIN
                 right_exists: index < count
           ensure -- from DYNAMIC_CHAIN
                 new_count: count = old count - 1
                 same_index: index = old index

     wipe_out
                 -- Remove all items.
                 -- (from LINKED_LIST)
           require -- from COLLECTION
                 prunable
           ensure -- from COLLECTION
                 wiped_out: is_empty
           ensure then -- from DYNAMIC_LIST
                 is_before: before
     
feature -- Transformation

     swap (i: INTEGER)
                 -- Exchange item at i-th position with item
                 -- at cursor position.
                 -- (from CHAIN)
           require -- from CHAIN
                 not_off: not off
                 valid_index: valid_index (i)
           ensure -- from CHAIN
                 swapped_to_item: item = old i_th (i)
                 swapped_from_item: i_th (i) = old item
     
feature -- Conversion

     linear_representation: LINEAR [G]
                 -- Representation as a linear structure
                 -- (from LINEAR)
     
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.
                 -- (from DYNAMIC_CHAIN)
           require -- from CHAIN
                 not_off_unless_after: off implies after
                 valid_subchain: n >= 0
     
feature -- Iteration

     do_all (action: PROCEDURE [ANY, TUPLE [G]])
                 -- Apply action to every item.
                 -- Semantics not guaranteed if action changes the structure;
                 -- in such a case, apply iterator to clone of structure instead.
                 -- (from LINEAR)
           require -- from TRAVERSABLE
                 action_exists: action /= void

     do_if (action: PROCEDURE [ANY, TUPLE [G]]; test: FUNCTION [ANY, TUPLE [G], BOOLEAN])
                 -- Apply action to every item that satisfies test.
                 -- Semantics not guaranteed if action or test changes the structure;
                 -- in such a case, apply iterator to clone of structure instead.
                 -- (from LINEAR)
           require -- from TRAVERSABLE
                 action_exists: action /= void
                 test_exits: test /= void

     for_all (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]): BOOLEAN
                 -- Is test true for all items?
                 -- (from LINEAR)
           require -- from TRAVERSABLE
                 test_exits: test /= void

     there_exists (test: FUNCTION [ANY, TUPLE [G], BOOLEAN]): BOOLEAN
                 -- Is test true for at least one item?
                 -- (from LINEAR)
           require -- from TRAVERSABLE
                 test_exits: test /= void
     
invariant

           -- from ANY
     reflexive_equality: standard_is_equal (Current)
     reflexive_conformance: conforms_to (Current)
           -- from LINKED_LIST
     prunable: prunable
     empty_constraint: is_empty implies ((first_element = void) and (active = void))
     not_void_unless_empty: (active = void) implies is_empty
     before_constraint: before implies (active = first_element)
     after_constraint: after implies (active = last_element)
           -- from LIST
     before_definition: before = (index = 0)
     after_definition: after = (index = count + 1)
           -- from CHAIN
     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
           -- from ACTIVE
     writable_constraint: writable implies readable
     empty_constraint: is_empty implies (not readable) and (not writable)
           -- from INDEXABLE
     index_set_not_void: index_set /= void
           -- from BILINEAR
     not_both: not (after and before)
     before_constraint: before implies off
           -- from LINEAR
     after_constraint: after implies off
           -- from TRAVERSABLE
     empty_constraint: is_empty implies off
           -- from FINITE
     empty_definition: is_empty = (count = 0)
     non_negative_count: count >= 0
           -- from DYNAMIC_CHAIN
     extendible: extendible

end -- class COLUMN

-- Generated by ISE Eiffel --

-- For more details: www.eiffel.com --