001: package java.util;
002:
003: public interface Collection {
004:
005: //@ public model instance non_null JMLEqualsBag theCollection;
006:
007: //@ instance ghost public \TYPE elementType;
008:
009: //@ public instance invariant elementType == theCollection.elementType;
010: //@ instance ghost public boolean containsNull;
011: //@ public instance invariant containsNull == theCollection.containsNull;
012:
013: //@ public instance ghost Object[] list;
014: //@ public instance ghost int end;
015: //@ public invariant (\forall int i; list.length > i) && end >= 0;
016:
017: /*@
018: @ public normal_behavior
019: @ assignable end, list[end];
020: @ ensures \old(end)+1 == end;
021: @ ensures list[end-1] == o;
022: @*/
023: boolean add(Object o);
024:
025: boolean addAll(Collection c);
026:
027: /*@ public behavior
028: @ assignable theCollection;
029: @ ensures theCollection.isEmpty();
030: @ ensures_redundantly size() == 0;
031: @ signals (UnsupportedOperationException);
032: @ also
033: @ public normal_behavior
034: @ assignable end;
035: @ ensures end == 0;
036: @*/
037: void clear();
038:
039: /*@ public normal_behavior
040: @ ensures \result <==> (\exists int i; i>=0 && i<end;
041: @ o==null ? list[i]==null : o.equals(list[i]));
042: @*/
043: boolean contains(Object o);
044:
045: /*@ public normal_behavior
046: @ ensures \result <==> (\forall int j; j>=0 && j<c.end;
047: @ (\exists int i; i>=0 && i<end;
048: @ c.list[j]==null ?
049: @ list[i]==null : c.list[j].equals(list[i])));
050: @*/
051: boolean containsAll(Collection c);
052:
053: boolean equals(Object o);
054:
055: int hashCode();
056:
057: /*@ public normal_behavior
058: @ ensures \result <==> (end == 0);
059: @*/
060: boolean isEmpty();
061:
062: /*@ public normal_behavior
063: @ assignable \nothing;
064: @ ensures \result != null;
065: @ ensures \result.elementType == elementType;
066: @ ensures containsNull == \result.returnsNull;
067: @ ensures (\forall int i; 0 <= i && i < size();
068: @ theCollection.has(\result.nthNextElement(i)));
069: @ ensures (\forall Object o; theCollection.has(o) ==>
070: @ (\exists int i; 0 <= i && i < size();
071: @ o == \result.nthNextElement(i)));
072: @ ensures size() > 0 ==> \result.hasNext((int)(size()-1));
073: @ ensures !\result.hasNext((int)(size()));
074: @ ensures_redundantly
075: @ (\forall int i; 0 <= i && i < size();
076: @ this.contains(\result.nthNextElement(i)));
077: @ ensures_redundantly size() != 0 ==> \result.moreElements;
078: @*/
079: Iterator iterator();
080:
081: /*@ public behavior
082: @ requires !containsNull ==> o != null;
083: @ requires (o == null) || \typeof(o) <: elementType;
084: @ assignable theCollection;
085: @ ensures \result
086: @ ==> theCollection.equals(\old(theCollection.remove(o)));
087: @ ensures \result && \old(size() <= Integer.MAX_VALUE)
088: @ ==> size() == \old(size()-1) && size() < Integer.MAX_VALUE
089: @ && size() >= 0;
090: @ ensures !\result || \old(size() == Integer.MAX_VALUE)
091: @ ==> size() == \old(size());
092: @ signals (UnsupportedOperationException);
093: @ signals (ClassCastException);
094: @*/
095: boolean remove(Object o);
096:
097: boolean removeAll(Collection c);
098:
099: boolean retainAll(Collection c);
100:
101: /*@ public normal_behavior
102: @ assignable \nothing;
103: @ ensures \result == theCollection.int_size();
104: @
105: @ also normal_behavior
106: @ ensures \result >= 0;
107: @ also normal_behavior
108: @ ensures \result == end;
109: @*/
110: int size();
111:
112: /*@ public normal_behavior
113: @ ensures \result.length == end && (\forall int i; i>=0 && i<end;
114: @ list[i] == \result[i]);
115: @*/
116: Object[] toArray();
117:
118: Object[] toArray(Object[] a);
119: }
|