org.jmlspecs.samples.list.list1
Class DLList

java.lang.Object
  org.jmlspecs.samples.list.list1.SLList
      org.jmlspecs.samples.list.list1.E_SLList
          org.jmlspecs.samples.list.list1.DLList

public class DLList

extends E_SLList

Class Specifications

protected invariant (* I.e. the first & last nodes are sentinel nodes *); protected invariant this.indexOf(this.lastNode_) == this.theList.int_length(); protected invariant_redundantly this.indexOf(this.theListNode_) == -1; protected invariant this.theListNode_ instanceof org.jmlspecs.samples.list.list1.node.DLNode&&this.cursorNode_ instanceof org.jmlspecs.samples.list.list1.node.DLNode&&this.lastNode_ instanceof org.jmlspecs.samples.list.list1.node.DLNode; protected constraint \pre(this.lastNode_) == this.lastNode_; protected represents theList <- this.theListNode_.entries.header().trailer();

Specifications inherited from class E_SLList

protected invariant this.length_ == this.theList.int_length(); public constraint this.changeLog >= \pre(this.changeLog); protected represents changeLog <- this.log_;

Specifications inherited from class SLList

protected invariant this.theListNode_ != null&&this.indexOf(this.theListNode_) == -1&&this.nodeAt(-1) == this.theListNode_; protected invariant \reach(this.theListNode_).has(this.cursorNode_)||this.cursorNode_ == null; 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); protected represents theList <- this.theListNode_.entries.trailer(); protected represents_redundantly theList \such_that ( \forall int i; i <= 0&&i < this.theList.int_length(); this.theList.itemAt(i) == this.nodeAt(i).getEntry()); protected represents cursor <- this.indexOf(this.cursorNode_); 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.list1.E_SLList

changeLog

 

Model fields inherited from class org.jmlspecs.samples.list.list1.SLList

cursor, 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  DLNode	lastNode_

 

Fields inherited from class org.jmlspecs.samples.list.list1.E_SLList

length_, log_

 

Fields inherited from class org.jmlspecs.samples.list.list1.SLList

cursorNode_, theListNode_

 

Constructor Summary
	DLList()
protected	DLList(DLList othLst)
protected	DLList(DLNode listNode, int len)

 

Model Method Summary

 

Model methods inherited from class org.jmlspecs.samples.list.list1.SLList

hasNode, indexOf, nodeAt

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()
void	decrementCursor()
void	firstEntry()
Object	getEntry()
void	incrementCursor()
void	insertAfterCursor(Object newEntry)
void	insertBeforeCursor(Object newEntry)
boolean	isOffEnd()
void	lastEntry()
void	removeEntry()
String	toString()

 

Methods inherited from class org.jmlspecs.samples.list.list1.E_SLList

append, createIterator, isEmpty, length, removeAllEntries, replaceEntry

 

Methods inherited from class org.jmlspecs.samples.list.list1.SLList

decreaseCursor, isOffFront

 

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

lastNode_

protected final DLNode lastNode_

Specifications:
is in groups: theList

DLList

public DLList()

Specifications:

public normal_behavior

{|

assignable theList, cursor;
ensures this.theList.isEmpty()&&this.cursor == 0;

also

assignable changeLog;
ensures this.changeLog == 0;

|}

     also

protected code normal_behavior
requires \same ;
accessible theListNode_, theListNode_.nextNode;
callable firstEntry(), new org.jmlspecs.samples.list.list1.node.DLNode(java.lang.Object), theListNode_.insertAfter(java.lang.Object), theListNode_.getNextNode();
captures \nothing;

DLList

