class interface DS_HASH_TABLE_CURSOR[G,K->HASHABLE]

creation
   make (a_table: like container)
      --  Create a new cursor for a_table.

      require
         a_table_not_void: a_table /= Void
      ensure
         container_set: container = a_table;
         before: before

feature(s) from DS_LINEAR_CURSOR
   --  Access

   container: DS_HASH_TABLE[G,K]
      --  Hash table traversed


feature(s) from DS_LINEAR_CURSOR
   --  Status report

   is_first: BOOLEAN
      --  Is cursor on the 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 the 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 KL_IMPORTED_FIXED_ARRAY_ROUTINES
   --  Access

   FIXED_ANY_ARRAY_: KL_FIXED_ARRAY_ROUTINES[ANY]
      --  Routines that ought to be in class FIXED_ARRAY

      ensure
         fixed_any_array_routines_not_void: Result /= Void

   FIXED_BOOLEAN_ARRAY_: KL_FIXED_ARRAY_ROUTINES[BOOLEAN]
      --  Routines that ought to be in class FIXED_ARRAY

      ensure
         fixed_boolean_array_routines_not_void: Result /= Void

   FIXED_INTEGER_ARRAY_: KL_FIXED_ARRAY_ROUTINES[INTEGER]
      --  Routines that ought to be in class FIXED_ARRAY

      ensure
         fixed_integer_array_routines_not_void: Result /= Void

   FIXED_STRING_ARRAY_: KL_FIXED_ARRAY_ROUTINES[STRING]
      --  Routines that ought to be in class FIXED_ARRAY

      ensure
         fixed_string_array_routines_not_void: Result /= Void

feature(s) from KL_IMPORTED_FIXED_ARRAY_ROUTINES
   --  Type anchors

   FIXED_ANY_ARRAY_TYPE: FIXED_ARRAY[ANY]

   FIXED_BOOLEAN_ARRAY_TYPE: FIXED_ARRAY[BOOLEAN]

   FIXED_INTEGER_ARRAY_TYPE: FIXED_ARRAY[INTEGER]

   FIXED_STRING_ARRAY_TYPE: FIXED_ARRAY[STRING]

feature(s) from DS_SPARSE_TABLE_CURSOR
   --  Access

   key: K
      --  Key at cursor position

      require
         not_off: not off

invariant
   --  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.)
   -- 	valid_position: valid_position (position)
   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 DS_HASH_TABLE_CURSOR[G,K->HASHABLE]