org.jutil.java.collections
Class Stack

java.lang.Object
  |
  +--org.jutil.java.collections.AbstractDispenser
        |
        +--org.jutil.java.collections.Stack

All Implemented Interfaces:

Dispenser

public class Stack

extends AbstractDispenser

A Stack is a Dispenser whose elements can be removed in last-in first-out order.

Class Specifications

public invariant elements != null;

Model Field Summary
java.util.List	elements

 

Field Summary
static java.lang.String	CVS_REVISION

 

Constructor Summary

Stack()           Initialize a new empty LinkedListStack.

 

Method Summary
protected  void	addImpl(java.lang.Object item)           See superclass.
void	clear()           See superclass.
java.lang.Object	getNext()           See superclass.
java.util.Iterator	iterator()           See superclass.
int	nbExplicitOccurrences(java.lang.Object item)           See superclass.
java.lang.Object	pop()           Remove and return the top element on the stack.
void	push(java.lang.Object item)           Add a new element on top of the stack.
void	removeNext()           See superclass.
int	size()           See superclass.
java.lang.Object	top()           Return the top element on the stack.

 

Methods inherited from class org.jutil.java.collections.AbstractDispenser

add, isEmpty

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Model Field Detail

elements

public java.util.List elements

CVS_REVISION

public static final java.lang.String CVS_REVISION

Stack

public Stack()

Initialize a new empty LinkedListStack.

Specifications:

public behavior
ensures size() == 0;

push

public void push(java.lang.Object item)

Add a new element on top of the stack.

Parameters:

item - the item to add

Specifications:

public behavior
requires item != null;
ensures elements.get(size()-1) == item;
ensures nbExplicitOccurrences(item) == \old(nbExplicitOccurrences(item))+1;

top

public java.lang.Object top()

Return the top element on the stack.

Specifications:

public behavior
requires !isEmpty();
ensures \result == elements.get(size()-1);

pop

public java.lang.Object pop()

Remove and return the top element on the stack.

Specifications:

public behavior
requires !isEmpty();
ensures \result == \old(top());
ensures nbExplicitOccurrences(\old(top())) == \old(nbExplicitOccurrences(top()))-1;

size

public int size()

See superclass.

Specifications:

     also

public behavior
ensures \result == elements.size();

Specifications inherited from overridden method in interface Dispenser:

public behavior
ensures \result == ( \sum Object item; ; nbExplicitOccurrences(item));

nbExplicitOccurrences

public int nbExplicitOccurrences(java.lang.Object item)

See superclass.

Specifications inherited from overridden method in interface Dispenser:

public behavior
ensures \result >= 0;

getNext

public java.lang.Object getNext()

See superclass.

Specifications:

     also

public behavior
ensures \result == top();

Specifications inherited from overridden method in interface Dispenser:

public behavior
requires !isEmpty();
ensures nbExplicitOccurrences(\result ) > 0;

removeNext

public void removeNext()

See superclass.

Specifications inherited from overridden method in interface Dispenser:

public behavior
requires !isEmpty();
ensures nbExplicitOccurrences(\old(getNext())) == \old(nbExplicitOccurrences(getNext()))-1;

addImpl

protected void addImpl(java.lang.Object item)

See superclass.

Specifications:

     also

public behavior
ensures elements.get(size()-1) == item;

Specifications inherited from overridden method in class AbstractDispenser:

public behavior
requires item != null;
ensures nbExplicitOccurrences(item) == \old(nbExplicitOccurrences(item))+1;

iterator

public java.util.Iterator iterator()

See superclass.

clear

public void clear()

See superclass.