deferred class interface DS_SPARSE_TABLE[G,K]

feature(s) from DS_TRAVERSABLE
   --  Access

   item_for_iteration: G
      --  Item at internal cursor position

      require
         not_off: not off

   new_cursor: DS_SPARSE_TABLE_CURSOR[G,K]
      --  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)

feature(s) from DS_SEARCHABLE
   --  Status report

   has_item (v: G): BOOLEAN
      --  Does table include v?
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)

      ensure
         not_empty: Result implies not is_empty

   same_items (v, u: G): BOOLEAN
      --  Are v and u considered equal?
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)


   same_equality_tester (other: DS_SEARCHABLE[G]): BOOLEAN
      --  Does container use the same comparison
      --  criterion as other?

      require
         other_not_void: other /= Void

feature(s) from DS_SEARCHABLE
   --  Measurement

   occurrences (v: G): INTEGER
      --  Number of times v appears in table
      --  (Use equality_tester's comparison criterion
      --  if not void, use = criterion otherwise.)

      ensure
         positive: Result >= 0;
         has: has_item(v) implies Result >= 1

feature(s) from DS_SEARCHABLE
   --  Access

   equality_tester: DS_EQUALITY_TESTER[G]
      --  Equality tester;
      --  A void equality tester means that =
      --  will be used as comparison criterion.


feature(s) from DS_SEARCHABLE
   --  Setting

   set_equality_tester (a_tester: like equality_tester)
      --  Set equality_tester to a_tester.
      --  A void equality tester means that =
      --  will be used as comparison criterion.

      ensure
         equality_tester_set: equality_tester = a_tester

feature(s) from DS_LINEAR
   --  Access

   first: G
      --  First item in table

      require
         not_empty: not is_empty
      ensure
         has_first: has_item(Result)

feature(s) from DS_LINEAR
   --  Status report

   is_first: BOOLEAN
      --  Is internal cursor on first item?

      ensure
         not_empty: Result implies not is_empty;
         not_off: Result implies not off;
         definition: Result implies item_for_iteration = first

   after: BOOLEAN
      --  Is there no valid position to right of internal cursor?


