org.jmlspecs.samples.list.list1
Class SLList

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

Direct Known Subclasses:

E_SLList

public class SLList

extends Object

Class Specifications

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
int	cursor
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  SLNode	cursorNode_
protected  SLNode	theListNode_

 

Constructor Summary
	SLList()
protected	SLList(SLNode listNode)
protected	SLList(SLList othLst)

 

Model Method Summary
protected  boolean	hasNode(SLNode currNode, SLNode nd)
protected  int	indexOf(SLNode nd)
protected  SLNode	nodeAt(int index)

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()
protected  void	decreaseCursor()
void	firstEntry()
Object	getEntry()
void	incrementCursor()
void	insertAfterCursor(Object newEntry)
void	insertBeforeCursor(Object newEntry)
boolean	isOffEnd()
boolean	isOffFront()
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.list1.DLList.lastNode_ theListNode_ theListNode_.entries org.jmlspecs.samples.list.list1.E_SLList.changeLog org.jmlspecs.samples.list.list1.E_SLList.length_

cursor

public int cursor

Specifications:
datagroup contains: cursorNode_

theListNode_

protected SLNode theListNode_

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

cursorNode_

protected SLNode cursorNode_

Specifications:
is in groups: cursor

SLList

public SLList()

Specifications:

public normal_behavior
assignable theList, cursor;
ensures this.theList != null&&this.theList.isEmpty()&&this.cursor == 0;

     also

protected code normal_behavior
requires \same ;
accessible \nothing;
captures \nothing;
callable new org.jmlspecs.samples.list.list1.node.SLNode(java.lang.Object);

SLList

protected SLList(SLList 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 theListNode_, othLst.theListNode_;
captures othLst.theListNode_.entries;
callable firstEntry(), othLst.theListNode_.clone();

SLList

protected SLList(SLNode listNode)

Specifications:

protected normal_behavior
requires listNode != null;
assignable theList, cursor;
ensures this.cursor == 0&&this.theListNode_.entries.equals(listNode.entries);

     also

protected code normal_behavior
requires \same ;
accessible theListNode_;
captures listNode.entries;
callable firstEntry(), listNode.clone();

indexOf

protected int indexOf(SLNode nd)

Specifications: pure

protected normal_behavior
requires this.hasNode(this.theListNode_,nd);

{|

requires nd.getNextNode() == null;
ensures \result == -1;

also

requires nd.getNextNode() != null;
ensures \result == this.indexOf(nd.getNextNode())+1;

|}

     also

requires nd == null;
ensures \result == this.theList.int_length();

nodeAt

protected SLNode nodeAt(int index)

Specifications: pure

protected normal_behavior
requires -1 <= index&&index <= this.theList.int_length();
ensures this.indexOf(\result ) == index;

hasNode

protected boolean hasNode(SLNode currNode,
                          SLNode nd)

Specifications: pure

protected normal_behavior
requires currNode != null;

{|

requires nd != null;

{|

requires nd == currNode;
ensures \result == true;

also

requires nd != currNode;
ensures \result == this.hasNode(currNode.getNextNode(),nd);

|}

also

requires nd == null;
ensures \result == false;

|}

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

isOffFront

public boolean isOffFront()

Specifications: pure

public normal_behavior
ensures \result == (this.cursor == -1);

     also

protected code normal_behavior
requires \same ;
captures \nothing;
accessible theListNode_;
callable \nothing;

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;

getEntry

public Object getEntry()

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

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

Specifications:

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 Object

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

decreaseCursor

protected void decreaseCursor()

Specifications:

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

     also

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

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;