Iterator specification

parent 4b4ded4b
......@@ -53,11 +53,12 @@ public interface Collection extends java.lang.Iterable
@ ensures \result.index == 0;
@ ensures \result.seq == seq;
@ ensures \fresh(\result) && \fresh(\result.*);
@ ensures \typeof(\result) == \type(java.util.CollectionIterator);
@ assignable \nothing;
@ determines \result.seq \by seq;
@ determines \result.index \by \nothing;
@*/
public java.util.CollectionIterator iterator();
public java.util.Iterator iterator();
public java.lang.Object[] toArray();
public java.lang.Object[] toArray(java.lang.Object[] arg0);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment