org.jutil.java.collections
Class AbstractFifo

java.lang.Object
  |
  +--org.jutil.java.collections.AbstractDispenser
        |
        +--org.jutil.java.collections.AbstractFifo

All Implemented Interfaces:

Dispenser, Fifo

Direct Known Subclasses:

FifoList

public abstract class AbstractFifo

extends AbstractDispenser

implements Fifo

AbstractFifo provides an implementation for several Dispenser methods, delegating them to the corresponding Fifo methods.

Specifications inherited from interface Fifo

public invariant elements != null;

Model fields inherited from interface org.jutil.java.collections.Fifo

elements

 

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

AbstractFifo()

 

Method Summary
protected  void	addImpl(java.lang.Object item)           See superclass
java.lang.Object	getNext()           See superclass
void	removeNext()           See superclass

 

Methods inherited from class org.jutil.java.collections.AbstractDispenser

add, isEmpty

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

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

getFirst, pop, push, size

 

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

add, isEmpty, nbExplicitOccurrences

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

AbstractFifo

public AbstractFifo()

addImpl

protected void addImpl(java.lang.Object item)

See superclass

Specifications inherited from overridden method in class AbstractDispenser:

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

removeNext

public void removeNext()

See superclass

Specifications inherited from overridden method in interface Dispenser:

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

getNext

public java.lang.Object getNext()

See superclass

Specifications inherited from overridden method in interface Fifo:

     also

public behavior
ensures \result == getFirst();

Specifications inherited from overridden method in interface Dispenser:

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