deferred class interface DS_LINEAR_CURSOR[G]

feature(s) from DS_CURSOR
   --  Access

   item: G
      --  Item at cursor position

      require
         not_off: not off

   container: DS_LINEAR[G]
      --  Data structure traversed


feature(s) from DS_CURSOR
   --  Status report

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


   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_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?


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

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;

end of deferred DS_LINEAR_CURSOR[G]