Vector class implements a growable array of
* objects. Like an array, it contains components that can be
* accessed using an integer index. However, the size of a
* Vector can grow or shrink as needed to accommodate
* adding and removing items after the Vector has been created.
*
* Each vector tries to optimize storage management by maintaining a
* capacity and a capacityIncrement. The
* capacity is always at least as large as the vector
* size; it is usually larger because as components are added to the
* vector, the vector's storage increases in chunks the size of
* capacityIncrement. An application can increase the
* capacity of a vector before inserting a large number of
* components; this reduces the amount of incremental reallocation.
* * As of the Java 2 platform v1.2, this class has been retrofitted to * implement List, so that it becomes a part of Java's collection framework. * Unlike the new collection implementations, Vector is synchronized.
* * The Iterators returned by Vector's iterator and listIterator * methods are fail-fast: if the Vector is structurally modified * at any time after the Iterator is created, in any way except through the * Iterator's own remove or add methods, the Iterator will throw a * ConcurrentModificationException. Thus, in the face of concurrent * modification, the Iterator fails quickly and cleanly, rather than risking * arbitrary, non-deterministic behavior at an undetermined time in the future. * The Enumerations returned by Vector's elements method are not * fail-fast. * *
Note that the fail-fast behavior of an iterator cannot be guaranteed * as it is, generally speaking, impossible to make any hard guarantees in the * presence of unsynchronized concurrent modification. Fail-fast iterators * throw ConcurrentModificationException on a best-effort basis. * Therefore, it would be wrong to write a program that depended on this * exception for its correctness: the fail-fast behavior of iterators * should be used only to detect bugs.
* * This class is a member of the * * Java Collections Framework. * * @author Lee Boynton * @author Jonathan Payne * @version 1.89, 01/23/03 * @see Collection * @see List * @see ArrayList * @see LinkedList * @since JDK1.0 */ public class Vector extends AbstractList implements List, RandomAccess, Cloneable, java.io.Serializable { /** * The array buffer into which the components of the vector are * stored. The capacity of the vector is the length of this array buffer, * and is at least large enough to contain all the vector's elements.
*
* Any array elements following the last element in the Vector are null.
*
* @serial
*/
protected /*@ spec_public rep @*/ Object elementData[];
/**
* The number of valid components in this Vector object.
* Components elementData[0] through
* elementData[elementCount-1] are the actual items.
*
* @serial
*/
protected /*@ spec_public rep @*/ int elementCount;
/**
* The amount by which the capacity of the vector is automatically
* incremented when its size becomes greater than its capacity. If
* the capacity increment is less than or equal to zero, the capacity
* of the vector is doubled each time it needs to grow.
*
* @serial
*/
protected int capacityIncrement;
/** use serialVersionUID from JDK 1.0.2 for interoperability */
private static final long serialVersionUID = -2767605614048989439L;
//@ instance invariant elementData != null;
//@ instance invariant elementCount >= 0;
//@ instance invariant elementCount <= elementData.length;
/*@ instance invariant (\forall int i; i >= elementCount && i < elementData.length;
elementData[i] == null); @*/
/*@ behavior
@ requires initialCapacity >= 0;
@ assignable elementData, capacityIncrement;
@ ensures \fresh(elementData) && \independent &&
@ elementData.length == initialCapacity &&
@ this.capacityIncrement == capacityIncrement;
@also
@ exceptional_behavior
@ requires initialCapacity < 0;
@ assignable \nothing;
@ signals (IllegalArgumentException);
@*/
public /*@ atomic @*/ Vector(int initialCapacity, int capacityIncrement) {
super();
if (initialCapacity < 0)
throw new IllegalArgumentException("Illegal Capacity: "+
initialCapacity);
this.elementData = new Object[initialCapacity];
this.capacityIncrement = capacityIncrement;
}
/*@ behavior
@ requires initialCapacity >= 0;
@ ensures \fresh(elementData) && \independent &&
@ elementData.length == initialCapacity &&
@ this.capacityIncrement == 0;
@*/
public /*@ atomic @*/ Vector(int initialCapacity) {
this(initialCapacity, 0);
}
/*@ behavior
@ ensures \fresh(elementData) && \independent &&
@ elementData.length == 10 &&
@ this.capacityIncrement == 0;
@*/
public /*@ atomic @*/ Vector() {
this(10);
}
/*@ behavior
@ requires c != null && \thread_safe(c);
@ assignable elementCount, elementData;
@ ensures elementCount == c.size() && \fresh(elementData);
@also
@ exceptional_behavior
@ requires c == null && \thread_safe(c);;
@ assignable \nothing;
@ signals (NullPointerException);
@*/
public /*@ atomic @*/ Vector(Collection c) {
elementCount = c.size();
// 10% for growth
elementData = new Object[
(int)Math.min((elementCount*110L)/100,Integer.MAX_VALUE)];
c.toArray(elementData);
}
/*@ behavior
@ requires \thread_safe(anArray) && anArray != null && anArray.length >= elementData.length;
@ locks this;
@ assignable elementData[*];
@ ensures (\forall int i; i >=0 && i < elementCount; elementData[i].equals(anArray[i]));
@also
@ exceptional_behavior
@ requires \thread_safe(anArray) && anArray == null || anArray.length < elementData.length;
@ locks this;
@ assignable \nothing;
@ signals (NullPointerException) anArray == null;
@ signals (IndexOutOfBoundsException) anArray.length < elementData.length;
@*/
public synchronized void copyInto(Object anArray[]) {
System.arraycopy(elementData, 0, anArray, 0, elementCount);
}
/*@ behavior
@ assignable elementData, modCount;
@ ensures modCount == \old(modCount) + 1 && \old(elementCount < elementData.length) ==>
@ (\fresh(elementData) && elementData.length == elementCount &&
@ (\forall int i; i >= 0 && i < elementCount; elementData[i].equals(\old(elementData[i]))));
@*/
public /*@ atomic @*/ synchronized void trimToSize() {
modCount++;
int oldCapacity = elementData.length;
if (elementCount < oldCapacity) {
Object oldData[] = elementData;
elementData = new Object[elementCount];
System.arraycopy(oldData, 0, elementData, 0, elementCount);
}
}
/*@ behavior
@ assignable elementData, modCount;
@ ensures modCount == \old(modCount) + 1 && \old(minCapacity > elementData.length) ==>
@ elementData.length >= newCapacity;
@*/
public /*@ atomic @*/ synchronized void ensureCapacity(int minCapacity) {
modCount++;
ensureCapacityHelper(minCapacity);
}
/*@ private behavior
@ requires \lockset.has(this);
@ assignable elementData;
@ ensures (\old(minCapacity > elementData.length) ==>
@ (\fresh(elementData) && elementData.length >= newCapacity &&
@ (\forall int i; i >= 0 && i < elementCount; elementData[i].equals(\old(elementData[i]))))) &&
@ \independent;
@*/
private /*@ atomic @*/ void ensureCapacityHelper(int minCapacity) {
int oldCapacity = elementData.length;
if (minCapacity > oldCapacity) {
Object oldData[] = elementData;
int newCapacity = (capacityIncrement > 0) ?
(oldCapacity + capacityIncrement) : (oldCapacity * 2);
if (newCapacity < minCapacity) {
newCapacity = minCapacity;
}
elementData = new Object[newCapacity];
System.arraycopy(oldData, 0, elementData, 0, elementCount);
}
}
/*@ behavior
@ requires newSize >= 0;
@ locks this;
@ assignable modCount, elementData, elementData[*];
@ ensures newSize == elementCount;
@ ensures (newSize > elementCount || newSize < elementCount) ==>
@ (\forall int i; i >= \old(elementCount) && i < elementCount; elementData[i] == null);
@also
@ exceptional_behavior
@ requires newSize < 0;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized void setSize(int newSize) {
modCount++;
if (newSize > elementCount) {
ensureCapacityHelper(newSize);
} else {
for (int i = newSize ; i < elementCount ; i++) {
elementData[i] = null;
}
}
elementCount = newSize;
}
/*@ behavior
@ ensures \result == elementData.length;
@*/
public /*@ atomic weakly_pure @*/ synchronized int capacity() {
return elementData.length;
}
/*@ behavior
@ ensures \result == elementCount;
@*/
public /*@ atomic weakly_pure @*/ synchronized int size() {
return elementCount;
}
/*@ behavior
@ ensures \result <==> elementCount == 0;
@*/
public /*@ atomic weakly_pure @*/ synchronized boolean isEmpty() {
return elementCount == 0;
}
/**
* Returns an enumeration of the components of this vector. The
* returned Enumeration object will generate all items in
* this vector. The first item generated is the item at index 0,
* then the item at index 1, and so on.
*
* @return an enumeration of the components of this vector.
* @see Enumeration
* @see Iterator
*/
public Enumeration elements() {
return new Enumeration() {
int count = 0;
public boolean hasMoreElements() {
return count < elementCount;
}
public Object nextElement() {
synchronized (Vector.this) {
if (count < elementCount) {
return elementData[count++];
}
}
throw new NoSuchElementException("Vector Enumeration");
}
};
}
/**
* Tests if the specified object is a component in this vector.
*
* @param elem an object.
* @return true if and only if the specified object
* is the same as a component in this vector, as determined by the
* equals method; false otherwise.
*/
/*@ behavior
@ requires (\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ ensures \result;
@also
@ requires !(\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ ensures !(\result);
@*/
public /*@ atomic @*/ boolean contains(Object elem) {
return indexOf(elem, 0) >= 0;
}
/**
* Searches for the first occurence of the given argument, testing
* for equality using the equals method.
*
* @param elem an object.
* @return the index of the first occurrence of the argument in this
* vector, that is, the smallest value k such that
* elem.equals(elementData[k]) is true;
* returns -1 if the object is not found.
* @see Object#equals(Object)
*/
/*@ behavior
@ requires (\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ ensures (elementData[\result].equals(elem)) && (\forall int i; i >= 0 && i < elementCount;
@ elementData[i].equals(elem) ==> \result <= i)
@ && \result >= 0
@ && \result < elementCount;
@also
@ requires !(\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ ensures \result == -1;
@*/
public /*@ atomic @*/ int indexOf(Object elem) {
return indexOf(elem, 0);
}
/**
* Searches for the first occurence of the given argument, beginning
* the search at index, and testing for equality using
* the equals method.
*
* @param elem an object.
* @param index the non-negative index to start searching from.
* @return the index of the first occurrence of the object argument in
* this vector at position index or later in the
* vector, that is, the smallest value k such that
* elem.equals(elementData[k]) && (k >= index) is
* true; returns -1 if the object is not
* found. (Returns -1 if index >= the
* current size of this Vector.)
* @exception IndexOutOfBoundsException if index is negative.
* @see Object#equals(Object)
*/
/*@ behavior
@ requires index >= 0 && index < elementCount &&
@ (\exists int i; i >= index && i < elementCount; elementData[i].equals(elem));
@ locks this;
@ ensures ensures (elementData[\result].equals(elem)) && (\forall int i; i >= index && i < elementCount;
@ elementData[i].equals(elem) ==> \result <= i)
@ && \result >= index
@ && \result < elementCount;
@also
@ requires index >= 0 && index < elementCount &&
@ !(\exists int i; i >= index && i < elementCount; elementData[i].equals(elem));
@ ensures \result == -1;
@*/
public /*@ atomic @*/ synchronized int indexOf(Object elem, int index) {
if (elem == null) {
for (int i = index ; i < elementCount ; i++)
if (elementData[i]==null)
return i;
} else {
for (int i = index ; i < elementCount ; i++)
if (elem.equals(elementData[i]))
return i;
}
return -1;
}
/**
* Returns the index of the last occurrence of the specified object in
* this vector.
*
* @param elem the desired component.
* @return the index of the last occurrence of the specified object in
* this vector, that is, the largest value k such that
* elem.equals(elementData[k]) is true;
* returns -1 if the object is not found.
*/
/*@ behavior
@ requires (\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ locks this;
@ ensures (elementData[\result].equals(elem)) && (\forall int i; i >= 0 && i < elementCount;
@ elementData[i].equals(elem) ==> \result >= i)
@ && \result >= 0
@ && \result < elementCount;
@also
@ requires !(\exists int i; i >= 0 && i < elementCount; elementData[i].equals(elem));
@ locks this;
@ ensures \result == -1;
@*/
public /*@ atomic @*/ synchronized int lastIndexOf(Object elem) {
return lastIndexOf(elem, elementCount-1);
}
/**
* Searches backwards for the specified object, starting from the
* specified index, and returns an index to it.
*
* @param elem the desired component.
* @param index the index to start searching from.
* @return the index of the last occurrence of the specified object in this
* vector at position less than or equal to index in
* the vector, that is, the largest value k such that
* elem.equals(elementData[k]) && (k <= index) is
* true; -1 if the object is not found.
* (Returns -1 if index is negative.)
* @exception IndexOutOfBoundsException if index is greater
* than or equal to the current size of this vector.
*/
/*@ behavior
@ requires index >= 0 && index < elementCount && (\exists int i; i >= 0 && i < index; elementData[i].equals(elem));
@ locks this;
@ ensures ensures (elementData[\result].equals(elem)) && (\forall int i; i >= 0 && i < index;
@ elementData[i].equals(elem) ==> \result >= i)
@ && \result >= 0
@ && \result < index;
@also
@ requires index >= 0 && index < elementCount && !(\exists int i; i >= 0 && i < index; elementData[i].equals(elem));
@ ensures \result == -1;
@*/
public /*@ atomic @*/ synchronized int lastIndexOf(Object elem, int index) {
if (index >= elementCount)
throw new IndexOutOfBoundsException(index + " >= "+ elementCount);
if (elem == null) {
for (int i = index; i >= 0; i--)
if (elementData[i]==null)
return i;
} else {
for (int i = index; i >= 0; i--)
if (elem.equals(elementData[i]))
return i;
}
return -1;
}
/*@ behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ ensures \result.equals(elementData[index]);
@also
@ exceptional_behavior
@ requires index < 0 || index >= elementCount;
@ locks this;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized Object elementAt(int index) {
if (index >= elementCount) {
throw new ArrayIndexOutOfBoundsException(index + " >= " + elementCount);
}
return elementData[index];
}
/*@ public normal_behavior
@ requires !isEmpty();
@ locks this;
@ ensures \result.equals(elementData[0]);
@also
@ public exceptional_behavior
@ requires isEmpty();
@ locks this;
@ signals(NoSuchElementException);
@*/
public /*@ atomic @*/ synchronized Object firstElement() {
if (elementCount == 0) {
throw new NoSuchElementException();
}
return elementData[0];
}
/*@ public behavior
@ requires !isEmpty();
@ locks this;
@ ensures \result.equals(elementData[elementCount - 1]);
@also
@ public exceptional_behavior
@ requires isEmpty();
@ locks this;
@ signals(NoSuchElementException);
@*/
public /*@ atomic @*/ synchronized Object lastElement() {
if (elementCount == 0) {
throw new NoSuchElementException();
}
return elementData[elementCount - 1];
}
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ assignable elementData[index];
@ ensures elementData[index].equals(obj);
@also
@ public exceptional_behavior
@ requires index < 0 || index >= elementCount;
@ locks this.
@ assignable \nothing;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized void setElementAt(Object obj, int index) {
if (index >= elementCount) {
throw new ArrayIndexOutOfBoundsException(index + " >= " +
elementCount);
}
elementData[index] = obj;
}
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ assignable elementCount, elementData[*], modCount;
@ ensures elementCount == (\old(elementCount) - 1) && modCount == (\old(modCount) + 1) &&
@ (\forall int i; i >= index && i < elementCount;
@ elementData[i] == \old(elementData[i + 1])) &&
@ (\forall int i; i >= 0 && i < index;
@ elementData[i] == \old(elementData[i]));
@also
@ public exceptional_behavior
@ requires index < 0 && index >= elementCount;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized void removeElementAt(int index) {
modCount++;
if (index >= elementCount) {
throw new ArrayIndexOutOfBoundsException(index + " >= " +
elementCount);
}
else if (index < 0) {
throw new ArrayIndexOutOfBoundsException(index);
}
int j = elementCount - index - 1;
if (j > 0) {
System.arraycopy(elementData, index + 1, elementData, index, j);
}
elementCount--;
elementData[elementCount] = null; /* to let gc do its work */
}
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ assignable elementCount, elementData[*], elementData, modCount;
@ ensures elementData[index] == obj && modCount == \old(modCount) + 1 &&
@ elementCount == \old(elementCount) + 1 &&
@ (\forall int i; i > index && i < elementCount;
@ elementData[i] == \old(elementData[i - 1])) &&
@ (\forall int i; i >= 0 && i < index;
@ elementData[i] == \old(elementData[i]));
@also
@ public exceptional_behavior
@ requires index < 0 || index >= elementCount;
@ locks this;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized void insertElementAt(Object obj, int index) {
modCount++;
if (index > elementCount) {
throw new ArrayIndexOutOfBoundsException(index
+ " > " + elementCount);
}
ensureCapacityHelper(elementCount + 1);
System.arraycopy(elementData, index, elementData, index + 1, elementCount - index);
elementData[index] = obj;
elementCount++;
}
/*@ public behavior
@ locks this;
@ assignable modCount, elementData[*], elementData;
@ ensures elementCount == (\old(elementCount) + 1) && elementData[elementCount] == obj &&
@ modCount == (\old(modCount) + 1);
@ ensures \old(capacity() == size()) ==> capacity() > \old(capacity());
@*/
public /*@ atomic @*/ synchronized void addElement(Object obj) {
modCount++;
ensureCapacityHelper(elementCount + 1);
elementData[elementCount++] = obj;
}
/*@ public behavior
@ locks this;
@ assignable modCount, elementCount, elementData[*];
@ ensures \result <==> \old(\exists int i; i >= 0 && i < elementCount;
@ elementData[i].equals(obj));
@ ensures \old(\exists int i; i >= 0 && i < elementCount; elementData[i].equals(obj)) ==>
@ elementCount == (\old(elementCount) - 1) && modCount == (\old(modCount) + 1);
@*/
public /*@ atomic @*/ synchronized boolean removeElement(Object obj) {
modCount++;
int i = indexOf(obj);
if (i >= 0) {
removeElementAt(i);
return true;
}
return false;
}
/*@ public behavior
@ locks this;
@ assignable modCount, elementData[*], elementCount;
@ ensures modCount == (\old(modCount) + 1) && elementCount == 0;
@*/
public /*@ atomic @*/ synchronized void removeAllElements() {
modCount++;
// Let gc do its work
for (int i = 0; i < elementCount; i++)
elementData[i] = null;
elementCount = 0;
}
/**
* Returns a clone of this vector. The copy will contain a
* reference to a clone of the internal data array, not a reference
* to the original internal data array of this Vector object.
*
* @return a clone of this vector.
*/
public /*@ atomic @*/ synchronized Object clone() {
try {
Vector v = (Vector)super.clone();
v.elementData = new Object[elementCount];
System.arraycopy(elementData, 0, v.elementData, 0, elementCount);
v.modCount = 0;
return v;
} catch (CloneNotSupportedException e) {
// this shouldn't happen, since we are Cloneable
throw new InternalError();
}
}
/**
* Returns an array containing all of the elements in this Vector
* in the correct order.
*
* @since 1.2
*/
/*@ public behavior
@ ensures \fresh(\result) && (\forall int i; i >= 0 && i < elementCount; \result[i].equals(elementData[i]));
@*/
public /*@ atomic @*/ synchronized Object[] toArray() {
Object[] result = new Object[elementCount];
System.arraycopy(elementData, 0, result, 0, elementCount);
return result;
}
/**
* Returns an array containing all of the elements in this Vector in the
* correct order; the runtime type of the returned array is that of the
* specified array. If the Vector fits in the specified array, it is
* returned therein. Otherwise, a new array is allocated with the runtime
* type of the specified array and the size of this Vector.
*
* If the Vector fits in the specified array with room to spare
* (i.e., the array has more elements than the Vector),
* the element in the array immediately following the end of the
* Vector is set to null. This is useful in determining the length
* of the Vector only if the caller knows that the Vector
* does not contain any null elements.
*
* @param a the array into which the elements of the Vector are to
* be stored, if it is big enough; otherwise, a new array of the
* same runtime type is allocated for this purpose.
* @return an array containing the elements of the Vector.
* @exception ArrayStoreException the runtime type of a is not a supertype
* of the runtime type of every element in this Vector.
* @throws NullPointerException if the given array is null.
* @since 1.2
*/
public /*@ atomic @*/ synchronized Object[] toArray(Object a[]) {
if (a.length < elementCount)
a = (Object[])java.lang.reflect.Array.newInstance(
a.getClass().getComponentType(), elementCount);
System.arraycopy(elementData, 0, a, 0, elementCount);
if (a.length > elementCount)
a[elementCount] = null;
return a;
}
// Positional Access Operations
/**
* Returns the element at the specified position in this Vector.
*
* @param index index of element to return.
* @return object at the specified index
* @exception ArrayIndexOutOfBoundsException index is out of range (index
* < 0 || index >= size()).
* @since 1.2
*/
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ ensures \result == elementData[index];
@also
@ public exceptional_behavior
@ requires index < 0 || index >= elementCount;
@ locks this;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic weakly_pure @*/ synchronized Object get(int index) {
if (index >= elementCount)
throw new ArrayIndexOutOfBoundsException(index);
return elementData[index];
}
/**
* Replaces the element at the specified position in this Vector with the
* specified element.
*
* @param index index of element to replace.
* @param element element to be stored at the specified position.
* @return the element previously at the specified position.
* @exception ArrayIndexOutOfBoundsException index out of range
* (index < 0 || index >= size()).
* @since 1.2
*/
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ assignable elementData[index];
@ ensures element == elementData[index] && \result == \old(elementData[index]);
@also
@ public exceptional_behavior
@ requires index < 0 || index >= elementCount;
@ locks this;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized Object set(int index, Object element) {
if (index >= elementCount)
throw new ArrayIndexOutOfBoundsException(index);
Object oldValue = elementData[index];
elementData[index] = element;
return oldValue;
}
/**
* Appends the specified element to the end of this Vector.
*
* @param o element to be appended to this Vector.
* @return true (as per the general contract of Collection.add).
* @since 1.2
*/
/*@ behavior
@ locks this;
@ assignable modCount, elementData[*], elementData;
@ ensures elementCount == (\old(elementCount) + 1) && elementData[elementCount] == o &&
@ modCount == (\old(modCount) + 1) && \result;
@ ensures \old(capacity() == size()) ==> capacity() > \old(capacity());
@*/
public /*@ atomic @*/synchronized boolean add(Object o) {
modCount++;
ensureCapacityHelper(elementCount + 1);
elementData[elementCount++] = o;
return true;
}
/**
* Removes the first occurrence of the specified element in this Vector
* If the Vector does not contain the element, it is unchanged. More
* formally, removes the element with the lowest index i such that
* (o==null ? get(i)==null : o.equals(get(i))) (if such
* an element exists).
*
* @param o element to be removed from this Vector, if present.
* @return true if the Vector contained the specified element.
* @since 1.2
*/
/*@ public behavior
@ assignable modCount, elementCount, elementData[*];
@ ensures \result <==> \old(\exists int i; i >= 0 && i < elementCount;
@ elementData[i].equals(o));
@ ensures \old(\exists int i; i >= 0 && i < elementCount; elementData[i].equals(o)) ==>
@ elementCount == (\old(elementCount) - 1) && modCount == (\old(modCount) + 1);
@*/
public /*@ atomic @*/ boolean remove(Object o) {
return removeElement(o);
}
/**
* Inserts the specified element at the specified position in this Vector.
* Shifts the element currently at that position (if any) and any
* subsequent elements to the right (adds one to their indices).
*
* @param index index at which the specified element is to be inserted.
* @param element element to be inserted.
* @exception ArrayIndexOutOfBoundsException index is out of range
* (index < 0 || index > size()).
* @since 1.2
*/
/*@ public behavior
@ assignable elementCount, elementData[*], elementData, modCount;
@ ensures elementData[index] == element && modCount == (\old(modCount) + 1) &&
@ elementCount == (\old(elementCount) + 1) &&
@ (\forall int i; i > index && i < elementCount;
@ elementData[i] == \old(elementData[i - 1])) &&
@ (\forall int i; i >= 0 && i < index;
@ elementData[i] == \old(elementData[i]));
@*/
public /*@ atomic @*/ void add(int index, Object element) {
insertElementAt(element, index);
}
/**
* Removes the element at the specified position in this Vector.
* shifts any subsequent elements to the left (subtracts one from their
* indices). Returns the element that was removed from the Vector.
*
* @exception ArrayIndexOutOfBoundsException index out of range (index
* < 0 || index >= size()).
* @param index the index of the element to removed.
* @return element that was removed
* @since 1.2
*/
/*@ public behavior
@ requires index >= 0 && index < elementCount;
@ locks this;
@ assignable elementCount, elementData[*], modCount;
@ ensures elementCount == (\old(elementCount) - 1) && modCount == (\old(modCount) + 1) &&
@ (\forall int i; i >= index && i < elementCount;
@ elementData[i].equals(\old(elementData[i + 1]))) &&
@ (\forall int i; i >= 0 && i < index;
@ elementData[i].equals(\old(elementData[i]))) &&
@ \result == \old(elementData[index]);
@also
@ public exceptional_behavior
@ locks this;
@ requires index < 0 && index >= elementCount;
@ signals (ArrayIndexOutOfBoundsException);
@*/
public /*@ atomic @*/ synchronized Object remove(int index) {
modCount++;
if (index >= elementCount)
throw new ArrayIndexOutOfBoundsException(index);
Object oldValue = elementData[index];
int numMoved = elementCount - index - 1;
if (numMoved > 0)
System.arraycopy(elementData, index+1, elementData, index,
numMoved);
elementData[--elementCount] = null; // Let gc do its work
return oldValue;
}
/**
* Removes all of the elements from this Vector. The Vector will
* be empty after this call returns (unless it throws an exception).
*
* @since 1.2
*/
public /*@ atomic @*/ void clear() {
removeAllElements();
}
// Bulk Operations
/**
* Returns true if this Vector contains all of the elements in the
* specified Collection.
*
* @param c a collection whose elements will be tested for containment
* in this Vector
* @return true if this Vector contains all of the elements in the
* specified collection.
* @throws NullPointerException if the specified collection is null.
*/
public /*@ atomic @*/ synchronized boolean containsAll(Collection c) {
return super.containsAll(c);
}
/**
* Appends all of the elements in the specified Collection to the end of
* this Vector, in the order that they are returned by the specified
* Collection's Iterator. The behavior of this operation is undefined if
* the specified Collection is modified while the operation is in progress.
* (This implies that the behavior of this call is undefined if the
* specified Collection is this Vector, and this Vector is nonempty.)
*
* @param c elements to be inserted into this Vector.
* @return true if this Vector changed as a result of the call.
* @throws NullPointerException if the specified collection is null.
* @since 1.2
*/
/*@ public normal_behavior
@ requires \thread_safe(c) && c != null;
@ locks this;
@ ensures \result <==> c.size() > 0;
@ ensures (\forall Object o; c.contains(o);
@ (\exits int i; i >= \old(elementData.length) && i < \old(elementData.length) + c.size();
@ o == elementData[i] || (o != null && o.equals(elementData[i])))) &&
@ elementData.length == \old(elementData.length) + c.size() &&
@ (\forall int i; i >= 0 && i < \old(elementData.length); elementData[i] == \old(elementData[i]));
@*/
public /*@ atomic @*/ synchronized boolean addAll(Collection c) {
modCount++;
Object[] a = c.toArray();
int numNew = a.length;
ensureCapacityHelper(elementCount + numNew);
System.arraycopy(a, 0, elementData, elementCount, numNew);
elementCount += numNew;
return numNew != 0;
}
/**
* Removes from this Vector all of its elements that are contained in the
* specified Collection.
*
* @param c a collection of elements to be removed from the Vector
* @return true if this Vector changed as a result of the call.
* @throws NullPointerException if the specified collection is null.
* @since 1.2
*/
/*@ public normal_behavior
@ requires \thread_safe(c) && c != null;
@ locks this;
@ ensures \result <==> !(\not_modified(elementData));
@ ensures (\forall Object o; c.contains(o);
@ !(\exists int i; i >= 0 && i < elementData.length;
@ o == elementData[i] || (o != null && o.equals(elementData[i]))));
@*/
public /*@ atomic @*/ synchronized boolean removeAll(Collection c) {
return super.removeAll(c);
}
/**
* Retains only the elements in this Vector that are contained in the
* specified Collection. In other words, removes from this Vector all
* of its elements that are not contained in the specified Collection.
*
* @param c a collection of elements to be retained in this Vector
* (all other elements are removed)
* @return true if this Vector changed as a result of the call.
* @throws NullPointerException if the specified collection is null.
* @since 1.2
*/
/*@ public normal_behavior
@ requires \thread_safe(c) && c != null;
@ locks this;
@ ensures \result <==> !(\not_modified(elementData));
@ ensures (\forall int i; i >= 0 && i < elementData.length;
@ c.contains(elementData[i]));
@*/
public /*@ atomic @*/ synchronized boolean retainAll(Collection c) {
return super.retainAll(c);
}
/**
* Inserts all of the elements in in the specified Collection into this
* Vector at the specified position. Shifts the element currently at
* that position (if any) and any subsequent elements to the right
* (increases their indices). The new elements will appear in the Vector
* in the order that they are returned by the specified Collection's
* iterator.
*
* @param index index at which to insert first element
* from the specified collection.
* @param c elements to be inserted into this Vector.
* @return true if this Vector changed as a result of the call.
* @exception ArrayIndexOutOfBoundsException index out of range (index
* < 0 || index > size()).
* @throws NullPointerException if the specified collection is null.
* @since 1.2
*/
/*@ public normal_behavior
@ requires \thread_safe(c) && c != null && i >= 0 && i < elementData.length;
@ locks this;
@ ensures \result <==> c.size() > 0;
@ ensures (\forall Object o; c.contains(o);
@ (\exits int i; i >= index && i < index + c.size();
@ o == elementData[i] || (o != null && o.equals(elementData[i])))) &&
@ elementData.length == \old(elementData.length) + c.size() &&
@ (\forall int i; i >= 0 && i < index; elementData[i] == \old(elementData[i])) &&
@ (\forall int i; i >= index + c.size() && i < elementData.length;
@ elementData[i] == \old(elementData[i - c.size()]));
@also
@ public exceptional_behavior
@ requires i < 0 || i >= elementData.length;
@ signals (Exception ioobe) ioobe instanceof IndexOutOfBoundsException;
@*/
public /*@ atomic @*/ synchronized boolean addAll(int index, Collection c) {
modCount++;
if (index < 0 || index > elementCount)
throw new ArrayIndexOutOfBoundsException(index);
Object[] a = c.toArray();
int numNew = a.length;
ensureCapacityHelper(elementCount + numNew);
int numMoved = elementCount - index;
if (numMoved > 0)
System.arraycopy(elementData, index, elementData, index + numNew,
numMoved);
System.arraycopy(a, 0, elementData, index, numNew);
elementCount += numNew;
return numNew != 0;
}
/**
* Compares the specified Object with this Vector for equality. Returns
* true if and only if the specified Object is also a List, both Lists
* have the same size, and all corresponding pairs of elements in the two
* Lists are equal. (Two elements e1 and
* e2 are equal if (e1==null ? e2==null :
* e1.equals(e2)).) In other words, two Lists are defined to be
* equal if they contain the same elements in the same order.
*
* @param o the Object to be compared for equality with this Vector.
* @return true if the specified Object is equal to this Vector
*/
/*@ public normal_behavior
@ requires \thread_safe(o);
@ ensures \result <==> (o instanceof List &&
@ ((List)o).size() == elementData.length &&
@ (\forall Object ob; ((List)o).contains(ob);
@ (\exists int i; i >= 0 && i < elementData.length;
@ o == elementData[i] || (o != null && o.equals(elementData[i])))));
@*/
public /*@ atomic @*/ synchronized boolean equals(Object o) {
return super.equals(o);
}
/**
* Returns the hash code value for this Vector.
*/
public /*@ atomic @*/ synchronized int hashCode() {
return super.hashCode();
}
/**
* Returns a string representation of this Vector, containing
* the String representation of each element.
*/
public /*@ atomic @*/ synchronized String toString() {
return super.toString();
}
/**
* Returns a view of the portion of this List between fromIndex,
* inclusive, and toIndex, exclusive. (If fromIndex and ToIndex are
* equal, the returned List is empty.) The returned List is backed by this
* List, so changes in the returned List are reflected in this List, and
* vice-versa. The returned List supports all of the optional List
* operations supported by this List.
* * This method eliminates the need for explicit range operations (of * the sort that commonly exist for arrays). Any operation that expects * a List can be used as a range operation by operating on a subList view * instead of a whole List. For example, the following idiom * removes a range of elements from a List: *
* list.subList(from, to).clear(); ** Similar idioms may be constructed for indexOf and lastIndexOf, * and all of the algorithms in the Collections class can be applied to * a subList.
*
* The semantics of the List returned by this method become undefined if
* the backing list (i.e., this List) is structurally modified in
* any way other than via the returned List. (Structural modifications are
* those that change the size of the List, or otherwise perturb it in such
* a fashion that iterations in progress may yield incorrect results.)
*
* @param fromIndex low endpoint (inclusive) of the subList.
* @param toIndex high endpoint (exclusive) of the subList.
* @return a view of the specified range within this List.
* @throws IndexOutOfBoundsException endpoint index value out of range
* (fromIndex < 0 || toIndex > size)
* @throws IllegalArgumentException endpoint indices out of order
* (fromIndex > toIndex)
*/
public synchronized List subList(int fromIndex, int toIndex) {
return Collections.synchronizedList(super.subList(fromIndex, toIndex),
this);
}
/**
* Removes from this List all of the elements whose index is between
* fromIndex, inclusive and toIndex, exclusive. Shifts any succeeding
* elements to the left (reduces their index).
* This call shortens the ArrayList by (toIndex - fromIndex) elements. (If
* toIndex==fromIndex, this operation has no effect.)
*
* @param fromIndex index of first element to be removed.
* @param toIndex index after last element to be removed.
*/
/*@ normal_behavior
@ requires fromIndex >= 0 && fromIndex <= toIndex &&
@ toIndex <= elementData.length && fromIndex < elementData.length;
@ locks this;
@ ensures elementData.length == \old(elementData.length) - (toIndex - fromIndex) &&
@ (\forall int i; i >= 0 && i < fromIndex; elementData[i] == \old(elementData[i])) &&
@ (\forall int i; i >= toIndex && i < elementData.length;
@ elementData[i] == \old(elementData[i + (toIndex - fromIndex)]));
@also
@ private exceptional_behavior
@ requires fromIndex < 0 || fromIndex > toIndex ||
@ toIndex >= array.length && fromIndex >= array.length;
@ signals (Exception ioobe) ioobe instanceof IndexOutOfBoundsException;
@*/
protected void removeRange(int fromIndex, int toIndex) {
modCount++;
int numMoved = elementCount - toIndex;
System.arraycopy(elementData, toIndex, elementData, fromIndex,
numMoved);
// Let gc do its work
int newElementCount = elementCount - (toIndex-fromIndex);
while (elementCount != newElementCount)
elementData[--elementCount] = null;
}
/**
* Save the state of the Vector instance to a stream (that
* is, serialize it). This method is present merely for synchronization.
* It just calls the default readObject method.
*/
private synchronized void writeObject(java.io.ObjectOutputStream s)
throws java.io.IOException
{
s.defaultWriteObject();
}
}