JML

org.jmlspecs.samples.list.list3
Class TwoWayIterator

java.lang.Object
  extended byorg.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_
Field Detail

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

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();
Model Method Detail

indexOf

protected int indexOf(OneWayNode link)
Specifications: pure
Method Detail

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;

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.