pt.ua.base
Class Queue<T>

java.lang.Object
  pt.ua.base.Listable<T>
      pt.ua.base.Indexable<T>
          pt.ua.base.Queue<T>

Direct Known Subclasses:

ArrayedQueue, LinkedQueue

public abstract class Queue<T>
extends Indexable<T>

Generic queue module.

invariant: !isEmpty() ==> (peek() == itemAt(0))
invariant: Indexable

This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.

Author:

Miguel Oliveira e Silva (mos@ua.pt)

Constructor Summary

Queue()

Method Summary

abstract void	clear() Empties the queue.
void	copy(Queue<T> other) Copies a queue to this queue (deep copy).
abstract Queue<T>	deepClone() Clones current list.
abstract void	in(T e) Adds an element to the tail of the queue.
abstract void	out() Removes the head element from the queue.
T	peek() Without changing the queue, returns its head element.
T	peekIn() Without changing the queue, returns its tail element.

Methods inherited from class pt.ua.base.Indexable

headList, itemAt, subList, tailList, toArray, toList, toString

Methods inherited from class pt.ua.base.Listable

isEmpty, isFull, isLimited, maxSize, size

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Queue

public Queue()

Method Detail

copy

public void copy(Queue<T> other)

Copies a queue to this queue (deep copy).

requires: other != null
requires: !isLimited() || maxSize() >= other.size()

Parameters:

other - the queue to copy from

deepClone

public abstract Queue<T> deepClone()

Description copied from class: Listable

Clones current list.

ensures: \result.size() == size()

Specified by:

deepClone in class Indexable<T>

Returns:

a deep clone of current list

in

public abstract void in(T e)

Adds an element to the tail of the queue.

requires: !isFull()

ensures: !isEmpty() && itemAt(size()-1) == e
ensures: size() == \old(size()) + 1
ensures: headList(size()-1).equals(\old(toList()))

Parameters:

e - the element to enqueue

out

public abstract void out()

Removes the head element from the queue.

requires: !isEmpty()

ensures: !isFull()
ensures: size() == \old(size()) - 1
ensures: toList().equals(\old(tailList(1)))

peek

public T peek()

Without changing the queue, returns its head element.

requires: !isEmpty()

Returns:

head element

peekIn

public T peekIn()

Without changing the queue, returns its tail element.

requires: !isEmpty()

Returns:

tail element

clear

public abstract void clear()

Empties the queue.

ensures: isEmpty()