Interface Iterator

All Known Subinterfaces:
JMLIterator, ListIterator, ResettableIterator
All Known Implementing Classes:
ExternalInputIterator, FileIterator, JCompilationUnit.JCompilationUnit$1, JCompilationUnit.JCompilationUnit$4, JMLEnumerationToIterator, Launcher.ToolIterator, TestClassGenerator.MethodsIterator

public interface Iterator

JML's specification of java.util.Iterator. Some of this specification is taken from ESC/Java.

$Revision: 1.15 $
Gary T. Leavens, Brandon Shilling, Joe Kiniry, David Cok

Class Specifications
public invariant this.moreElements == this.hasNext(0);

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  boolean moreElements
          Do we have more elements?
Ghost Field Summary
[instance]  Class elementType
          The type of the elements we return.
[instance]  boolean remove_called_since
          Has remove() been called since the last element was returned?
[instance]  boolean returnsNull
          Do we ever return null as an element?
Model Method Summary
 boolean hasNext(int n)
 Object nthNextElement(int n)
Method Summary
 boolean hasNext()
 Object next()
 void remove()

Model Field Detail


public boolean moreElements
Do we have more elements?

Specifications: instance
is in groups: objectState
Ghost Field Detail


public Class elementType
The type of the elements we return.

Specifications: instance


public boolean returnsNull
Do we ever return null as an element?

Specifications: instance


public boolean remove_called_since
Has remove() been called since the last element was returned? It is initially false, since no element has yet been returned.

Specifications: instance
Model Method Detail


public boolean hasNext(int n)
Specifications: pure
public normal_behavior
requires n >= 0;
ensures (* \result is true when this iterator has n+1 more elements to return *);


public Object nthNextElement(int n)
Specifications: pure
public normal_behavior
requires n >= 0&&this.hasNext(n);
ensures (* \result is the nth, counting from 0, next element that would be returned by this iterator *);
ensures !this.returnsNull ==> \result != null;
ensures \result == null||\typeof(\result ) <: this.elementType;
public normal_example
requires n == 0&&this.moreElements;
ensures (* \result == the object that would be returned by calling next() *);
Method Detail


public boolean hasNext()
public normal_behavior
assignable objectState;
ensures \result <==> this.moreElements;


public Object next()
public normal_behavior
requires this.moreElements;
requires_redundantly this.hasNext(0);
assignable objectState, remove_called_since, moreElements;
ensures !this.remove_called_since;
ensures (\result == null)||\typeof(\result ) <: this.elementType;
ensures !this.returnsNull ==> (\result != null);
public exceptional_behavior
requires !this.moreElements;
assignable \nothing;
signals_only java.util.NoSuchElementException;


public void remove()
public behavior
assignable objectState, remove_called_since;
ensures !\old(this.remove_called_since)&&this.remove_called_since;
signals_only java.lang.UnsupportedOperationException, java.lang.IllegalStateException;
signals (java.lang.UnsupportedOperationException) (* if this iterator does not support removing elements *);
signals (java.lang.IllegalStateException) \old(this.remove_called_since);


JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.