01: package java.util;
02:
03: public interface Iterator {
04:
05: /*@ public model instance boolean moreElements;
06: @ in objectState;
07: @*/
08:
09: //@ instance ghost public \TYPE elementType;
10: //@ instance ghost public boolean returnsNull;
11: //@ public instance ghost boolean remove_called_since;
12: /*@ public normal_behavior
13: @ requires n >= 0;
14: public pure model boolean hasNext(int n);
15: @*/
16:
17: /*@ public normal_behavior
18: @ requires n >= 0 && hasNext(n);
19: @ ensures (* \result is the nth, counting from 0,
20: @ next element that would be returned by this iterator *);
21: @ ensures !returnsNull ==> \result != null;
22: @ ensures \result == null || \typeof(\result) <: elementType;
23: @ for_example
24: @ public normal_example
25: @ requires n == 0 && moreElements;
26: @ ensures (* \result == the object that would be
27: @ returned by calling next() *);
28: public pure model Object nthNextElement(int n);
29: @*/
30:
31: /*@ public normal_behavior
32: @ assignable objectState;
33: @ ensures \result <==> moreElements;
34: @*/
35: boolean hasNext();
36:
37: /*@ public normal_behavior
38: @ requires moreElements;
39: @ requires_redundantly hasNext(0);
40: @ assignable objectState, remove_called_since, moreElements;
41: @ ensures !remove_called_since;
42: @ ensures (\result == null) || \typeof(\result) <: elementType;
43: @ ensures !returnsNull ==> (\result != null);
44: @ also
45: @ public exceptional_behavior
46: @ requires !moreElements;
47: @ assignable \nothing;
48: @ signals (NoSuchElementException);
49: @*/
50: Object next();
51:
52: /*@ public behavior
53: @ assignable objectState, remove_called_since;
54: @ ensures !\old(remove_called_since) && remove_called_since;
55: @ signals (UnsupportedOperationException);
56: @ signals (IllegalStateException) \old(remove_called_since);
57: @*/
58: void remove();
59: }
|