JML

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
Method Detail

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;

JML

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.