COSTA: COSt and Termination Analyzer for Java Bytecode
    
    package net.datastructures;
import java.util.Iterator;
/**  
 * Realization of a List using a doubly-linked list of nodes.
 *   
 * @author Michael Goodrich, Natasha Gelfand, Roberto Tamassia, Eric Zamore
 */
/** 
 * @costaContext net/datastructures/DNode
 */  
public class NodeList implements List {

	protected int numElts;            	// Number of elements in the list
	protected DNode header, trailer;	// Special sentinels

	/** Constructor that creates an empty list; O(1) time */
	public NodeList() {
		numElts = 0;
		header = new DNode(null, null, null);	// create header
		trailer = new DNode(header, null, null);	// create trailer
		header.setNext(trailer);	// make header and trailer point to each other
	}

	/** Checks if position is valid for this list and converts it to
	 *  DNode if it is valid; O(1) time */
	protected DNode checkPosition(Position p) throws InvalidPositionException {
		if (p == null)
			throw new InvalidPositionException	
			("Null position passed to NodeList");
		if (p == header)
			throw new InvalidPositionException
			("The header node is not a valid position");
		if (p == trailer)
			throw new InvalidPositionException
			("The trailer node is not a valid position");
		try {
			DNode temp = (DNode)p;
			if ((temp.getPrev() == null) || (temp.getNext() == null))
				throw new InvalidPositionException
				("Position does not belong to a valid NodeList");
			return temp;
		} catch (ClassCastException e) {
			throw new InvalidPositionException
			("Position is of wrong type for this list");
		}
	}

	/** Returns the number of elements in the list;  O(1) time */
	public int size() { return numElts; }

	/** Returns whether the list is empty;  O(1) time  */
	public boolean isEmpty() { return (numElts == 0); }

	/** Returns the first position in the list; O(1) time */
	public Position first()
		throws EmptyListException {
		if (isEmpty())
			throw new EmptyListException("List is empty");
		return header.getNext();
	}

	/** Returns the last position in the list; O(1) time */
	public Position last()
		throws EmptyListException {
		if (isEmpty())
			throw new EmptyListException("List is empty");
		return trailer.getPrev();
	}

	/** Returns the position before the given one; O(1) time */
	public Position prev(Position p)
		throws InvalidPositionException, BoundaryViolationException {
		DNode v = checkPosition(p);
		DNode prev = v.getPrev();
		if (prev == header)
			throw new BoundaryViolationException
			("Cannot advance past the beginning of the list");
		return prev;
	}

	/** Returns the position after the given one; O(1) time */
	public Position next(Position p)
		throws InvalidPositionException, BoundaryViolationException {
		DNode v = checkPosition(p);
		DNode next = v.getNext();
		if (next == trailer)
			throw new BoundaryViolationException
			("Cannot advance past the end of the list");
		return next;
	}

	/** Insert the given element before the given position, returning
	 * the new position; O(1) time  */
	public Position insertBefore(Position p, Object element) 
		throws InvalidPositionException {			// 
		DNode v = checkPosition(p);
		numElts++;
		DNode newNode = new DNode(v.getPrev(), v, element);
		v.getPrev().setNext(newNode);
		v.setPrev(newNode);
		return newNode;
	}

	/** Insert the given element after the given position, returning the
	 * new position; O(1) time  */
	public Position insertAfter(Position p, Object element) 
		throws InvalidPositionException {
		DNode v = checkPosition(p);
		numElts++;
		DNode newNode = new DNode(v, v.getNext(), element);
		v.getNext().setPrev(newNode);
		v.setNext(newNode);
		return newNode;
	}

	/** Insert the given element at the beginning of the list, returning
	 * the new position; O(1) time  */
	public Position insertFirst(Object element) {
		numElts++;
		DNode newNode = new DNode(header, header.getNext(), element);
		header.getNext().setPrev(newNode);
		header.setNext(newNode);
		return newNode;
	}

	/** Insert the given element at the end of the list, returning
	 * the new position; O(1) time  */
	public Position insertLast(Object element) {
		numElts++;
		DNode oldLast = trailer.getPrev();
		DNode newNode = new DNode(oldLast, trailer, element);
		oldLast.setNext(newNode);
		trailer.setPrev(newNode);
		return newNode;
	}

	/**Remove the given position from the list; O(1) time */
	public Object remove(Position p)
		throws InvalidPositionException {
		DNode v = checkPosition(p);
		numElts--;
		DNode vPrev = v.getPrev();
		DNode vNext = v.getNext();
		vPrev.setNext(vNext);
		vNext.setPrev(vPrev);
		Object vElem = v.element();
		// unlink the position from the list and make it invalid
		v.setNext(null);
		v.setPrev(null);
		return vElem;
	}

	/** Replace the element at the given position with the new element
	 * and return the old element; O(1) time  */
	public Object replace(Position p, Object element)
		throws InvalidPositionException {
		DNode v = checkPosition(p);
		Object oldElt = v.element();
		v.setElement(element);
		return oldElt;
}

	/** Returns an iterator of all the nodes in the list. */
	public Iterator positions() { return new PositionIterator(this); }
	/** Returns an iterator of all the elements in the list. */
	public Iterator elements() { return new ElementIterator(this); }

	// Convenience methods
	/** Returns whether a position is the first one;  O(1) time */
	public boolean isFirst(Position p)
		throws InvalidPositionException {  
		DNode v = checkPosition(p);
		return v.getPrev() == header;
	}

	/** Returns whether a position is the last one;  O(1) time */
	public boolean isLast(Position p)
		throws InvalidPositionException {  
		DNode v = checkPosition(p);
		return v.getNext() == trailer;
	}

	/** Swap the elements of two give positions;  O(1) time */ 
	public void swapElements(Position a, Position b) 
		throws InvalidPositionException {
		DNode pA = checkPosition(a);
		DNode pB = checkPosition(b);
		Object temp = pA.element();
		pA.setElement(pB.element());
		pB.setElement(temp);
	}

	/** Returns a textual representation of the list */
	public String toString() {
		String s = "[";
		if (!isEmpty()) {
			Position p = first();
			while (true) {
				s += p.element();
				if (p==last())
					break; 
				s += ", ";
				p = next(p);
			}
		}
		s += "]";
		return s;
	}

	public static void main(String[] args) {

		// Prepare the test
		NodeList test = new NodeList();
		Position p = null;
		/*for (int i = 0; i < 25; i++) {
			Integer testNumber = i;
			p = test.insertLast(testNumber);
			}*/
		// Test
		//for (int i = 0; i < 10; i++) {
			p = test.prev(p);
			//}
		
	}
}