class interface P_CATALOG[G,K->HASHABLE]

creation
   make
      --  Initialise.


feature(s) from P_CONTAINER
   --  Status

   count: INTEGER
      --  Number of keys in container.

      ensure
         positive: Result >= 0

   is_empty: BOOLEAN
      --  Is the container empty?


   is_readable: BOOLEAN
      --  Is the container currently readable?


   is_writable: BOOLEAN
      --  Catalog is always writable.


   item: G
      --  Current item.

      require
         readable: is_readable;
         not_empty: not is_empty

feature(s) from P_CONTAINER
   --  Update

   reset
      --  Initialise.

      require
         writable: is_writable
      ensure
         done: is_empty

feature(s) from P_CONTAINER
   --  Output

   out: STRING
      --  String representation.

      ensure
         is_copy:  --  new string

feature(s) from P_CONTAINER
   --  Utility

   is_void (x: ANY): BOOLEAN
      --  Void assertion for generic parameters.


feature(s) from P_SEARCHABLE
   --  Search

   key_search (x: K)
      --  Search by key, compared using is_equal.

      require
         readable: is_readable

   found: BOOLEAN
      --  Result of search.


   found_count: INTEGER
      --  Number of items found corresponding to key.

      require
         meaningful: found = true
      ensure
         meaningful: Result >= 1

feature(s) from P_TABLE
   --  Status

   key: K
      --  Current key.

      require
         readable: is_readable;
         not_empty: not is_empty

   is_key_writable (k: K): BOOLEAN
      --  Is it possible to add item with corresponding key?
      --  (always true in catalog)

      require
         valid: not is_void(k)
      ensure
         catalog: Result = true

feature(s) from P_TABLE
   --  Update

   add (x: G; k: K)
      --  Add item with correspoding key.

      require
         writable: is_writable;
         not_void_key: not is_void(k);
         acceptable_key: is_key_writable(k)
      ensure
         keep_reference:  --  keep copy of item and key.

   replace (x: G)
      --  Replace the first item in item list.

      require
         meaningful: not is_empty;
         writable: is_writable
      ensure
         keep_reference:  --  keep copy of item.

   remove
      --  Remove current key and associated item(s).

      require
         meaningful: not is_empty;
         writable: is_writable

feature(s) from P_TABLE
   --  Conversion

   to_key_list: P_LIST[K]
      --  List of keys in the container.

      ensure
         valid: Result /= Void; --  new list generated each time (but real keys)
         is_shallow_copy: 

   to_item_list: P_LIST[G]
      --  List of items in the containers (possibly more than keys).

      ensure
         valid: Result /= Void; --  new list generated each time (but real items)
         is_shallow_copy: 

feature(s) from P_CATALOG
   --  Creation

   make
      --  Initialise.


feature(s) from P_CATALOG
   --  from ANY

   copy (other: like Current)
      --  Copy from other catalog.

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

   is_equal (other: like Current): BOOLEAN
      --  Equality.

      require
         other_not_void: other /= Void
      ensure
         consistent: standard_is_equal(other) implies Result;
         symmetric: Result implies other.is_equal(Current)

feature(s) from P_CATALOG
   --  Catalog

   item_list: P_LIST[G]
      --  List of items associated with a single key.

      require
         not_empty: not is_empty
      ensure
         is_shallow_copy:  --  list of real items in the list.

invariant
   empty: is_empty = count = 0;

end of P_CATALOG[G,K->HASHABLE]