org.jmlspecs.samples.list.list3
Class TwoWayIterator

java.lang.Object
  org.jmlspecs.samples.list.list3.TwoWayIterator

All Implemented Interfaces:

Iterator, RestartableIterator

public class TwoWayIterator

extends Object

implements RestartableIterator

Class Specifications

protected invariant this.firstLink_ != null; public invariant this.theList != null; public invariant -1 <= this.currIndex&&this.currIndex <= this.theList.int_length(); protected represents theList <- this.firstLink_.allButFirst; protected represents uniteratedElems <- (this.currIndex <= 0) ? org.jmlspecs.models.JMLObjectBag.convertFrom(this.theList) : org.jmlspecs.models.JMLObjectBag.convertFrom(this.theList.removePrefix(this.currIndex)); protected represents iteratedElems <- (this.currIndex <= 0) ? org.jmlspecs.models.JMLObjectBag.EMPTY : org.jmlspecs.models.JMLObjectBag.convertFrom(this.theList.prefix(this.currIndex)); protected represents currElem <- (0 <= this.currIndex&&this.currIndex < this.theList.int_length()) ? this.theList.itemAt(this.currIndex) : null; protected represents currIndex <- this.indexOf(this.currLink_); public represents unchanged <- true;

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
int	currIndex
JMLObjectSequence	theList

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

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

iteratedElems

 

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

currElem, unchanged, uniteratedElems

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
protected  TwoWayNode	currLink_
protected  TwoWayNode	firstLink_
protected  TwoWayNode	lastLink_

 

Constructor Summary
protected	TwoWayIterator()
	TwoWayIterator(TwoWayNode link)

 

Model Method Summary
protected  int	indexOf(OneWayNode link)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	currentItem()
void	first()
boolean	isAtFront()
boolean	isDone()
void	last()
void	next()
void	previous()
String	toString()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Model Field Detail

theList

public JMLObjectSequence theList

Specifications:
is in groups: currElem uniteratedElems iteratedElems

currIndex

public int currIndex

Specifications:
is in groups: currElem uniteratedElems iteratedElems
datagroup contains: currLink_

firstLink_

protected TwoWayNode firstLink_

Specifications:
is in groups: currElem uniteratedElems iteratedElems
maps firstLink_.entries \into unchanged

currLink_

protected TwoWayNode currLink_

Specifications:
is in groups: currIndex currElem uniteratedElems iteratedElems
maps currLink_.entries \into unchanged uniteratedElems, currLink_.prevEntries \into unchanged iteratedElems

lastLink_

protected TwoWayNode lastLink_

Specifications:
is in groups: uniteratedElems

TwoWayIterator

public TwoWayIterator(TwoWayNode link)

Specifications:

public normal_behavior
requires link != null&&link.prevNode == null;
assignable currElem, uniteratedElems, iteratedElems, currIndex;
assignable_redundantly theList;
ensures this.currIndex == 0;

     also

protected code normal_behavior
requires \same ;
assignable currLink_, lastLink_, firstLink_;
accessible link, currLink_, firstLink_;
captures link;
callable isDone(), first(), next();

TwoWayIterator

protected TwoWayIterator()

Specifications:

protected code normal_behavior
assignable currElem, uniteratedElems, iteratedElems, currIndex;
ensures this.theList.isEmpty()&&this.currIndex == 0;

     also

protected code normal_behavior
requires \same ;
assignable firstLink_, currLink_, lastLink_;
accessible firstLink_, currLink_;
captures \nothing;
callable new org.jmlspecs.samples.list.node.TwoWayNode(), first();

indexOf

protected int indexOf(OneWayNode link)

Specifications: pure

first

public void first()

Specified by:

first in interface RestartableIterator

Specifications:

     also

public normal_behavior
requires this.unchanged;
assignable currIndex;
ensures this.currIndex == 0;

     also

protected code normal_behavior
requires \same ;
assignable currLink_;
accessible firstLink_;
captures \nothing;
callable firstLink_.getNextNode();

Specifications inherited from overridden method in interface RestartableIterator:

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 RestartableIterator

Specifications:

     also

public normal_behavior
requires this.unchanged&&0 <= this.currIndex&&this.currIndex < this.theList.int_length();
assignable currIndex;
ensures this.currIndex == \old(this.currIndex)+1;

     also

protected code normal_behavior
requires \same ;
assignable currLink_;
accessible currLink_;
captures \nothing;
callable currLink_.getNextNode();

Specifications inherited from overridden method in interface RestartableIterator:

     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 RestartableIterator

Specifications: (inherited)pure

     also

protected code normal_behavior
requires \same ;
assignable \nothing;
accessible currLink_;
captures \nothing;
callable \nothing;

    implies_that

public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == (this.currIndex == this.theList.int_length());

Specifications inherited from overridden method in interface RestartableIterator:
       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 RestartableIterator

Specifications: (inherited)pure

     also

protected code normal_behavior
requires \same ;
assignable \nothing;
accessible currLink_;
captures \nothing;
callable currLink_.getEntry();

    implies_that

public normal_behavior
requires 0 <= this.currIndex&&this.currIndex < this.theList.int_length()&&this.unchanged;
assignable \nothing;
ensures \result == this.theList.itemAt(this.currIndex);

Specifications inherited from overridden method in interface RestartableIterator:
       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;

last

public void last()

Specifications:

public normal_behavior
requires this.unchanged;
assignable currIndex;
ensures this.currIndex == this.theList.int_length()-1;

     also

protected code normal_behavior
requires \same ;
assignable currLink_;
accessible lastLink_;
captures \nothing;
callable \nothing;

previous

public void previous()

Specifications:

public normal_behavior
requires this.unchanged&&0 < this.currIndex;
assignable currIndex;
ensures this.currIndex == \old(this.currIndex)-1;

     also

protected code normal_behavior
requires \same ;
assignable currLink_;
accessible currLink_;
captures \nothing;
callable currLink_.getPrevNode();

isAtFront

public boolean isAtFront()

Specifications: pure

public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == (this.currIndex == 0);

     also

protected code normal_behavior
requires \same ;
assignable \nothing;
accessible firstLink_, currLink_;
captures \nothing;
callable firstLink_.getNextNode(), currLink_.getPrevNode();

toString

public String toString()

Overrides:

toString in class Object

Specifications: non_null

Specifications inherited from overridden method in class Object:
       non_null

public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);

     also

public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);

     also

public code model_program { ... }

    implies_that

assignable objectState;
ensures \result != null;