java.util
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.

Version:

$Revision: 1.15 $

Author:

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

moreElements

public boolean moreElements

Do we have more elements?

Specifications: instance
is in groups: objectState

elementType

public Class elementType

The type of the elements we return.

Specifications: instance

returnsNull

public boolean returnsNull

Do we ever return null as an element?

Specifications: instance

remove_called_since

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

hasNext

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 *);

nthNextElement

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;

    for_example

public normal_example
requires n == 0&&this.moreElements;
ensures (* \result == the object that would be returned by calling next() *);

hasNext

public boolean hasNext()

Specifications:

public normal_behavior
assignable objectState;
ensures \result <==> this.moreElements;

next

public Object next()

Specifications:

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);

     also

public exceptional_behavior
requires !this.moreElements;
assignable \nothing;
signals_only java.util.NoSuchElementException;

remove

public void remove()

Specifications:

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);