001: package java.util;
002:
003: import java.io.IOException;
004: import java.io.ObjectInputStream;
005: import java.io.ObjectOutputStream;
006: import java.io.Serializable;
007: import java.lang.reflect.Array;
008:
009: public class ArrayList extends AbstractList implements List,
010: RandomAccess, Cloneable, Serializable {
011:
012: /*@ public model int capacity;
013: @*/
014:
015: /*@ public normal_behavior
016: @ requires 0 <= initialCapacity;
017: @ assignable capacity, theCollection;
018: @ ensures capacity == initialCapacity;
019: @ ensures this.isEmpty();
020: @ also
021: @ public exceptional_behavior
022: @ requires initialCapacity < 0;
023: @ assignable \nothing;
024: @ signals (IllegalArgumentException) initialCapacity < 0;
025: @*/
026: public ArrayList(int initialCapacity) {
027: }
028:
029: /*@ public normal_behavior
030: @ assignable capacity, theCollection;
031: @ ensures capacity == 10;
032: @ ensures this.isEmpty();
033: @*/
034: public ArrayList() {
035: }
036:
037: /*@ public normal_behavior
038: @ requires c != null;
039: @ requires c.size()*2 <= Integer.MAX_VALUE;
040: @ assignable capacity, theCollection;
041: @ ensures this.size() == c.size();
042: @ ensures (\forall int i; 0 <= i && i < c.size();
043: @ this.get(i).equals(c.iterator().nthNextElement(i)));
044: @ ensures_redundantly c.theCollection.equals(this.theCollection);
045: @ ensures capacity == c.size();
046: @ also
047: @ public exceptional_behavior
048: @ requires c == null;
049: @ assignable \nothing;
050: @ signals (NullPointerException) c == null;
051: @*/
052: public ArrayList(Collection c) {
053: }
054:
055: /*@ public normal_behavior
056: @ assignable capacity, theCollection;
057: @ ensures capacity == this.size();
058: @*/
059: public void trimToSize() {
060: }
061:
062: public void ensureCapacity(int minCapacity) {
063: }
064:
065: public int size() {
066: }
067:
068: public boolean isEmpty() {
069: }
070:
071: public boolean contains(Object e) {
072: }
073:
074: public int indexOf(Object e) {
075: }
076:
077: public int lastIndexOf(Object e) {
078: }
079:
080: /*@ also
081: @ implies_that
082: @ public normal_behavior
083: @ assignable \nothing;
084: @ ensures \result != this;
085: @ ensures \result.getClass() == this.getClass();
086: @ ensures \result.equals(this);
087: @ ensures \result != null;
088: @ ensures ((ArrayList)\result).size() == this.size();
089: @ ensures (\forall int i; 0 <= i && i < this.size();
090: @ ((ArrayList)\result).get(i) == this.get(i));
091: @*/
092: public Object clone() {
093: }
094:
095: public Object[] toArray() {
096: }
097:
098: /*@ also
099: @ public exceptional_behavior
100: @ requires elementType <: \elemtype(\typeof(a));
101: @ assignable \nothing;
102: @ signals (ArrayStoreException);
103: @*/
104: public Object[] toArray(Object[] a) {
105: }
106:
107: public Object get(int index) {
108: }
109:
110: /*@ also
111: @ public exceptional_behavior
112: @ requires index < 0 || index >= this.size();
113: @ assignable \nothing;
114: @ signals (IndexOutOfBoundsException);
115: @*/
116: public Object set(int index, Object e) {
117: }
118:
119: public boolean add(Object e) {
120: }
121:
122: /*@ also
123: @ public exceptional_behavior
124: @ requires index < 0 || index >= this.size();
125: @ assignable \nothing;
126: @ signals (IndexOutOfBoundsException);
127: @*/
128: public void add(int index, Object e) {
129: }
130:
131: /*@ also
132: @ public exceptional_behavior
133: @ requires index < 0 || index >= this.size();
134: @ assignable \nothing;
135: @ signals (IndexOutOfBoundsException);
136: @*/
137: public Object remove(int index) {
138: }
139:
140: public void clear() {
141: }
142:
143: public boolean addAll(Collection c) {
144: }
145:
146: /*@ also
147: @ public exceptional_behavior
148: @ requires index < 0 || index >= this.size() || c == null;
149: @ assignable \nothing;
150: @ signals (IndexOutOfBoundsException) index < 0 || index >= this.size();
151: @ signals (NullPointerException) c == null;
152: @*/
153: public boolean addAll(int index, Collection c) {
154: }
155:
156: protected void removeRange(int fromIndex, int toIndex) {
157: }
158:
159: private void checkBoundInclusive(int index) {
160: }
161:
162: private void checkBoundExclusive(int index) {
163: }
164:
165: boolean removeAllInternal(Collection c) {
166: }
167:
168: boolean retainAllInternal(Collection c) {
169: }
170:
171: private void writeObject(ObjectOutputStream s) throws IOException {
172: }
173:
174: private void readObject(ObjectInputStream s) throws IOException,
175: ClassNotFoundException {
176: }
177: }
|