org.jutil.java.collections
Class SynchronizedFifoList

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

All Implemented Interfaces:

Dispenser, Fifo

public class SynchronizedFifoList

extends FifoList

Synchronized version of a FifoList.

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

SynchronizedFifoList()

 

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

 

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

iterator

 

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

SynchronizedFifoList

public SynchronizedFifoList()

push

public void push(java.lang.Object obj)

See superclass.

Specifications inherited from overridden method in class FifoList:
      --- None ---

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 class FifoList:
      --- None ---

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

getFirst

public java.lang.Object getFirst()

See superclass.

Specifications inherited from overridden method in class FifoList:
      --- None ---

Specifications inherited from overridden method in interface Fifo:

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

clear

public void clear()

See superclass/

Specifications inherited from overridden method in class FifoList:
      --- None ---

size

public int size()

See superclass.

Specifications inherited from overridden method in class FifoList:
      --- None ---

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

nbExplicitOccurrences

public int nbExplicitOccurrences(java.lang.Object item)

See superclass.

Specifications inherited from overridden method in class FifoList:
      --- None ---

Specifications inherited from overridden method in interface Dispenser:

public behavior
ensures \result >= 0;