org.jutil.java.collections
Class BlockingFifoList

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

All Implemented Interfaces:

Dispenser, Fifo

public class BlockingFifoList

extends FifoList

Synchronized fifo list that will block the request to pop the first object until a first object is present.

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

BlockingFifoList()           Initialize a new empty blocking fifo list.

 

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

BlockingFifoList

public BlockingFifoList()

Initialize a new empty blocking fifo list.

Specifications:

public behavior
ensures size() == 0;

push

public void push(java.lang.Object object)

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. Will block until the list is non-empty.

Specifications:

     also

public behavior
requires true;

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;