pt.ua.base
Class Stack<T>

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

Direct Known Subclasses:

ArrayedStack, LinkedStack

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

Generic stack module.

invariant: !isEmpty() ==> (top() == 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

Stack()

Method Summary

abstract void	clear() Empties the stack.
void	copy(Stack<T> other) Copies a stack to this stack (deep copy).
abstract Stack<T>	deepClone() Clones current list.
abstract void	pop() Removes the top element from the stack.
abstract void	push(T e) Adds an element to the top of the stack.
T	top() Without changing the stack, returns its top 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

Stack

public Stack()

Method Detail

copy

public void copy(Stack<T> other)

Copies a stack to this stack (deep copy).

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

Parameters:

other - the stack to copy from

deepClone

public abstract Stack<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

push

public abstract void push(T e)

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

Parameters:

e - the element to push

pop

public abstract void pop()

Removes the top element from the stack.

requires: !isEmpty()

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

top

public T top()

Without changing the stack, returns its top element.

requires: !isEmpty()

Returns:

top element

clear

public abstract void clear()

Empties the stack.

ensures: isEmpty()