java.util
Interface ListIterator

All Superinterfaces:

Iterator

public interface ListIterator

extends Iterator

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

Version:

$Revision: 1.16 $

Author:

Gary T. Leavens

Class Specifications

instance public invariant 0 <= this.cursor_position; instance public invariant this.previousElements != null; instance public represents cursor_position <- this.previousElements.int_size(); public initially this.previousElements.isEmpty();

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Specifications inherited from interface Iterator

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

Model Field Summary
[instance]  int	cursor_position
[instance]  JMLEqualsSequence	previousElements

 

Model fields inherited from interface java.util.Iterator

moreElements

 

Ghost Field Summary

 

Ghost fields inherited from interface java.util.Iterator

elementType, remove_called_since, returnsNull

 

Model Method Summary

 

Model methods inherited from interface java.util.Iterator

hasNext, nthNextElement

 

Method Summary
void	add(Object o)
boolean	hasNext()
boolean	hasPrevious()
Object	next()
int	nextIndex()
Object	previous()
int	previousIndex()
void	remove()
void	set(Object o)

 

Model Field Detail

cursor_position

public int cursor_position

Specifications: instance
is in groups: objectState
datagroup contains: previousElements

previousElements

public JMLEqualsSequence previousElements

Specifications: instance
is in groups: cursor_position

hasNext

public boolean hasNext()

Specified by:

hasNext in interface Iterator

Specifications: pure

Specifications inherited from overridden method in interface Iterator:

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

next

public Object next()

Specified by:

next in interface Iterator

Specifications:

     also

public normal_behavior
requires this.hasNext();
assignable objectState, remove_called_since, moreElements;
ensures this.previousElements.equals(\old(this.previousElements).insertBack(\result ));

Specifications inherited from overridden method in interface Iterator:

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;

hasPrevious

public boolean hasPrevious()

Specifications: pure

public normal_behavior
ensures \result <==> !this.previousElements.isEmpty();

previous

public Object previous()

Specifications:

public normal_behavior
requires this.hasPrevious();
assignable objectState, previousElements, remove_called_since;
ensures \result == \old(this.previousElements.last())&&this.previousElements.equals(\old(this.previousElements.header()));
ensures !this.remove_called_since;

nextIndex

public int nextIndex()

Specifications: pure

public normal_behavior
ensures \result == this.previousElements.int_size();
ensures_redundantly \result == this.cursor_position;

previousIndex

public int previousIndex()

Specifications: pure

public normal_behavior
ensures \result == this.previousElements.int_size()-1;
ensures_redundantly \result == this.cursor_position-1;

remove

public void remove()

Specified by:

remove in interface Iterator

Specifications:

     also

assignable objectState, remove_called_since;
assignable previousElements;
ensures this.previousElements.equals(this.previousElements.header());
ensures_redundantly this.previousElements.int_size() == \old(this.previousElements.int_size()-1);
ensures_redundantly this.cursor_position == \old(this.cursor_position-1);

Specifications inherited from overridden method in interface Iterator:

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

set

public void set(Object o)

Specifications:

assignable objectState, previousElements;
ensures this.previousElements.equals(\old(this.previousElements.header().insertBack(o)));
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.IllegalArgumentException, java.lang.IllegalStateException;
signals (java.lang.IllegalStateException) \old(this.remove_called_since);

add

public void add(Object o)

Specifications:

assignable objectState, previousElements, remove_called_since;
ensures this.remove_called_since;
ensures this.previousElements.equals(\old(this.previousElements.insertBack(o)));
signals_only java.lang.UnsupportedOperationException, java.lang.ClassCastException, java.lang.IllegalArgumentException;