org.jutil.java.collections
Class FifoList

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

All Implemented Interfaces:

Dispenser, Fifo

Direct Known Subclasses:

BlockingFifoList, SynchronizedFifoList

public class FifoList

extends AbstractFifo

FifoList is a class of objects that represent simple first-in first-out lists .

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

FifoList()           Initialize a new empty FifoList.

 

Method Summary
void	clear()           See superclass/
java.lang.Object	getFirst()           See superclass.
java.util.Iterator	iterator()           See superclass.
int	nbExplicitOccurrences(java.lang.Object item)           See superclass.
java.lang.Object	pop()           See superclass.
void	push(java.lang.Object object)           See superclass.
int	size()           See superclass.

 

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

addImpl, getNext, removeNext

 

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.Dispenser

add, isEmpty

 

Field Detail

CVS_REVISION

public static final java.lang.String CVS_REVISION

FifoList

public FifoList()

Initialize a new empty FifoList.

Specifications:

public behavior
ensures size() == 0;

push

public void push(java.lang.Object object)

See superclass.

Specifications inherited from overridden method in interface Fifo:

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

pop

public java.lang.Object pop()

See superclass.

Specifications inherited from overridden method in interface Fifo:

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)));

clear

public void clear()

See superclass/

iterator

public java.util.Iterator iterator()

See superclass.

size

public int size()

See superclass.

Specifications inherited from overridden method in interface Fifo:

     also

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

Specifications inherited from overridden method in interface Dispenser:

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

getFirst

public java.lang.Object getFirst()

See superclass.

Specifications inherited from overridden method in interface Fifo:

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

nbExplicitOccurrences

public int nbExplicitOccurrences(java.lang.Object item)

See superclass.

Specifications inherited from overridden method in interface Dispenser:

public behavior
ensures \result >= 0;