JML

org.jmlspecs.samples.list.iterator
Interface Iterator

All Known Subinterfaces:
RestartableIterator
All Known Implementing Classes:
ListIterator, TwoWayIterator, TwoWayIterator

public interface Iterator


Class Specifications
instance public invariant this.uniteratedElems.has(this.currElem)||this.currElem == null;

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

Model Field Summary
[instance]  Object currElem
           
[instance]  boolean unchanged
           
[instance]  JMLObjectBag uniteratedElems
           
 
Method Summary
 Object currentItem()
           
 boolean isDone()
           
 void next()
           
 

Model Field Detail

uniteratedElems

public JMLObjectBag uniteratedElems
Specifications: instance
datagroup contains: org.jmlspecs.samples.list.iterator.RestartableIterator.iteratedElems org.jmlspecs.samples.list.list1.ListIterator.currIndex org.jmlspecs.samples.list.list2.TwoWayIterator.theList org.jmlspecs.samples.list.list2.TwoWayIterator.currIndex org.jmlspecs.samples.list.list2.TwoWayIterator.firstLink_ org.jmlspecs.samples.list.list2.TwoWayIterator.currLink_ currLink_.entries org.jmlspecs.samples.list.list2.TwoWayIterator.lastLink_ org.jmlspecs.samples.list.list3.TwoWayIterator.theList org.jmlspecs.samples.list.list3.TwoWayIterator.currIndex org.jmlspecs.samples.list.list3.TwoWayIterator.firstLink_ org.jmlspecs.samples.list.list3.TwoWayIterator.currLink_ currLink_.entries org.jmlspecs.samples.list.list3.TwoWayIterator.lastLink_

currElem

public Object currElem
Specifications: instance nullable
datagroup contains: org.jmlspecs.samples.list.list1.ListIterator.currIndex org.jmlspecs.samples.list.list2.TwoWayIterator.theList org.jmlspecs.samples.list.list2.TwoWayIterator.currIndex org.jmlspecs.samples.list.list2.TwoWayIterator.firstLink_ org.jmlspecs.samples.list.list2.TwoWayIterator.currLink_ org.jmlspecs.samples.list.list3.TwoWayIterator.theList org.jmlspecs.samples.list.list3.TwoWayIterator.currIndex org.jmlspecs.samples.list.list3.TwoWayIterator.firstLink_ org.jmlspecs.samples.list.list3.TwoWayIterator.currLink_

unchanged

public boolean unchanged
Specifications: instance
datagroup contains: listRef_.changeLog firstLink_.entries currLink_.entries currLink_.prevEntries firstLink_.entries currLink_.entries currLink_.prevEntries
Method Detail

next

public void next()
Specifications:
public normal_behavior
requires this.unchanged&&!this.isDone();
{|
requires this.uniteratedElems.int_size() > 1;
assignable uniteratedElems, currElem;
ensures this.uniteratedElems.equals(\old(this.uniteratedElems).remove(\old(this.currElem)))&&this.uniteratedElems.has(this.currElem);
ensures_redundantly this.uniteratedElems.int_size() == \old(this.uniteratedElems).int_size()-1;
also
requires this.uniteratedElems.int_size() == 1;
assignable uniteratedElems;
ensures this.uniteratedElems.isEmpty();
|}

isDone

public boolean isDone()
Specifications: pure
public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == this.uniteratedElems.isEmpty();

currentItem

public Object currentItem()
Specifications: pure nullable
public normal_behavior
requires this.unchanged&&!this.isDone();
assignable \nothing;
ensures \result == this.currElem;

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.