class interface ES_PRIORITY_QUEUE[G->COMPARABLE,K]
   -- 
   --  A priority queue. Each item that is put into this structure
   --  will have a cooresponding key. That item with the key
   --  will always be the first in queue.
   -- 

creation
   make (initial_capacity: INTEGER)
      --  Create with initial_capacity.
      require
         positive: initial_capacity > 0
      ensure
         empty: count = 0

feature(s) from ES_PRIORITY_QUEUE
   --  Accessors

   empty: BOOLEAN
      --  Is the queue empty?

   count: INTEGER
      --  The number of elements in the queue

   item: K
      --  The minimum item in the queue
      require
         not_empty: not empty

   key: G
      --  The minimum key in the queue
      require
         not_empty: not empty

   has (which: like item): BOOLEAN
      --  Is t in the queue?
      ensure
         sanity: Result implies not empty

   has_key (which_key: like key): BOOLEAN
      --  Is there a value which_key in the queue?
      ensure
         sanity: Result implies not empty;
         priority_condition: Result implies key <= which_key

   key_of_item (which: like item): like key
      --  Return the key associated with which.
      require
         not_void: which /= Void;
         item_present: has(which)
      ensure
         not_void: Result /= Void;
         priority: key <= Result

feature(s) from ES_PRIORITY_QUEUE
   --  Modifiers

   clear
      --  Empty the queue.
      ensure
         now_empty: empty

   put (which: like item; which_key: like key)
      --  Add which to the queue.
      require
         not_void: which /= Void and which_key /= Void;
         unique_instance: not has(which)
      ensure
         size_increased: count = old count + 1;
         now_in_queue: has(which) and has_key(which_key)

   remove (which: like item)
      --  Remove which from the queue.
      require
         present: has(which)
      ensure
         size_decreased: count = old count - 1

invariant

    non_negative: count >= 0;

    empty_definition: empty = count = 0;

    good_fit: count <= data.count;

    consitant_arrays: data.count = keys.count;

    set_beginning: data.lower = 1 and keys.lower = 1;

end of ES_PRIORITY_QUEUE[G->COMPARABLE,K]