JML

org.jmlspecs.samples.list.list2
Class E_OneWayList

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

public class E_OneWayList
extends OneWayList


Class Specifications
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 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
 
Model fields inherited from class org.jmlspecs.samples.list.list2.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  int length_
           
 
Fields inherited from class org.jmlspecs.samples.list.list2.OneWayList
cursorNode_, theListNode_
 
Constructor Summary
  E_OneWayList()
           
protected E_OneWayList(E_OneWayList othLst)
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 void append(Object newEntry)
           
 Object clone()
           
 boolean equals(nullable Object obj)
           
private  boolean equalsNode(nullable OneWayNode nd1, nullable OneWayNode nd2)
           
 int hashCode()
           
 void insertAfterCursor(Object newEntry)
           
 void insertBeforeCursor(Object newEntry)
           
 boolean isEmpty()
           
protected  void lastEntry()
           
 int length()
           
 void removeAllEntries()
           
 void removeEntry()
           
 
Methods inherited from class org.jmlspecs.samples.list.list2.OneWayList
firstEntry, getEntry, incrementCursor, isOffEnd, isOffFront, previousNode, replaceEntry, toString
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

length_

protected int length_
Specifications:
is in groups: theList
Constructor Detail

E_OneWayList

public E_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 super();

E_OneWayList

protected E_OneWayList(E_OneWayList 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 length_, othLst.*;
captures othLst.theList;
callable super(org.jmlspecs.samples.list.list2.OneWayList), othLst.length();
Method Detail

length

public int length()
Specifications: pure
public normal_behavior
assignable \nothing;
ensures \result == this.theList.int_length();
     also
protected code normal_behavior
requires \same ;
accessible length_;
captures \nothing;
callable \nothing;

isEmpty

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

equals

public boolean equals(nullable Object obj)
Overrides:
equals in class Object
Specifications: pure
     also
public normal_behavior
requires obj instanceof org.jmlspecs.samples.list.list2.OneWayList;
assignable \nothing;
ensures \result == ((org.jmlspecs.samples.list.list2.OneWayList)obj).theList.equals(this.theList);
     also
requires !(obj instanceof org.jmlspecs.samples.list.list2.OneWayList);
assignable \nothing;
ensures \result == false;
     also
protected code normal_behavior
requires \same ;
accessible obj.*, theListNode_.entries;
captures \nothing;
callable OneWayNode.getEntry(), OneWayNode.getNextNode();
Specifications inherited from overridden method equals(Object obj) in class Object:
       pure
public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
     also
public normal_behavior
requires this == obj;
ensures \result ;
     also
public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
     also
diverges false;
ensures obj == null ==> !\result ;

removeEntry

public void removeEntry()
Overrides:
removeEntry in class OneWayList
Specifications:
     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 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();

insertAfterCursor

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

insertBeforeCursor

public void insertBeforeCursor(Object newEntry)
Overrides:
insertBeforeCursor in class OneWayList
Specifications:
     also
protected code normal_behavior
requires \same ;
accessible length_;
captures newEntry;
callable previousNode(org.jmlspecs.samples.list.node.OneWayNode,org.jmlspecs.samples.list.node.OneWayNode), cursorNode_.insertAfter(java.lang.Object), incrementCursor();
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(), previousNode(org.jmlspecs.samples.list.node.OneWayNode,org.jmlspecs.samples.list.node.OneWayNode), insertAfterCursor(java.lang.Object), incrementCursor();

append

public void append(Object newEntry)
Specifications:
public normal_behavior
requires newEntry != null;
assignable theList, cursor;
ensures this.theList.equals(\old(this.theList).insertBack(newEntry))&&this.cursor == this.theList.int_length()-1;
     also
protected code normal_behavior
requires \same ;
accessible \nothing;
captures newEntry;
callable lastEntry(), isOffEnd(), insertBeforeCursor(java.lang.Object), insertAfterCursor(java.lang.Object), incrementCursor();

removeAllEntries

public void removeAllEntries()
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 firstEntry(), isOffEnd(), removeEntry(), incrementCursor();

clone

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

lastEntry

protected void lastEntry()
Specifications:
protected normal_behavior
assignable cursor;
ensures this.cursor == this.theList.int_length()-1;
     also
protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), cursorNode_.getNextNode(), incrementCursor();

hashCode

public int hashCode()
Overrides:
hashCode in class Object
Specifications: pure
Specifications inherited from overridden method in class Object:
public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
     also
public code normal_behavior
assignable \nothing;

equalsNode

private boolean equalsNode(nullable OneWayNode nd1,
                           nullable OneWayNode nd2)
Specifications: pure

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.