JML

org.jmlspecs.samples.list.list3
Class TwoWayList

java.lang.Object
  extended byorg.jmlspecs.samples.list.list3.OneWayList
      extended byorg.jmlspecs.samples.list.list3.E_OneWayList
          extended byorg.jmlspecs.samples.list.list3.TwoWayList

public class TwoWayList
extends E_OneWayList


Class Specifications
protected invariant this.lastNode_ != null;
protected invariant this.lastNode_.entries.int_size() == 1;
protected invariant this.theListNode_.entries.int_size() == this.theList.int_size()+1;
protected invariant this.theListNode_ instanceof org.jmlspecs.samples.list.node.TwoWayNode&&(this.cursorNode_ == null||this.cursorNode_ instanceof org.jmlspecs.samples.list.node.TwoWayNode)&&this.lastNode_ instanceof org.jmlspecs.samples.list.node.TwoWayNode;
protected represents cursorNodeTwoWay <- (org.jmlspecs.samples.list.node.TwoWayNode)this.cursorNode_;

Specifications inherited from class E_OneWayList
protected invariant this.length_ == this.theList.int_length();

Specifications inherited from class OneWayList
protected invariant this.theListNode_ != null&&this.theListNode_.entries.int_size()-1 == this.theList.int_length();
protected invariant \reach(this.theListNode_).has(this.cursorNode_)||this.cursorNode_ == null;
protected invariant \reach(this.theListNode_).has(this.prevCursorNode_)||this.prevCursorNode_ == null;
protected invariant (this.prevCursorNode_ != null) ==> (this.prevCursorNode_.getNextNode() == this.cursorNode_);
protected invariant this.isOffEnd() <==> (this.cursorNode_ == null);
protected invariant this.isOffFront() <==> (this.cursorNode_ == this.theListNode_);
public invariant this.isOffFront()||this.isOffEnd()||(0 <= this.cursor&&this.cursor < this.theList.int_length());
public invariant this.theList != null&&( \forall int i; 0 <= i&&i < this.theList.int_length(); this.theList.itemAt(i) != null);
public invariant (this.isOffFront()||this.isOffEnd())||(this.theList.itemAt(this.cursor) == this.cursorEntry&&this.cursorEntry != null);
protected constraint this.theListNode_ == \old(this.theListNode_);
protected represents theList <- this.theListNode_.entries.trailer();
protected represents cursorEntry <- (this.cursorNode_ == null) ? null : this.cursorNode_.getEntry();
protected represents cursor <- (this.cursorNode_ == null) ? (int)(this.theListNode_.entries.int_size()-1) : (int)(this.theListNode_.entries.int_size()-this.cursorNode_.entries.int_size()-1);
public initially this.theList.isEmpty()&&this.cursor == 0;

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
protected  TwoWayNode cursorNodeTwoWay
           
 
Model fields inherited from class org.jmlspecs.samples.list.list3.OneWayList
cursor, cursorEntry, theList
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
protected  TwoWayNode lastNode_
           
 
Fields inherited from class org.jmlspecs.samples.list.list3.E_OneWayList
length_
 
Fields inherited from class org.jmlspecs.samples.list.list3.OneWayList
cursorNode_, prevCursorNode_, theListNode_
 
Constructor Summary
  TwoWayList()
           
protected TwoWayList(TwoWayList othLst)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
           
 TwoWayIterator createIterator()
           
 void decrementCursor()
           
 void insertAfterCursor(Object newEntry)
           
 void insertBeforeCursor(Object newEntry)
           
 void lastEntry()
           
 void removeEntry()
           
 
Methods inherited from class org.jmlspecs.samples.list.list3.E_OneWayList
append, equals, hashCode, isEmpty, length, removeAllEntries
 
Methods inherited from class org.jmlspecs.samples.list.list3.OneWayList
firstEntry, getEntry, incrementCursor, isOffEnd, isOffFront, replaceEntry, toString
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

cursorNodeTwoWay

protected TwoWayNode cursorNodeTwoWay
Specifications:
is in groups: cursor
Field Detail

lastNode_

protected TwoWayNode lastNode_
Specifications:
is in groups: theList
maps lastNode_.entries \into theList
Constructor Detail

TwoWayList

public TwoWayList()
Specifications:
public normal_behavior
assignable theList, cursor;
ensures this.theList.isEmpty()&&this.cursor == 0;
     also
