deferred class interface DS_LIST_CURSOR[G]

feature(s) from DS_LINEAR_CURSOR
   --  Access

   container: DS_LIST[G]
      --  List traversed


feature(s) from DS_LINEAR_CURSOR
   --  Status report

   is_first: BOOLEAN
      --  Is cursor on first item?

      ensure
         not_empty: Result implies not container.is_empty;
         not_off: Result implies not off;
         definition: Result implies item = container.first

   after: BOOLEAN
      --  Is there no valid position to right of cursor?


   off: BOOLEAN
      --  Is there no item at cursor position?


feature(s) from DS_LINEAR_CURSOR
   --  Cursor movement

   start
      --  Move cursor to first position.

      ensure
         empty_behavior: container.is_empty implies after;
         not_empty_behavior: not container.is_empty implies is_first

   forth
      --  Move cursor to next position.

      require
         not_after: not after

   search_forth (v: G)
      --  Move to first position at or after current
      --  position where item and v are equal.
      --  (Use equality_tester's criterion from container
      --  if not void, use = criterion otherwise.)
      --  Move after if not found.

      require
         not_off: not off or after

   go_after
      --  Move cursor to after position.

      ensure
         after: after

feature(s) from DS_CURSOR
   --  Access

   item: G
      --  Item at cursor position

      require
         not_off: not off

feature(s) from DS_CURSOR
   --  Status report

   same_position (other: like Current): BOOLEAN
      --  Is current cursor at same position as other?

      require
         other_not_void: other /= Void

feature(s) from DS_CURSOR
   --  Cursor movement

   go_to (other: like Current)
      --  Move cursor to other's position.

      require
         other_not_void: other /= Void;
         valid_cursor: container.valid_cursor(other)
      ensure
         same_position: same_position(other)

feature(s) from DS_CURSOR
   --  Duplication

   copy (other: like Current)
      --  Copy other to current cursor.

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

feature(s) from DS_CURSOR
   --  Comparison

   is_equal (other: like Current): BOOLEAN
      --  Are other and current cursor at the same position?

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

feature(s) from DS_BILINEAR_CURSOR
   --  Status report

   is_last: BOOLEAN
      --  Is cursor on last item?

      ensure
         not_empty: Result implies not container.is_empty;
         not_off: Result implies not off;
         definition: Result implies item = container.last

   before: BOOLEAN
      --  Is there no valid position to left of cursor?


feature(s) from DS_BILINEAR_CURSOR
   --  Cursor movement

   finish
      --  Move cursor to last position.

      ensure
         empty_behavior: container.is_empty implies before;
         not_empty_behavior: not container.is_empty implies is_last

   back
      --  Move cursor to previous position.

      require
         not_before: not before

   search_back (v: G)
      --  Move to first position at or before current
      --  position where item and v are equal.
      --  (Use equality_tester's criterion from container
      --  if not void, use = criterion otherwise.)
      --  Move before if not found.

      require
         not_off: not off or before

   go_before
      --  Move cursor to before position.

      ensure
         before: before

feature(s) from DS_DYNAMIC_CURSOR
   --  Element change

   replace (v: G)
      --  Replace item at cursor position by v.

      require
         not_off: not off
      ensure
         replaced: item = v

   swap (other: DS_DYNAMIC_CURSOR[G])
      --  Exchange items at current and other's positions.
      --  Note: cursors may reference two different containers.

      require
         not_off: not off;
         other_not_void: other /= Void;
         other_not_off: not other.off
      ensure
         new_item: item = old other.item;
         new_other: other.item = old item

feature(s) from DS_INDEXED_CURSOR
   --  Access

   index: INTEGER
      --  Index of current position

      ensure
         valid_index: valid_index(Result)

feature(s) from DS_INDEXED_CURSOR
   --  Status report

   valid_index (i: INTEGER): BOOLEAN
      --  Is i a valid index value?

      ensure
         definition: Result = (0 <= i and i <= container.count + 1)

