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

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;