org.jmlspecs.samples.list.list3
Class TwoWayList

java.lang.Object
  org.jmlspecs.samples.list.list3.OneWayList
      org.jmlspecs.samples.list.list3.E_OneWayList
          org.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

lastNode_

protected TwoWayNode lastNode_

Specifications:
is in groups: theList
maps lastNode_.entries \into theList

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

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