001: package java.util;
002:
003: public interface List extends Collection {
004:
005: /*@ public model instance non_null JMLEqualsSequence theList;
006: @ in theCollection;
007: @ public instance represents theCollection <- theList.toBag();
008: @*/
009:
010: /*@
011: @ public normal_behavior
012: @ requires index <= end;
013: @ assignable end, list[end];
014: @ ensures \old(end)+1 == end;
015: @ ensures list[index] == o;
016: @ ensures (\forall int i; i>=index && i<end-1; \old(list[i]) == list[i+1]);
017: @*/
018: void add(int index, Object o);
019:
020: /*@ also
021: @ public behavior
022: @ assignable theCollection;
023: @ ensures \result ==> theList.equals(\old(theList).insertBack(o));
024: @*/
025: boolean add(Object o);
026:
027: /*@ public behavior
028: @ requires c != null;
029: @ requires 0 <= index && index <= size();
030: @ requires c.elementType <: elementType;
031: @ requires !containsNull ==> !c.containsNull;
032: @ assignable theCollection;
033: @ ensures \result
034: @ ==> theList.equals(
035: @ \old(theList.subsequence(0,index))
036: @ .concat(JMLEqualsSequence.convertFrom(c))
037: @ .concat(\old(theList.subsequence(index,size()))));
038: @ signals (UnsupportedOperationException);
039: @ signals (IllegalArgumentException);
040: @ also
041: @ public exceptional_behavior
042: @ requires c == null || !(0 <= index && index <= size())
043: @ || !(c.elementType <: elementType)
044: @ || (!containsNull && c.containsNull);
045: @ assignable \nothing;
046: @ signals (ClassCastException)
047: @ c != null && !(c.elementType <: elementType);
048: @ signals (NullPointerException) c == null;
049: @ signals (IndexOutOfBoundsException)
050: @ !(0 <= index && index <= size());
051: @*/
052: boolean addAll(int index, Collection c);
053:
054: boolean addAll(Collection c);
055:
056: void clear();
057:
058: boolean contains(Object o);
059:
060: //@ pure
061: boolean containsAll(Collection c);
062:
063: boolean equals(Object o);
064:
065: /*@ public normal_behavior
066: @ requires 0 <= index && index < size();
067: @ assignable \nothing;
068: @ ensures \result == theList.get(index);
069: @ also
070: @ public normal_behavior
071: @ requires 0 <= index && index < size();
072: @ assignable \nothing;
073: @ ensures \result == list[index];
074: @ also
075: @ public exceptional_behavior
076: @ requires !(0 <= index && index < size());
077: @ assignable \nothing;
078: @ signals (IndexOutOfBoundsException);
079: @*/
080: //@ pure
081: Object get(int index);
082:
083: int hashCode();
084:
085: /*@ public normal_behavior
086: @ requires (\exists int i; 0<=i && i<end;
087: @ o == null ? list[i] == o : o.equals(list[i]));
088: @ ensures o == null ? list[\result] == o : o.equals(list[\result]);
089: @ ensures (\forall int j; 0<=j && j<end; o == null ?
090: @ list[j] == o ==> j>=\result :
091: @ o.equals(list[j]) ==> j>=\result);
092: @ also public normal_behavior
093: @ requires (\forall int i; 0<=i && i<end;
094: @ o == null ? list[i] != o : !o.equals(list[i]));
095: @ ensures \result == -1;
096: @*/
097: int /*@ pure @*/indexOf(Object o);
098:
099: boolean /*@ pure @*/isEmpty();
100:
101: /*@ also
102: @ public behavior
103: @ assignable \nothing;
104: @ ensures \result != null;
105: @ ensures size() < Integer.MAX_VALUE
106: @ ==> (\forall int i; 0 <= i && i < size();
107: @ \result.hasNext(i) && \result.nthNextElement(i)
108: @ == toArray()[i]);
109: @*/
110: Iterator iterator();
111:
112: int lastIndexOf(Object o);
113:
114: ListIterator listIterator();
115:
116: ListIterator listIterator(int index);
117:
118: Object remove(int index);
119:
120: /*@ also
121: @ public behavior
122: @ assignable theCollection;
123: @ ensures \result
124: @ ==> theList
125: @ .equals(\old(theList.removeItemAt(theList.indexOf(o))));
126: @*/
127: boolean remove(Object o);
128:
129: boolean removeAll(Collection c);
130:
131: boolean retainAll(Collection c);
132:
133: /*@
134: @ public behavior
135: @ requires !containsNull ==> element != null;
136: @ requires (element == null) || \typeof(element) <: elementType;
137: @ {|
138: @ requires 0 <= index && index < size();
139: @ assignable theCollection;
140: @ ensures \result == (\old(theList.get(index)));
141: @ ensures theList.equals(
142: @ \old(theList.subsequence(0,index))
143: @ .insertBack(element)
144: @ .concat(\old(theList.subsequence(index+1,size()))));
145: @ signals (UnsupportedOperationException);
146: @ signals (ClassCastException);
147: @ signals (NullPointerException);
148: @ signals (IllegalArgumentException);
149: @ also
150: @ requires !(0 <= index && index < size());
151: @ assignable \nothing;
152: @ ensures false;
153: @ signals (IndexOutOfBoundsException);
154: @ |}
155: @*/
156: Object set(int index, Object element);
157:
158: int /*@ pure @*/size();
159:
160: List subList(int fromIndex, int toIndex);
161:
162: /*@ also
163: @ public normal_behavior
164: @ requires size() < Integer.MAX_VALUE;
165: @ assignable \nothing;
166: @ ensures \result != null;
167: @ ensures \result.length == size();
168: @ ensures (\forall int i; 0 <= i && i < size();
169: @ \result[i].equals(theList.get(i)));
170: @*/
171: //@ pure
172: Object[] toArray();
173:
174: /*@ also
175: @ public normal_behavior
176: @ old int colSize = theCollection.int_size();
177: @ old int arrSize = a.length;
178: @ requires a!= null && colSize < Integer.MAX_VALUE;
179: @ requires elementType <: \elemtype(\typeof(a));
180: @ requires (\forall Object o; contains(o); \typeof(o) <: \elemtype(\typeof(a)));
181: @ {|
182: @ requires colSize <= arrSize;
183: @ assignable a[*];
184: @ ensures \result == a;
185: @ ensures (\forall int k; 0 <= k && k < colSize;
186: @ theList.get(k) == \result[k]);
187: @ ensures (\forall int i; colSize <= i && i < arrSize;
188: @ \result[i] == null);
189: @ also
190: @ requires colSize > arrSize;
191: @ assignable \nothing;
192: @ ensures \fresh(\result) && \result.length == colSize;
193: @ ensures (\forall int k; 0 <= k && k < colSize;
194: @ theList.get(k) == \result[k]);
195: @ |}
196: @*/
197: Object[] toArray(Object[] a);
198: }
|