org.jutil.java.collections
Interface Fifo

All Superinterfaces:

Dispenser

All Known Implementing Classes:

AbstractFifo

public interface Fifo

extends Dispenser

Interface for first-in first-out like datastructures.

Class Specifications

public invariant elements != null;

Model Field Summary
static java.util.List	elements

 

Field Summary
static java.lang.String	CVS_REVISION

 

Method Summary
abstract  java.lang.Object	getFirst()
abstract  java.lang.Object	getNext()           See superclass.
abstract  java.lang.Object	pop()           Pop the first object from this fifo.
abstract  void	push(java.lang.Object item)           Push a new object in the Fifo.
abstract  int	size()           See superclass.

 

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

add, isEmpty, nbExplicitOccurrences, removeNext

 

Model Field Detail

elements

public static java.util.List elements

CVS_REVISION

public static final java.lang.String CVS_REVISION

size

public abstract int size()

See superclass.

Specifications:

     also

public behavior
ensures \result == elements.size();

Specifications inherited from overridden method in interface Dispenser:

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

push

public abstract void push(java.lang.Object item)

Push a new object in the Fifo.

Parameters:

item - The object to be put in the fifo.

Specifications:

public behavior
requires size() < Integer.MAX_VALUE;
ensures elements.get(elements.size()-1) == item;
ensures nbExplicitOccurrences(item) == \old(nbExplicitOccurrences(item))+1;

getFirst

public abstract java.lang.Object getFirst()

Specifications:

public behavior
requires !isEmpty();
ensures \result == elements.get(0);

getNext

public abstract java.lang.Object getNext()

See superclass.

Specifications:

     also

public behavior
ensures \result == getFirst();

Specifications inherited from overridden method in interface Dispenser:

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

pop

public abstract java.lang.Object pop()

Pop the first object from this fifo.

Specifications:

public behavior
requires !isEmpty();
ensures \result == \old(getFirst());
ensures nbExplicitOccurrences(\result ) == \old(nbExplicitOccurrences(getNext()))-1;
ensures ( \forall int index; index >= 0&&index < size(); elements.get(index) == \old(elements.get(index+1)));