01: package java.util;
02:
03: public interface Enumeration {
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 normal_behavior
12: @ assignable objectState;
13: @ ensures \result <==> moreElements;
14: @*/
15: boolean hasMoreElements();
16:
17: /*@ public normal_behavior
18: @ requires moreElements;
19: @ assignable objectState;
20: @ assignable moreElements;
21: @ ensures (\result == null) || \typeof(\result) <: elementType;
22: @ ensures !returnsNull ==> (\result != null);
23: @ also
24: @ public exceptional_behavior
25: @ requires !moreElements;
26: @ assignable \nothing;
27: @ signals (NoSuchElementException);
28: @*/
29: Object nextElement();
30: }
|