org.jmlspecs.samples.list.list1
Class ListIterator

java.lang.Object
  org.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_

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

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

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;