org.jmlspecs.samples.list.iterator
Interface RestartableIterator

All Superinterfaces:

Iterator

All Known Implementing Classes:

ListIterator, TwoWayIterator, TwoWayIterator

public interface RestartableIterator

extends Iterator

Class Specifications

Specifications inherited from class Object

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

Specifications inherited from interface Iterator

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

Model Field Summary
[instance]  JMLObjectBag	iteratedElems

 

Model fields inherited from interface org.jmlspecs.samples.list.iterator.Iterator

currElem, unchanged, uniteratedElems

 

Method Summary
Object	currentItem()
void	first()
boolean	isDone()
void	next()

 

Model Field Detail

iteratedElems

public JMLObjectBag iteratedElems

Specifications: instance
is in groups: uniteratedElems
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_ currLink_.prevEntries 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_.prevEntries

first

public void first()

Specifications:

public normal_behavior
requires this.unchanged;
assignable iteratedElems, currElem, uniteratedElems;
ensures this.uniteratedElems.equals(\old(this.iteratedElems).union(\old(this.uniteratedElems)))&&this.iteratedElems.isEmpty();

next

public void next()

Specified by:

next in interface Iterator

Specifications:

     also

public normal_behavior
requires this.unchanged&&!this.isDone();
assignable iteratedElems;
ensures this.iteratedElems.equals(\old(this.iteratedElems).insert(\old(this.currElem)));

Specifications inherited from overridden method in interface Iterator:

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

Specified by:

isDone in interface Iterator

Specifications: pure

     also

public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == this.uniteratedElems.isEmpty();

Specifications inherited from overridden method in interface Iterator:
       pure

public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == this.uniteratedElems.isEmpty();

currentItem

public Object currentItem()

Specified by:

currentItem in interface Iterator

Specifications: pure nullable

     also

public normal_behavior
requires this.unchanged&&!this.isDone();
assignable \nothing;
ensures \result == this.currElem;

Specifications inherited from overridden method in interface Iterator:
       pure nullable

public normal_behavior
requires this.unchanged&&!this.isDone();
assignable \nothing;
ensures \result == this.currElem;