001: package java.util;
002:
003: public interface Map {
004:
005: //@ public model instance non_null JMLEqualsSet theMap;
006: //@ instance ghost public boolean containsNull;
007: //@ public instance ghost Object[][] concrete_map;
008:
009: /*@ public instance invariant
010: @ (\forall int i; i>=0 && i<concrete_map.length;
011: @ concrete_map[i].length == 2) &&
012: @ \nonnullelements(concrete_map) &&
013: @ (\forall int i,j; concrete_map[j][0]==concrete_map[i][0]; i==j);
014: @*/
015:
016: /*@ public instance invariant
017: @ (\forall Object o; theMap.has(o); o instanceof java.util.Map.Entry);
018: @*/
019:
020: /*@ public instance invariant
021: @ (\forall Object o1, o2; theMap.has(o1) && theMap.has(o2);
022: @ o2!=o1 ==> !JMLNullSafe.equals(o2,o1));
023: @*/
024:
025: /*@ public normal_behavior
026: @ assignable theMap;
027: @ ensures theMap.isEmpty();
028: @*/
029: void clear();
030:
031: /*@ public normal_behavior
032: @ requires key != null;
033: @ ensures \result <==>
034: @ (\exists java.util.Map.Entry e; theMap.has(e) && e != null;
035: @ JMLNullSafe.equals(e.abstractKey, key));
036: @ also
037: @ public normal_behavior
038: @ requires key != null;
039: @ ensures \result <==> (\exists int i; i>=0 && i<size();
040: @ concrete_map[i][0].equals(key));
041: @*/
042: /*@ pure @*/
043: boolean containsKey(Object key);
044:
045: /*@ public behavior
046: @ ensures \result <==>
047: @ (\exists java.util.Map.Entry e; theMap.has(e) && e != null;
048: @ JMLNullSafe.equals(e.abstractValue, value));
049: @ signals (ClassCastException)
050: @ (* if the value is not appropriate for this object *);
051: @ signals (NullPointerException) value == null
052: @ && (* this type doesn't permit null values *);
053: @*/
054: boolean /*@ pure @*/containsValue(Object value);
055:
056: /*@ public normal_behavior
057: @ ensures \result != null && \result.theSet.equals(theMap);
058: @*/
059: /*@ pure @*/
060: Set entrySet();
061:
062: boolean /*@ pure @*/equals(Object o);
063:
064: /*@ public normal_behavior
065: @ requires !containsKey(key);
066: @ ensures \result == null;
067: @ also
068: @ public normal_behavior
069: @ requires containsKey(key);
070: @ ensures (\exists java.util.Map.Entry e; theMap.has(e); e != null
071: @ && JMLNullSafe.equals(e.abstractKey, key)
072: @ && \result.equals(e.abstractValue));
073: @ also
074: @ public normal_behavior
075: @ requires (\exists int i; i>=0 && i<concrete_map.length;
076: @ concrete_map[i][0]==key);
077: @ ensures (\exists int i; i>=0 && i<concrete_map.length;
078: @ concrete_map[i][0]==key && \result == concrete_map[i][1]);
079: @*/
080: Object /*@ pure @*/get(Object key);
081:
082: /*@ public behavior
083: @ assignable theMap;
084: @ ensures (\exists java.util.Map.Entry e; theMap.has(e); e != null
085: @ && JMLNullSafe.equals(e.abstractKey, key)
086: @ && JMLNullSafe.equals(e.abstractValue, value)
087: @ && \result.equals(\old(e.abstractValue)));
088: @ signals (NullPointerException) \not_modified(value)
089: @ && (key==null)||(value==null) && !containsNull;
090: @ signals (UnsupportedOperationException) \not_modified(theMap)
091: @ && (* if the map's put operation is not supported *);
092: @ signals (ClassCastException) \not_modified(theMap)
093: @ && (* \typeof(key) or \typeof(value) is incompatible
094: @ with the valueType or keyType of this map *);
095: @ signals (IllegalArgumentException) \not_modified(theMap)
096: @ && (* if some aspect of key or value is not
097: @ allowed in the map *);
098: @*/
099: Object put(Object key, Object value);
100:
101: int /*@ pure @*/hashCode();
102:
103: /*@ public normal_behavior
104: @ ensures \result <==> theMap.isEmpty();
105: @*/
106: boolean isEmpty();
107:
108: /*@ public normal_behavior
109: @ ensures \result != null
110: @ && (\forall Object k; containsKey(k); \result.contains(k))
111: @ && (\forall Object k; \result.contains(k); containsKey(k));
112: @*/
113: Set /*@ pure @*/keySet();
114:
115: /*@ public behavior
116: @ assignable theMap;
117: @ ensures (\forall java.util.Map.Entry e; t.theMap.has(e);
118: @ theMap.has(e));
119: @ signals (NullPointerException) \not_modified(theMap)
120: @ && (t == null) && !containsNull;
121: @ signals (UnsupportedOperationException) \not_modified(theMap)
122: @ && (* if the map's put operation is not supported *);
123: @ signals (ClassCastException) \not_modified(theMap)
124: @ && (* \typeof(t) or is incompatible
125: @ with this map *);
126: @ signals (IllegalArgumentException) \not_modified(theMap)
127: @ && (* if some aspect of a key or value is not
128: @ allowed in the map *);
129: @*/
130: void putAll(Map t);
131:
132: /*@ public behavior
133: @ assignable theMap;
134: @ ensures \result != null
135: @ ==> (\exists java.util.Map.Entry e; e != null && \old(theMap.has(e));
136: @ JMLNullSafe.equals(e.abstractKey, key)
137: @ && \result.equals(e.abstractValue));
138: @ ensures !(\exists java.util.Map.Entry e; e != null && \old(theMap.has(e));
139: @ JMLNullSafe.equals(e.abstractKey, key));
140: @ signals (UnsupportedOperationException)
141: @ (* if this operation is not supported *);
142: @ signals (ClassCastException)
143: @ (* if the argument is not appropriate *);
144: @ signals (NullPointerException) key == null
145: @ && (* if this map doesn't support null keys *);
146: @*/
147: Object remove(Object key);
148:
149: int size();
150:
151: /*@ public normal_behavior
152: @ ensures \result != null
153: @ && (\forall Object v; containsValue(v); \result.contains(v))
154: @ && (\forall Object v; \result.contains(v); containsValue(v));
155: @*/
156: /*@ pure @*/
157: Collection values();
158:
159: /*@ also
160: @ public normal_behavior
161: @ requires o instanceof Map;
162: @ ensures \result <==> theMap.equals(o);
163: @ also
164: @ public normal_behavior
165: @ requires !(o instanceof Map);
166: @ ensures \result == false;
167: @*/
168: /*@ pure @*/boolean equals(Object o);
169:
170: interface Entry {
171: //@ public model instance Object abstractKey;
172: //@ public model instance Object abstractValue;
173: //@ ghost public boolean containsNull;
174:
175: /*@ public normal_behavior
176: @ ensures \result.equals(abstractKey);
177: @*/
178: Object getKey();
179:
180: /*@ public normal_behavior
181: @ ensures \result.equals(abstractValue);
182: @*/
183: Object getValue();
184:
185: /*@ public behavior
186: @ assignable this.abstractValue;
187: @ ensures JMLNullSafe.equals(\result, \old(this.abstractValue))
188: @ && JMLNullSafe.equals(value, this.abstractValue);
189: @ signals (NullPointerException) \not_modified(this.abstractValue)
190: @ && (abstractValue == null) && !containsNull;
191: @ signals (UnsupportedOperationException)
192: @ \not_modified(this.abstractValue)
193: @ && (* if the map's put operation is not supported *);
194: @ signals (ClassCastException) \not_modified(this.abstractValue)
195: @ && (* \typeof(abstractValue) is incompatible
196: @ with the valueType of this map *);
197: @ signals (IllegalArgumentException) \not_modified(this.abstractValue)
198: @ && (* if some aspect of value is not
199: @ allowed in the map *);
200: @*/
201: Object setValue(Object value);
202:
203: /*@ pure @*/
204: int hashCode();
205:
206: /*@ also
207: @ public normal_behavior
208: @ requires o instanceof Entry;
209: @ ensures \result ==
210: @ ( JMLNullSafe.equals(((Entry)o).abstractKey, abstractKey)
211: @ && JMLNullSafe.equals(((Entry)o).abstractValue,
212: @ abstractValue) );
213: @ also
214: @ public normal_behavior
215: @ requires !(o instanceof Entry);
216: @ ensures \result == false;
217: @*/
218: boolean equals(Object o);
219: }
220: }
|