deferred class interface DS_TRAVERSABLE[G]

feature(s) from DS_CONTAINER
   --  Measurement

   count: INTEGER
      --  Number of items in container


feature(s) from DS_CONTAINER
   --  Status report

   is_empty: BOOLEAN
      --  Is container empty?


feature(s) from DS_CONTAINER
   --  Comparison

   is_equal (other: like Current): BOOLEAN
      --  Is current container equal to other?

      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_CONTAINER
   --  Removal

   wipe_out
      --  Remove all items from container.

      ensure
         wiped_out: is_empty

feature(s) from DS_TRAVERSABLE
   --  Access

   item_for_iteration: G
      --  Item at internal cursor position

      require
         not_off: not off

   new_cursor: DS_CURSOR[G]
      --  New external cursor for traversal

      ensure
         cursor_not_void: Result /= Void;
         valid_cursor: valid_cursor(Result)

feature(s) from DS_TRAVERSABLE
   --  Status report

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


   same_position (a_cursor: like new_cursor): BOOLEAN
      --  Is internal cursor at same position as a_cursor?

      require
         a_cursor_not_void: a_cursor /= Void

   valid_cursor (a_cursor: DS_CURSOR[G]): BOOLEAN
      --  Is a_cursor a valid cursor?

      require
         a_cursor_not_void: a_cursor /= Void

feature(s) from DS_TRAVERSABLE
   --  Cursor movement

   go_to (a_cursor: like new_cursor)
      --  Move internal cursor to a_cursor's position.

      require
         cursor_not_void: a_cursor /= Void;
         valid_cursor: valid_cursor(a_cursor)
      ensure
         same_position: same_position(a_cursor)

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;
   empty_constraint: is_empty implies off;
   internal_cursor_not_void: internal_cursor /= Void;
   valid_internal_cursor: valid_cursor(internal_cursor);

end of deferred DS_TRAVERSABLE[G]