feature(s) from DS_LINEAR
   --  Cursor movement

   start
      --  Move internal cursor to first position.

      ensure
         empty_behavior: is_empty implies after;
         not_empty_behavior: not is_empty implies is_first

   forth
      --  Move internal cursor to next position.

      require
         not_after: not after

   search_forth (v: G)
      --  Move internal cursor to first position at or after current
      --  position where item_for_iteration and v are equal.
      --  (Use equality_tester's comparison criterion
      --  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_CONTAINER
   --  Measurement

   count: INTEGER
      --  Number of items in table


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 table equal to other?
      --  Do not take cursor positions, capacity
      --  nor equality_tester into account.

      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 table.
      --  Move all cursors off.

      ensure
         wiped_out: is_empty

feature(s) from DS_TABLE
   --  Access

   infix "@" (k: K): G
      --  Item associated with k

      require
         has_k: has(k)

feature(s) from DS_TABLE
   --  Access

   item (k: K): G
      --  Item associated with k

      require
         has_k: has(k)

feature(s) from DS_TABLE
   --  Status report

   valid_key (k: K): BOOLEAN
      --  Is k a valid key?

      ensure
         defintion: Result = true

   has (k: K): BOOLEAN
      --  Is there an item associated with k?

      ensure
         valid_key: Result implies valid_key(k)

feature(s) from DS_TABLE
   --  Element change

   replace (v: G; k: K)
      --  Replace item associated with k by v.
      --  Do not move cursors.

      require
         has_k: has(k)
      ensure
         replaced: item(k) = v;
         same_count: count = old count

   force (v: G; k: K)
      --  Associate v with key k.
      --  Resize table if necessary.
      --  Move cursors off when resizing.

      require
         valid_key: valid_key(k)
      ensure
         inserted: has(k) and then item(k) = v;
         same_count: old has(k) implies count = old count;
         one_more: not old has(k) implies count = old count + 1

   force_new (v: G; k: K)
      --  Associate v with key k.
      --  Resize table if necessary.
      --  Move cursors off when resizing.

      require
         valid_key: valid_key(k);
         new_item: not has(k)
      ensure
         one_more: count = old count + 1;
         inserted: has(k) and then item(k) = v

   swap (k, l: K)
      --  Exchange items associated with k and l.

      require
         valid_k: has(k);
         valid_l: has(l)
      ensure
         same_count: count = old count;
         new_k: item(k) = old item(l);
         new_l: item(l) = old item(k)

feature(s) from DS_TABLE
   --  Removal

   remove (k: K)
      --  Remove item associated with k.
      --  Move any cursors at this position forth.

      require
         valid_key: valid_key(k)
      ensure
         same_count: not old has(k) implies count = old count;
         one_less: old has(k) implies count = old count - 1;
         removed: not has(k)

feature(s) from DS_BILINEAR
   --  Access

   last: G
      --  Last item in table

      require
         not_empty: not is_empty
      ensure
         has_last: has_item(Result)

feature(s) from DS_BILINEAR
   --  Status report

   is_last: BOOLEAN
      --  Is internal cursor on last item?

      ensure
         not_empty: Result implies not is_empty;
         not_off: Result implies not off;
         definition: Result implies item_for_iteration = last

   before: BOOLEAN
      --  Is there no valid position to left of internal cursor?


feature(s) from DS_BILINEAR
   --  Cursor movement

   finish
      --  Move internal cursor to last position.

      ensure
         empty_behavior: is_empty implies before;
         not_empty_behavior: not is_empty implies is_last

   back
      --  Move internal cursor to previous position.

      require
         not_before: not before

   search_back (v: G)
      --  Move internal cursor to first position at or before current
      --  position where item_for_iteration and v are equal.
      --  (Use equality_tester's comparison criterion
      --  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_RESIZABLE
   --  Measurement

   capacity: INTEGER
      --  Maximum number of items in table


feature(s) from DS_RESIZABLE
   --  Status report

   is_full: BOOLEAN
      --  Is container full?


feature(s) from DS_RESIZABLE
   --  Resizing

   resize (n: INTEGER)
      --  Resize table so that it can contain
      --  at least n items. Do not lose any item.
      --  Move all cursors off.

      require
         n_large_enough: n >= capacity
      ensure
         capacity_set: capacity = n

feature(s) from KL_IMPORTED_FIXED_ARRAY_TYPE
   --  Type anchors

   FIXED_ITEM_ARRAY_TYPE: FIXED_ARRAY[G]

feature(s) from KL_IMPORTED_FIXED_ARRAY_TYPE2
   --  Type anchors

   FIXED_KEY_ARRAY_TYPE: FIXED_ARRAY[G]

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
   --  Access

   key (k: K): K
      --  Key associated with k

      require
         has_k: has(k)

   found_item: G
      --  Item found by last call to search

      require
         item_found: found

   key_for_iteration: K
      --  Key at internal cursor position

      require
         not_off: not off

feature(s) from DS_SPARSE_TABLE
   --  Status report

   found: BOOLEAN
      --  Did last call to search succeed?

      ensure
         definition: Result = (found_position /= No_position)

feature(s) from DS_SPARSE_TABLE
   --  Search

   search (k: K)
      --  Search for item at key k.
      --  If found, set found to true, and set
      --  found_item to item associated with k.

      ensure
         found_set: found = has(k);
         found_item_set: found implies found_item = item(k)

feature(s) from DS_SPARSE_TABLE
   --  Duplication

   copy (other: like Current)
      --  Copy other to current table.
      --  Move all cursors off (unless other = Current).

      require
         other_not_void: other /= Void
      ensure
         is_equal: is_equal(other)

feature(s) from DS_SPARSE_TABLE
   --  Element change

   replace_found_item (v: G)
      --  Replace item associated with
      --  the key of found_item by v.
      --  Do not move cursors.

      require
         item_found: found
      ensure
         replaced: found_item = v;
         same_count: count = old count

   put (v: G; k: K)
      --  Associate v with key k.
      --  Do not move cursors.

      require
         not_full: not is_full;
         valid_key: valid_key(k)
      ensure
         same_count: old has(k) implies count = old count;
         one_more: not old has(k) implies count = old count + 1;
         inserted: has(k) and then item(k) = v

   put_new (v: G; k: K)
      --  Associate v with key k.
      --  Do not move cursors.

      require
         not_full: not is_full;
         valid_key: valid_key(k);
         new_item: not has(k)
      ensure
         one_more: count = old count + 1;
         inserted: has(k) and then item(k) = v

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;
   count_constraint: count <= capacity;
   full_definition: is_full = count = capacity;
   empty_constraint: is_empty implies off;
   internal_cursor_not_void: internal_cursor /= Void;
   valid_internal_cursor: valid_cursor(internal_cursor);
   after_constraint: after implies off;
   not_both: not (after and before);
   before_constraint: before implies off;
   items_not_void: items /= Void;
   items_count: items.count = capacity;
   keys_not_void: keys /= Void;
   keys_count: keys.count = capacity;
   clashes_not_void: clashes /= Void;
   clashes_count: clashes.count = capacity;
   slots_not_void: slots /= Void;
   slots_count: slots.count = modulus + 1;
   valid_position: position = No_position or else valid_position(position);
   capacity_constraint: capacity < modulus + 1;

end of deferred DS_SPARSE_TABLE[G,K]