protected code normal_behavior
requires \same ;
accessible theListNode_;
captures \nothing;
callable new org.jmlspecs.samples.list.node.TwoWayNode(java.lang.Object), firstEntry();

TwoWayList

protected TwoWayList(TwoWayList othLst)
Specifications:
protected normal_behavior
requires othLst != null;
assignable theList, cursor;
ensures this.theList.equals(othLst.theList)&&this.cursor == 0;
     also
protected code normal_behavior
requires \same ;
accessible othLst.theList, theListNode_, lastNode_;
accessible theListNode_, length_, lastNode_;
captures othLst.theList;
callable firstEntry();
callable firstEntry(), lastNode_.getNextNode();
Method Detail

decrementCursor

public void decrementCursor()
Specifications:
public normal_behavior
requires !this.isOffFront();
assignable cursor;
ensures this.cursor == \old(this.cursor)-1;
     also
protected code normal_behavior
requires \same ;
accessible lastNode_, cursorNode_, prevCursorNode_;
captures \nothing;
callable isOffFront(), isOffEnd(), lastEntry(), cursorNodeTwoWay.getPrevNode();
    implies_that
public normal_behavior
requires this.cursor == 0;
assignable cursor;
ensures this.cursor == -1;
ensures_redundantly this.isOffFront();

lastEntry

public void lastEntry()
Overrides:
lastEntry in class E_OneWayList
Specifications:
     also
public normal_behavior
assignable cursor;
ensures this.cursor == this.theList.int_length()-1;
     also
protected code normal_behavior
requires \same ;
accessible lastNode_;
captures \nothing;
callable lastNode_.getPrevNode();
Specifications inherited from overridden method in class E_OneWayList:
protected normal_behavior
assignable cursor;
ensures this.cursor == this.theList.int_length()-1;
     also
protected code normal_behavior
requires \same ;
accessible theListNode_, cursorNode_;
captures \nothing;
callable isOffEnd(), cursorNode_.getNextNode(), incrementCursor();

removeEntry

public void removeEntry()
Overrides:
removeEntry in class E_OneWayList
Specifications:
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_, length_;
captures \nothing;
callable isOffEnd(), isOffFront(), decrementCursor(), cursorNode_.getNextNode(), incrementCursor(), cursorNode_.removeNextNode();
Specifications inherited from overridden method in class E_OneWayList:
     also
protected code normal_behavior
requires \same ;
accessible length_;
captures \nothing;
callable super.removeEntry();
Specifications inherited from overridden method in class OneWayList:
public normal_behavior
old org.jmlspecs.models.JMLObjectSequence preList = (!this.isOffFront()&&!this.isOffEnd()) ? this.theList.removeItemAt(this.cursor) : null;
requires !this.isOffFront()&&!this.isOffEnd();
assignable theList, cursor;
ensures \not_modified(cursor)&&this.theList.equals(preList);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), isOffFront(), prevCursorNode_.removeNextNode(), prevCursorNode_.getNextNode();

insertAfterCursor

public void insertAfterCursor(Object newEntry)
Overrides:
insertAfterCursor in class E_OneWayList
Specifications:
     also
public normal_behavior
requires newEntry != null&&this.isOffEnd();
assignable theList, cursor;
ensures this.theList.equals(\old(this.theList).insertBack(newEntry))&&this.cursor == this.theList.int_length();
ensures_redundantly this.isOffEnd();
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_, length_;
captures newEntry;
callable isOffEnd(), decrementCursor(), cursorNode_.insertAfter(java.lang.Object), incrementCursor(), cursorNode_.getNextNode(), super.insertAfterCursor(java.lang.Object);
Specifications inherited from overridden method insertAfterCursor(Object newEntry) in class E_OneWayList:
     also
protected code normal_behavior
requires \same ;
accessible length_;
captures newEntry;
callable super.insertAfterCursor(java.lang.Object);
Specifications inherited from overridden method insertAfterCursor(Object newEntry) in class OneWayList:
public normal_behavior
requires newEntry != null;
{|
old org.jmlspecs.models.JMLObjectSequence preList = (!this.isOffFront()&&!this.isOffEnd()) ? this.theList.insertAfterIndex(this.cursor,newEntry) : null;
requires !this.isOffFront()&&!this.isOffEnd();
assignable theList, cursor;
ensures this.theList.equals(preList)&&\not_modified(cursor);
also
old org.jmlspecs.models.JMLObjectSequence preList = this.isOffFront() ? this.theList.insertFront(newEntry) : null;
requires this.isOffFront();
assignable theList, cursor;
ensures this.theList.equals(preList)&&\not_modified(cursor);
|}
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures newEntry;
callable isOffEnd(), cursorNode_.insertAfter(java.lang.Object);
    implies_that
