JML

org.jmlspecs.samples.list.list1
Class ListIterator

java.lang.Object
  extended byorg.jmlspecs.samples.list.list1.ListIterator
All Implemented Interfaces:
Iterator, RestartableIterator

public class ListIterator
extends Object
implements RestartableIterator


Class Specifications
public invariant this.listPtr != null;
public invariant 0 <= this.currIndex&&this.currIndex <= this.listPtr.theList.int_length();
protected represents listPtr <- this.listRef_;
protected represents currIndex <- this.listRef_.cursor;
protected represents origChgLog <- this.origLog_;
protected represents currElem <- (!this.listRef_.isOffFront()&&!this.listRef_.isOffEnd()) ? this.currentItem() : null;
protected represents iteratedElems <- org.jmlspecs.models.JMLObjectBag.convertFrom(this.listRef_.theList.prefix(this.currIndex));
protected represents uniteratedElems <- org.jmlspecs.models.JMLObjectBag.convertFrom(this.listRef_.theList.removePrefix(this.currIndex));
protected represents currIndex <- this.listRef_.cursor;
protected represents unchanged <- (this.listRef_.changeLog == this.origChgLog);

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
           
 E_SLList listPtr
           
 int origChgLog
           
 
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  E_SLList listRef_
           
protected  int origLog_
           
 
Constructor Summary
private ListIterator()
           
  ListIterator(E_SLList lst)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object currentItem()
           
 void first()
           
 boolean isDone()
           
 void next()
           
 String toString()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Model Field Detail

listPtr

public E_SLList listPtr
Specifications:
datagroup contains: listRef_

currIndex

public int currIndex
Specifications:
is in groups: currElem uniteratedElems iteratedElems
datagroup contains: listRef_.cursor

origChgLog

public int origChgLog
Specifications:
datagroup contains: origLog_
Field Detail

listRef_

protected E_SLList listRef_
Specifications:
is in groups: listPtr
maps listRef_.cursor \into currIndex, listRef_.changeLog \into unchanged

origLog_

protected int origLog_
Specifications:
is in groups: origChgLog
Constructor Detail

ListIterator

public ListIterator(E_SLList lst)
Specifications:
public normal_behavior
requires lst != null;
assignable listPtr, currIndex, origChgLog;
ensures this.currIndex == 0&&( \forall java.lang.Object obj; ; lst.theList.count(obj) == this.listPtr.theList.count(obj))&&this.origChgLog == lst.changeLog;
     also
protected normal_behavior
requires lst != null;
assignable listRef_, listRef_.cursor, origLog_;
ensures this.listRef_.cursor == 0&&this.listRef_.theList.equals(lst.theList)&&\fresh(this.listRef_);

ListIterator

private ListIterator()
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 normal_behavior
assignable listRef_.cursor;
ensures this.listRef_.cursor == 0;
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&&this.currIndex < this.listPtr.theList.int_length();
assignable currIndex;
ensures this.currIndex == \pre(this.currIndex)+1;
     also
protected normal_behavior
requires !this.listRef_.isOffEnd();
assignable listRef_.cursor;
ensures this.listRef_.cursor == \pre(this.listRef_.cursor+1);
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 normal_behavior
assignable \nothing;
ensures \result == (this.listRef_.cursor == this.listRef_.theList.int_length());
    implies_that
public normal_behavior
requires this.unchanged;
assignable \nothing;
ensures \result == (this.currIndex == this.listPtr.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 normal_behavior
requires !this.listRef_.isOffFront()&&!this.listRef_.isOffEnd();
requires_redundantly this.listRef_.length() > 0;
assignable \nothing;
ensures \result == this.listRef_.theList.itemAt(this.listRef_.cursor);
    implies_that
public normal_behavior
requires this.unchanged&&0 <= this.currIndex&&this.currIndex < this.listPtr.theList.int_length();
assignable \nothing;
ensures \result == this.listPtr.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;

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.