deferred class interface DS_TABLE[G,K]

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_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?


   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.

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

   put (v: G; k: K)
      --  Associate v with key k.

      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

   put_new (v: G; k: K)
      --  Associate v with key k.

      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.

      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)

invariant
   positive_count: count >= 0;
   empty_definition: is_empty = count = 0;

end of deferred DS_TABLE[G,K]