pt.ua.base
Class LinkedStack<T>

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

public class LinkedStack<T>
extends Stack<T>

Stack module implemented with a linked list.

invariant: Stack

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

LinkedStack()
Creates an unbounded stack.

LinkedStack(int maxSize)
Creates an bounded stack limited to maxSize elements.

Method Summary

void	clear() Empties the stack.
Stack<T>	deepClone() Clones current list.
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	pop() Removes the top element from the stack.
void	push(T e) Adds an element to the top of the stack.
int	size() The list total number of elements.

Methods inherited from class pt.ua.base.Stack

copy, top

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

LinkedStack

public LinkedStack()

Creates an unbounded stack.

LinkedStack

public LinkedStack(int maxSize)

Creates an bounded stack 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 Stack<T> deepClone()

Description copied from class: Listable

Clones current list.

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

Specified by:

deepClone in class Stack<T>

Returns:

a deep clone of current list

push

public void push(T e)

Description copied from class: Stack

Adds an element to the top of the stack.

requires: !isFull()

ensures: !isEmpty() && top() == e
ensures: size() == \old(size()) + 1
ensures: tailList(1).equals(\old(tailList(0)))

Specified by:

push in class Stack<T>

Parameters:

e - the element to push

pop

public void pop()

Description copied from class: Stack

Removes the top element from the stack.

requires: !isEmpty()

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

Specified by:

pop in class Stack<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: Stack

Empties the stack.

ensures: isEmpty()

Specified by:

clear in class Stack<T>