org.jutil.java.collections
Interface PriorityQueue

All Superinterfaces:

Dispenser

All Known Implementing Classes:

AbstractPriorityQueue

public interface PriorityQueue

extends Dispenser

A PriorityQueue is a container of objects with an associated priority/ordering, that allows the retrieval of the element with the smallest value. The order of the elements is determined by a Comparator.

See also priority-queues.webhop.org for more information on priority queues.

Field Summary
static java.lang.String	CVS_REVISION

 

Method Summary
abstract  java.util.Comparator	getComparator()           Return the comparator that is used to determine the order of the elements.
abstract  java.lang.Object	getNext()           Return the object that is next to be removed.
abstract  java.lang.Object	min()           Return the smallest object in this PriorityQueue.
abstract  java.lang.Object	pop()           Return the smallest object in this PriorityQueue and remove it.

 

Methods inherited from interface org.jutil.java.collections.Dispenser

add, isEmpty, nbExplicitOccurrences, removeNext, size

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

min

public abstract java.lang.Object min()

Return the smallest object in this PriorityQueue.

Specifications:

public behavior
requires !isEmpty();
ensures nbExplicitOccurrences(\result ) > 0;
ensures ( \forall Object o; nbExplicitOccurrences(o) > 0; ExtendedComparator.ensureExtended(getComparator()).notGreater(o,\result ));

getNext

public abstract java.lang.Object getNext()

Description copied from interface: Dispenser

Return the object that is next to be removed.

Specifications:

     also

public behavior
ensures \result == min();

Specifications inherited from overridden method in interface Dispenser:

public behavior
requires !isEmpty();
ensures nbExplicitOccurrences(\result ) > 0;

pop

public abstract java.lang.Object pop()

Return the smallest object in this PriorityQueue and remove it.

Specifications:

public behavior
requires !isEmpty();
ensures \result == \old(min());
ensures nbExplicitOccurrences(\result ) == \old(nbExplicitOccurrences(getNext()))-1;

getComparator

public abstract java.util.Comparator getComparator()

Return the comparator that is used to determine the order of the elements.

Specifications:

public behavior
ensures \result != null;