public normal_behavior
requires this.isOffEnd();
assignable theList, cursor;
ensures \not_specified ;

insertBeforeCursor

public void insertBeforeCursor(Object newEntry)
Overrides:
insertBeforeCursor in class E_OneWayList
Specifications:
     also
public normal_behavior
requires newEntry != null&&this.isOffFront();
assignable theList, cursor;
ensures this.theList.equals(\old(this.theList).insertFront(newEntry))&&\not_modified(cursor);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_, length_;
captures newEntry;
callable isOffFront(), isOffEnd(), insertAfterCursor(java.lang.Object), decrementCursor(), incrementCursor();
Specifications inherited from overridden method insertBeforeCursor(Object newEntry) in class E_OneWayList:
     also
protected code normal_behavior
requires \same ;
accessible length_;
captures newEntry;
callable prevCursorNode_.insertAfter(java.lang.Object), prevCursorNode_.getNextNode();
Specifications inherited from overridden method insertBeforeCursor(Object newEntry) in class OneWayList:
public normal_behavior
old org.jmlspecs.models.JMLObjectSequence preList = (newEntry != null&&!this.isOffFront()) ? this.theList.insertBeforeIndex(this.cursor,newEntry) : null;
requires newEntry != null&&!this.isOffFront();
assignable theList, cursor;
ensures this.cursor == \pre(this.cursor)+1&&this.theList.equals(preList);
     also
protected code normal_behavior
requires \same ;
accessible \nothing;
captures newEntry;
callable isOffFront(), prevCursorNode_.insertAfter(java.lang.Object), prevCursorNode_.getNextNode();
    implies_that
public normal_behavior
requires this.isOffFront();
assignable \not_specified;
ensures \not_specified ;

clone

public Object clone()
Overrides:
clone in class E_OneWayList
Specifications: non_null
     also
public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list3.TwoWayList;
ensures_redundantly ((org.jmlspecs.samples.list.list3.TwoWayList)\result ).theList.equals(this.theList)&&((org.jmlspecs.samples.list.list3.TwoWayList)\result ).cursor == 0;
     also
protected code normal_behavior
requires \same ;
accessible theList;
captures theListNode_.entries;
callable new org.jmlspecs.samples.list.list3.TwoWayList(org.jmlspecs.samples.list.list3.TwoWayList);
Specifications inherited from overridden method in class E_OneWayList:
       non_null
     also
public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list3.E_OneWayList&&((org.jmlspecs.samples.list.list3.E_OneWayList)\result ).theList.equals(this.theList)&&((org.jmlspecs.samples.list.list3.E_OneWayList)\result ).cursor == 0&&\fresh(\result );
     also
protected code normal_behavior
requires \same ;
accessible this;
captures theList;
callable new org.jmlspecs.samples.list.list3.E_OneWayList(org.jmlspecs.samples.list.list3.E_OneWayList);
Specifications inherited from overridden method in class OneWayList:
       non_null
     also
public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list3.OneWayList&&((org.jmlspecs.samples.list.list3.OneWayList)\result ).cursor == 0&&((org.jmlspecs.samples.list.list3.OneWayList)\result ).theList.equals(this.theList);
     also
protected code normal_behavior
requires \same ;
accessible this;
captures theListNode_.entries;
callable new org.jmlspecs.samples.list.list3.OneWayList(org.jmlspecs.samples.list.list3.OneWayList);
Specifications inherited from overridden method in class Object:
       non_null
protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);
     also
protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));
     also
protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;
     also
protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);

createIterator

public TwoWayIterator createIterator()
Specifications:
     also
protected code normal_behavior
requires \same ;
accessible theList;
captures theListNode_;
callable new org.jmlspecs.samples.list.list3.TwoWayIterator(org.jmlspecs.samples.list.node.TwoWayNode);

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.