org.jutil.java.collections
Interface Fifo

All Known Implementing Classes:

FifoList

public interface Fifo

Interface for first-in first-out like datastructures.

Version:

$Revision: 1.3 $

Author:

Tom Schrijvers, Marko van Dooren

Method Summary

void	clear() public behavior post size() == 0; Clear the list.
boolean	isEmpty() public behavior post \result == (size() == 0); Check whether or not this Fifo is empty.
java.lang.Object	pop() public behavior pre size() > 0; post elements.size() == \old(elements.size()) - 1; post \result == \old(elements.get(elements.size() - 1)); Pop the first object from this fifo.
void	push(java.lang.Object obj) public invariant size() >= 0; // A model field representing the elements in this Fifo.
int	size() public behavior post \result == elements.size(); Return the size of this BlockingFifoList.

Method Detail

push

public void push(java.lang.Object obj)

public invariant size() >= 0;

// A model field representing the elements in this Fifo. Necessary
// in order to write full specifications, but we don't want to provide
// a getElements() method.
public model List elements;
public invariant elements != null;

public behavior

pre size() < Integer.MAX_VALUE;

post elements.size() == \old(elements.size()) + 1;
post elements.get(elements.size() - 1) == obj;
Push a new object in the Fifo.

Parameters:

object - The object to be put in the fifo.

pop

public java.lang.Object pop()

public behavior

pre size() > 0;

post elements.size() == \old(elements.size()) - 1;
post \result == \old(elements.get(elements.size() - 1));
Pop the first object from this fifo.

clear

public void clear()

public behavior

post size() == 0;
Clear the list.

size

public int size()

public behavior

post \result == elements.size();
Return the size of this BlockingFifoList.

isEmpty

public boolean isEmpty()

public behavior

post \result == (size() == 0);
Check whether or not this Fifo is empty.