COSTA: COSt and Termination Analyzer for Java Bytecode
    
    package net.datastructures;
/**
 * Implementation of a stack by means of a singly linked list.
 *   
 * @author Natasha Gelfand
 * @see Node
 */
/** 
 * @costaContext net/datastructures/Node
 */  
public class NodeStack implements Stack {

	protected Node top;		// reference to the head node
	protected int size;		// number of elements in the stack

	/** Creates an empty stack. */
	public NodeStack() {	// constructs an empty stack
		top = null;
		size = 0;
	}

	public int size() {
		return size;
	}

	public boolean isEmpty() {
		if (top == null)
			return true;
		return false;
	}

	public void push(Object elem) {
		Node v = new Node(elem, top);	// create and link-in a new node
		top = v;
		size++;
	}

	public Object top() throws EmptyStackException {
		if (isEmpty())
		throw new EmptyStackException("Stack is empty.");
		return top.getElement();
	}

	public Object pop() throws EmptyStackException {
		if (isEmpty())
		throw new EmptyStackException("Stack is empty.");
		Object temp = top.getElement();
		top = top.getNext();	// link-out the former top node
		size--;
		return temp;
	}

	public static void main(String[] args) {

		// Prepare the test
		NodeStack test = new NodeStack();
		for (int i = 0; i < 10; i++) {
			Integer testNumber = i;
			test.push(testNumber);
		}
		// Test
		for (int i = 0; i < 10; i++) {
			test.pop();
		}
	}

}