refinement<F, E extends F>

	Element is F

    Bag[Element] is  Bag<F> {
        makeBag: --> Bag[Element]                       is Bag();
        add: Bag[Element] e:Element --> Bag[Element]    is void add(F e);
        contains: Bag[Element] e:Element                is boolean contains(F e);
        remove: Bag[Element] e:Element --> Bag[Element] is void remove(F e);
        howMany: Bag[Element] e:Element --> int         is int howMany(F e);
        isEmptyBag: Bag[Element]                        is boolean isEmpty();
    }

    TotalPreOrder is E {
        geq: POrderable e:POrderable is boolean greaterEq(E e);
    }
    
    PriorityQueue[TotalPreOrder] is HeapMinPriorityQueue<E> {
        makePQ: --> PriorityQueue[POrderable] 				
        		is HeapMinPriorityQueue();
        offer: PriorityQueue[POrderable] e:POrderable --> PriorityQueue[POrderable] 
        		is void add (E e);
        minElement: PriorityQueue[POrderable] -->? POrderable 		
        		is E min ();
        removeMin: PriorityQueue[POrderable] -->? PriorityQueue[POrderable] 
        		is void delMin ();
        isEmpty: PriorityQueue[POrderable] 					
        		is boolean isEmpty ();
        els: PriorityQueue[POrderable] --> Bag[POrderable]			
        		is Bag<E> elements();
    }    
end refinement