deferred class interface DS_INDEXED_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_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?


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

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_INDEXED_CURSOR[G]