JML

org.jmlspecs.samples.list.list2
Class OneWayList

java.lang.Object
  extended byorg.jmlspecs.samples.list.list2.OneWayList
Direct Known Subclasses:
E_OneWayList

public class OneWayList
extends Object


Class Specifications
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 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_.allButFirst;
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
 int cursor
           
 Object cursorEntry
           
 JMLObjectSequence 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  OneWayNode cursorNode_
           
protected  OneWayNode theListNode_
           
 
Constructor Summary
  OneWayList()
           
protected OneWayList(OneWayList othLst)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
           
 void firstEntry()
           
 Object getEntry()
           
 void incrementCursor()
           
 void insertAfterCursor(Object newEntry)
           
 void insertBeforeCursor(Object newEntry)
           
 boolean isOffEnd()
           
 boolean isOffFront()
           
protected  OneWayNode previousNode(OneWayNode curr, OneWayNode node)
           
 void removeEntry()
           
 void replaceEntry(Object newEntry)
           
 String toString()
           
 
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Model Field Detail

theList

public JMLObjectSequence theList
Specifications:
datagroup contains: org.jmlspecs.samples.list.list2.E_OneWayList.length_ theListNode_ theListNode_.entries org.jmlspecs.samples.list.list2.TwoWayList.lastNode_ lastNode_.entries

cursor

public int cursor
Specifications:
datagroup contains: cursorEntry cursorNode_ org.jmlspecs.samples.list.list2.TwoWayList.cursorNodeTwoWay

cursorEntry

public Object cursorEntry
Specifications:
is in groups: cursor
datagroup contains: cursorNode_.theEntry
Field Detail

theListNode_

protected OneWayNode theListNode_
Specifications:
is in groups: theList
maps theListNode_.entries \into theList

cursorNode_

protected OneWayNode cursorNode_
Specifications:
is in groups: cursor
maps cursorNode_.theEntry \into cursorEntry
Constructor Detail

OneWayList

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

OneWayList

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

firstEntry

public void firstEntry()
Specifications:
public normal_behavior
assignable cursor;
ensures this.cursor == 0;
     also
protected code normal_behavior
requires \same ;
accessible theListNode_;
captures \nothing;
callable theListNode_.getNextNode();

incrementCursor

public void incrementCursor()
Specifications:
public normal_behavior
requires !this.isOffEnd();
assignable cursor;
ensures this.cursor == \pre(this.cursor+1);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), cursorNode_.getNextNode();

isOffEnd

public boolean isOffEnd()
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result == (this.cursor == this.theList.int_length());
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable \nothing;

isOffFront

public boolean isOffFront()
Specifications: pure
public normal_behavior
ensures \result == (this.cursor == -1);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_, theListNode_;
captures \nothing;
callable \nothing;

getEntry

public Object getEntry()
Specifications: pure
public normal_behavior
requires !this.isOffFront()&&!this.isOffEnd();
assignable \nothing;
ensures \result == this.cursorEntry;
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), isOffFront(), cursorNode_.getEntry();

removeEntry

public void removeEntry()
Specifications:
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 this.cursor == \pre(this.cursor-1)&&this.theList.equals(preList);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), isOffFront(), previousNode(org.jmlspecs.samples.list.node.OneWayNode,org.jmlspecs.samples.list.node.OneWayNode), cursorNode_.removeNextNode();

replaceEntry

public void replaceEntry(Object newEntry)
Specifications:
public normal_behavior
old org.jmlspecs.models.JMLObjectSequence preList = (newEntry != null&&!this.isOffFront()&&!this.isOffEnd()) ? this.theList.replaceItemAt(this.cursor,newEntry) : null;
requires !this.isOffFront()&&!this.isOffEnd()&&newEntry != null;
assignable theList;
ensures this.theList.equals(preList);
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_, newEntry;
captures newEntry;
callable cursorNode_.setEntry(java.lang.Object);

insertAfterCursor

public void insertAfterCursor(Object newEntry)
Specifications:
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);

insertBeforeCursor

public void insertBeforeCursor(Object newEntry)
Specifications:
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(), previousNode(org.jmlspecs.samples.list.node.OneWayNode,org.jmlspecs.samples.list.node.OneWayNode), insertAfterCursor(java.lang.Object), incrementCursor();

clone

public Object clone()
Overrides:
clone in class Object
Specifications: non_null
     also
public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list2.OneWayList&&((org.jmlspecs.samples.list.list2.OneWayList)\result ).cursor == 0&&((org.jmlspecs.samples.list.list2.OneWayList)\result ).theList.equals(this.theList);
     also
protected code normal_behavior
requires \same ;
accessible this;
captures theListNode_.entries;
callable new org.jmlspecs.samples.list.list2.OneWayList(org.jmlspecs.samples.list.list2.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]);

previousNode

protected OneWayNode previousNode(OneWayNode curr,
                                  OneWayNode node)
Specifications:
protected normal_behavior
requires curr != null;
assignable \nothing;
ensures \result .nextNode == node;
     also
protected code normal_behavior
requires \same ;
accessible curr, node;
captures \nothing;
callable curr.getNextNode(), previousNode(org.jmlspecs.samples.list.node.OneWayNode,org.jmlspecs.samples.list.node.OneWayNode);

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.