org.jmlspecs.samples.list.list2
Class OneWayList

java.lang.Object
  org.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

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

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

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;