pt.ua.base
Class ArrayedQueue<T>

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

public class ArrayedQueue<T>
extends Queue<T>

Queue module implemented with an array.

invariant: Queue

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

ArrayedQueue()
Creates an unbounded queue.

ArrayedQueue(int maxSize)
Creates an bounded queue limited to maxSize elements.

Method Summary

void	clear() Empties the queue.
Queue<T>	deepClone() Clones current list.
void	in(T e) Adds an element to the tail of the queue.
boolean	isFull() Queries the list fullness.
boolean	isLimited() Checks if list is unbounded.
T	itemAt(int idx) Returns the element of the list at the idx position.
int	maxSize() The list maximum number of elements.
void	out() Removes the head element from the queue.
int	size() The list total number of elements.

Methods inherited from class pt.ua.base.Queue

copy, peek, peekIn

Methods inherited from class pt.ua.base.Indexable

headList, subList, tailList, toArray, toList, toString

Methods inherited from class pt.ua.base.Listable

isEmpty

Methods inherited from class java.lang.Object

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

Constructor Detail

ArrayedQueue

public ArrayedQueue()

Creates an unbounded queue.

ArrayedQueue

public ArrayedQueue(int maxSize)

Creates an bounded queue limited to maxSize elements.

requires: maxSize >= 0

Method Detail

isLimited

public boolean isLimited()

Description copied from class: Listable

Checks if list is unbounded.

Specified by:

isLimited in class Listable<T>

Returns:

true if list is unbounded, false otherwise

maxSize

public int maxSize()

Description copied from class: Listable

The list maximum number of elements.

requires: isLimited()

Specified by:

maxSize in class Listable<T>

Returns:

list's size

deepClone

public Queue<T> deepClone()

Description copied from class: Listable

Clones current list.

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

Specified by:

deepClone in class Queue<T>

Returns:

a deep clone of current list

in

public void in(T e)

Description copied from class: Queue

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

Specified by:

in in class Queue<T>

Parameters:

e - the element to enqueue

out

public void out()

Description copied from class: Queue

Removes the head element from the queue.

requires: !isEmpty()

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

Specified by:

out in class Queue<T>

size

public int size()

Description copied from class: Listable

The list total number of elements.

Specified by:

size in class Listable<T>

Returns:

list's size

isFull

public boolean isFull()

Description copied from class: Listable

Queries the list fullness.

Specified by:

isFull in class Listable<T>

Returns:

true if list is full, false otherwise

itemAt

public T itemAt(int idx)

Description copied from class: Indexable

Returns the element of the list at the idx position.

requires: idx >= 0 && idx < size()

Specified by:

itemAt in class Indexable<T>

Parameters:

idx - the index

Returns:

the element

clear

public void clear()

Description copied from class: Queue

Empties the queue.

ensures: isEmpty()

Specified by:

clear in class Queue<T>