COSTA: COSt and Termination Analyzer for Java Bytecode
    
    package net.datastructures;
/** Realization of a vector by means of an array.  The array has
  * initial length 16 and is doubled when the size of the vector
  * exceeds the capacity of the array.  No shrinking of the array is
  * performed.
  *
  * @author Roberto Tamassia
  */
public class ArrayVector implements Vector {
  private Object[] A;		// array storing the elements of the vector
  private int capacity = 16;	// initial length of array A
  private int size = 0;		// number of elements stored in the vector
  /** Creates the vector with initial capacity 16. */
  public ArrayVector() { 
    A = new Object[capacity];
  }
  /** Returns the number of elements in the vector. */
  public int size() {
    return size;
  }
  /** Returns whether the vector is empty. */
  public boolean isEmpty() {
    return size() == 0; 
  }
  /** Returns the element stored at the given rank. */
  public Object elemAtRank(int r) 
    throws BoundaryViolationException {
    checkRank(r, size());
    return A[r]; 
  }
  /** Replaces the element stored at the given rank. */
  public Object replaceAtRank(int r, Object e) 
    throws BoundaryViolationException {
    checkRank(r, size());
    Object temp = A[r];
    A[r] = e;
    return temp;
  }
  /** Inserts an element at the given rank. */
  public void insertAtRank(int r, Object e) 
    throws BoundaryViolationException {
    checkRank(r, size() + 1);
    if (size == capacity) {		// an overflow
      capacity *= 2;
      Object[] B = new Object[capacity];
      for (int i=0; i<size; i++) 
	B[i] = A[i];
      A = B;
    }
    for (int i=size-1; i>=r; i--)	// shift elements up
      A[i+1] = A[i];
    A[r] = e;
    size++;
  }
  /** Removes the element stored at the given rank. */
  public Object removeAtRank(int r) 
    throws BoundaryViolationException {
    checkRank(r, size());
    Object temp = A[r];
    for (int i=r; i<size-1; i++)	// shift elements down
      A[i] = A[i+1];
    size--;
    return temp;
  }
  /** Checks whether the given rank is in the range [0, n - 1] */
  protected void checkRank(int r, int n) 
    throws BoundaryViolationException {
    if (r < 0 || r >= n)
      throw new BoundaryViolationException("Illegal vector index: " + r);
  }
}