org.jutil.java.collections
Interface Dispenser

All Known Subinterfaces:

Fifo, PriorityQueue

All Known Implementing Classes:

AbstractDispenser

public interface Dispenser

A Dispenser is a Collection with an inherent order of removal of its objects, e.g. last-in first-out, first-in first-out, priority based, ...

Field Summary
static java.lang.String	CVS_REVISION

 

Method Summary
abstract  boolean	add(java.lang.Object item)           See superclass.
abstract  java.lang.Object	getNext()           Return the object that is next to be removed.
abstract  boolean	isEmpty()           Temporary substitute
abstract  int	nbExplicitOccurrences(java.lang.Object item)           Return the nummer of explicit occurrences of the given object.
abstract  void	removeNext()           Remove the next item in the removal ordering.
abstract  int	size()           See superclass.

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

add

public abstract boolean add(java.lang.Object item)

See superclass. The item is always added.

Specifications:

public behavior
requires item != null;
ensures nbExplicitOccurrences(item) == \old(nbExplicitOccurrences(item))+1;
ensures \result == true;

removeNext

public abstract void removeNext()

Remove the next item in the removal ordering.

Specifications:

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

getNext

public abstract java.lang.Object getNext()

Return the object that is next to be removed.

Specifications:

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

size

public abstract int size()

See superclass.

Specifications:

public behavior
ensures \result == ( \sum Object item; ; nbExplicitOccurrences(item));

nbExplicitOccurrences

public abstract int nbExplicitOccurrences(java.lang.Object item)

Return the nummer of explicit occurrences of the given object.

Parameters:

item - the object

Specifications:

public behavior
ensures \result >= 0;

isEmpty

public abstract boolean isEmpty()

Temporary substitute