feature(s) from DS_INDEXED_CURSOR
   --  Cursor movement

   go_i_th (i: INTEGER)
      --  Move cursor to i-th position.

      require
         valid_index: valid_index(i)
      ensure
         moved: index = i

feature(s) from DS_LIST_CURSOR
   --  Element change

   put_left (v: G)
      --  Add v to left of cursor position.
      --  Do not move cursors.

      require
         extendible: container.extendible(1);
         not_before: not before
      ensure
         one_more: container.count = old container.count + 1

   put_right (v: G)
      --  Add v to right of cursor position.
      --  Do not move cursors.

      require
         extendible: container.extendible(1);
         not_after: not after
      ensure
         one_more: container.count = old container.count + 1

   force_left (v: G)
      --  Add v to left of cursor position.
      --  Do not move cursors.

      require
         not_before: not before
      ensure
         one_more: container.count = old container.count + 1

   force_right (v: G)
      --  Add v to right of cursor position.
      --  Do not move cursors.

      require
         not_after: not after
      ensure
         one_more: container.count = old container.count + 1

   extend_left (other: DS_LINEAR[G])
      --  Add items of other to left of cursor position.
      --  Keep items of other in the same order.
      --  Do not move cursors.

      require
         other_not_void: other /= Void;
         extendible: container.extendible(other.count);
         not_before: not before
      ensure
         new_count: container.count = old container.count + other.count

   extend_right (other: DS_LINEAR[G])
      --  Add items of other to right of cursor position.
      --  Keep items of other in the same order.
      --  Do not move cursors.

      require
         other_not_void: other /= Void;
         extendible: container.extendible(other.count);
         not_after: not after
      ensure
         new_count: container.count = old container.count + other.count

   append_left (other: DS_LINEAR[G])
      --  Add items of other to left of cursor position.
      --  Keep items of other in the same order.
      --  Do not move cursors.

      require
         other_not_void: other /= Void;
         not_before: not before
      ensure
         new_count: container.count = old container.count + other.count

   append_right (other: DS_LINEAR[G])
      --  Add items of other to right of cursor position.
      --  Keep items of other in the same order.
      --  Do not move cursors.

      require
         other_not_void: other /= Void;
         not_after: not after
      ensure
         new_count: container.count = old container.count + other.count

feature(s) from DS_LIST_CURSOR
   --  Removal

   remove
      --  Remove item at cursor position.
      --  Move any cursors at this position forth.

      require
         not_off: not off
      ensure
         one_less: container.count = old container.count - 1

   remove_left
      --  Remove item to left of cursor position.
      --  Move any cursors at this position forth.

      require
         not_empty: not container.is_empty;
         not_before: not before;
         not_first: not is_first
      ensure
         one_less: container.count = old container.count - 1

   remove_right
      --  Remove item to right of cursor position.
      --  Move any cursors at this position forth.

      require
         not_empty: not container.is_empty;
         not_after: not after;
         not_last: not is_last
      ensure
         one_less: container.count = old container.count - 1

   prune_left (n: INTEGER)
      --  Remove n items to left of cursor position.
      --  Move all cursors off.

      require
         valid_n: 0 <= n and n < index
      ensure
         new_count: container.count = old container.count - n

   prune_right (n: INTEGER)
      --  Remove n items to right of cursor position.
      --  Move all cursors off.

      require
         valid_n: 0 <= n and n <= container.count - index
      ensure
         new_count: container.count = old container.count - n

invariant
   container_not_void: container /= Void; --  The following assertion are commented out because
 --  some Eiffel compilers check invariants even when the
 --  execution of the creation procedure is not completed.
 --  (In this case, this is container which is not fully
 --  created yet, breaking its invariant.)
 -- 	empty_constraint: container.is_empty implies off
   after_constraint: after implies off;
   not_both: not (after and before);
   before_constraint: before implies off;

end of deferred DS_LIST_CURSOR[G]