deferred class interface DS_DYNAMIC_CURSOR[G]

feature(s) from DS_CURSOR
   --  Access

   item: G
      --  Item at cursor position

      require
         not_off: not off

   container: DS_TRAVERSABLE[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_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

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

end of deferred DS_DYNAMIC_CURSOR[G]