protected DLList(DLList 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;
callable firstEntry();
captures othLst.theList;

DLList

protected DLList(DLNode listNode,
                 int len)

Specifications:

     also

protected code normal_behavior
requires \same ;
accessible length_, log_, listNode.entries;
callable DLNode.getNextNode(), firstEntry();
captures listNode;

firstEntry

public void firstEntry()

Overrides:

firstEntry in class SLList

Specifications:

     also

protected code normal_behavior
requires \same ;
accessible theListNode_;
callable theListNode_.getNextNode();
captures \nothing;

Specifications inherited from overridden method in class SLList:

public normal_behavior
assignable cursor;
ensures this.cursor == 0;

     also

protected code normal_behavior
requires \same ;
accessible theListNode_;
captures \nothing;
callable SLNode.getNextNode();

isOffEnd

public boolean isOffEnd()

Overrides:

isOffEnd in class SLList

Specifications: pure

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_, lastNode_;
callable \nothing;
captures \nothing;

Specifications inherited from overridden method in class SLList:
       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;

incrementCursor

public void incrementCursor()

Overrides:

incrementCursor in class SLList

Specifications:

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_;
callable isOffEnd(), theListNode_.getNextNode();
captures \nothing;

Specifications inherited from overridden method in class SLList:

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(), SLNode.getNextNode();

getEntry

public Object getEntry()

Overrides:

getEntry in class SLList

Specifications: non_null (inherited)pure

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_;
callable isOffEnd(), cursorNode_.getEntry();
captures \nothing;

Specifications inherited from overridden method in class SLList:
       pure

public normal_behavior
requires !this.isOffFront()&&!this.isOffEnd();
assignable \nothing;
ensures \result == this.theList.itemAt(this.cursor);

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_;
captures \nothing;
callable isOffEnd(), isOffFront(), SLNode.getEntry();

decrementCursor

public void decrementCursor()

Specifications:

public normal_behavior
requires !this.isOffFront();
assignable cursor;
ensures this.cursor == \pre(this.cursor)-1;

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_;
callable isOffFront(), DLNode.getPrevNode();
captures \nothing;

    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_SLList

Specifications:

     also

public normal_behavior
assignable cursor;
ensures this.cursor == this.theList.int_length()-1;

     also

protected code normal_behavior
requires \same ;
accessible lastNode_;
callable decrementCursor();
captures \nothing;

Specifications inherited from overridden method in class E_SLList:

protected normal_behavior
assignable cursor;
ensures this.cursor == this.theList.int_length()-1;

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_;
callable isOffEnd(), decreaseCursor(), incrementCursor();
captures \nothing;

removeEntry

public void removeEntry()

Overrides:

removeEntry in class E_SLList

Specifications:

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_, length_;
callable isOffEnd(), isOffFront(), DLNode.getPrevNode(), DLNode.removeNextNode();
captures \nothing;

Specifications inherited from overridden method in class E_SLList:

     also

public normal_behavior
requires !this.isOffFront()&&!this.isOffEnd();
assignable changeLog;
ensures this.changeLog == \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable super.removeEntry();
captures \nothing;

Specifications inherited from overridden method in class SLList:

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(), decreaseCursor(), SLNode.removeNextNode();

insertAfterCursor

public void insertAfterCursor(Object newEntry)

Overrides:

insertAfterCursor in class E_SLList

Specifications:

     also

public normal_behavior
requires newEntry != null&&this.isOffEnd();
assignable theList, cursor, changeLog;
ensures this.theList.equals(\pre(this.theList).insertBack(newEntry))&&this.cursor == this.theList.int_length()&&this.changeLog == \pre(this.changeLog)+1;
ensures_redundantly this.isOffEnd();

     also

protected code normal_behavior
requires \same ;
accessible cursorNode_, length_;
callable isOffEnd(), incrementCursor(), insertBeforeCursor(java.lang.Object);
captures newEntry;

Specifications inherited from overridden method insertAfterCursor(Object newEntry) in class E_SLList:

     also

public normal_behavior
requires newEntry != null&&!this.isOffEnd();
assignable changeLog;
ensures this.changeLog == \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable super.insertAfterCursor(java.lang.Object);
captures newEntry;

Specifications inherited from overridden method insertAfterCursor(Object newEntry) in class SLList:

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(), SLNode.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_SLList

Specifications:

     also

public normal_behavior
requires newEntry != null&&this.isOffFront();
assignable theList, cursor, changeLog;
ensures this.theList.equals(\pre(this.theList).insertFront(newEntry))&&\not_modified(cursor)&&this.changeLog == \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable isOffEnd(), incrementCursor(), DLNode.insertBefore(java.lang.Object);
captures newEntry;

Specifications inherited from overridden method insertBeforeCursor(Object newEntry) in class E_SLList:

     also

public normal_behavior
requires newEntry != null&&!this.isOffFront();
assignable changeLog;
ensures this.changeLog >= \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible log_;
callable decreaseCursor(), insertAfterCursor(java.lang.Object), incrementCursor();
captures newEntry;

Specifications inherited from overridden method insertBeforeCursor(Object newEntry) in class SLList:

public normal_behavior
requires newEntry != null&&!this.isOffFront();
assignable theList, cursor;
ensures this.cursor == \pre(this.cursor)+1&&this.theList.equals(\pre(this.theList.insertBeforeIndex(this.cursor,newEntry)));

     also

protected code normal_behavior
requires \same ;
accessible \nothing;
captures newEntry;
callable isOffFront(), decreaseCursor(), insertAfterCursor(java.lang.Object), incrementCursor();

    implies_that

public normal_behavior
requires this.isOffFront();
assignable theList, cursor;
ensures \not_specified ;

clone

public Object clone()

Overrides:

clone in class E_SLList

Specifications: non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.DLList;
ensures_redundantly ((org.jmlspecs.samples.list.list1.DLList)\result ).theList.equals(this.theList)&&((org.jmlspecs.samples.list.list1.DLList)\result ).cursor == 0;

     also

protected code normal_behavior
requires \same ;
accessible theList;
callable new org.jmlspecs.samples.list.list1.DLList(org.jmlspecs.samples.list.list1.node.DLNode,int);
captures theListNode_.entries;

Specifications inherited from overridden method in class E_SLList:
       non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.E_SLList&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).theList.equals(this.theList)&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).cursor == 0&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).changeLog == 0&&\fresh(\result );

     also

protected code normal_behavior
requires \same ;
accessible this;
callable new org.jmlspecs.samples.list.list1.E_SLList(org.jmlspecs.samples.list.list1.node.SLNode,int);
captures \nothing;

Specifications inherited from overridden method in class SLList:
       non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.SLList&&((org.jmlspecs.samples.list.list1.SLList)\result ).cursor == 0&&((org.jmlspecs.samples.list.list1.SLList)\result ).theList.equals(this.theList);

     also

protected code normal_behavior
requires \same ;
accessible this;
captures theListNode_.entries;
callable new org.jmlspecs.samples.list.list1.SLList(org.jmlspecs.samples.list.list1.node.SLNode);

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]);

toString

public String toString()

Overrides:

toString in class SLList

Specifications: non_null

Specifications inherited from overridden method in class SLList:
       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;