org.jmlspecs.samples.list.list1.node
Class DLNode

java.lang.Object
  org.jmlspecs.samples.list.list1.node.SLNode
      org.jmlspecs.samples.list.list1.node.DLNode

public class DLNode

extends SLNode

Class Specifications

protected invariant (this.prevNode != null) ? (this.prevNode.nextNode == this) : true; protected invariant (this.nextNode != null) ? (this.nextDL.prevNode == this) : true; protected invariant (* the nodes are linked both ways *); public invariant (this.nextNode == null||this.nextNode instanceof org.jmlspecs.samples.list.list1.node.DLNode); public invariant this.prevEntries != null; protected represents prevNode <- this.prevNode_; protected represents nextDL <- (org.jmlspecs.samples.list.list1.node.DLNode)this.nextNode_; protected represents prevEntries <- (this.prevNode_ == null) ? new org.jmlspecs.models.JMLObjectSequence() : this.prevNode_.prevEntries.insertBack(this.prevNode_.entry_); public represents nextDL <- (org.jmlspecs.samples.list.list1.node.DLNode)this.nextNode;

Specifications inherited from class SLNode

public invariant this.entries != null&&this.allButFirst != null&&this.entries.equals(this.allButFirst.insertFront(this.theEntry)); protected represents theEntry <- this.entry_; protected represents nextNode <- this.nextNode_; protected represents entries <- this.allButFirst.insertFront(this.entry_); protected represents allButFirst <- (this.nextNode_ == null) ? new org.jmlspecs.models.JMLObjectSequence() : this.nextNode_.entries;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary
DLNode	nextDL
JMLObjectSequence	prevEntries
DLNode	prevNode

 

Model fields inherited from class org.jmlspecs.samples.list.list1.node.SLNode

allButFirst, entries, nextNode, theEntry

 

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	prevNode_

 

Fields inherited from class org.jmlspecs.samples.list.list1.node.SLNode

entry_, nextNode_

 

Constructor Summary
	DLNode(Object ent)
protected	DLNode(Object ent, DLNode prvNode, DLNode nxtNode)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	clone()
protected  DLNode	cloneNext()
protected  DLNode	clonePrevious()
DLNode	getPrevNode()
void	insertAfter(Object newEntry)
void	insertBefore(Object newEntry)
protected  void	linkTo(DLNode nxtNode)
void	removeNextNode()

 

Methods inherited from class org.jmlspecs.samples.list.list1.node.SLNode

getEntry, getNextNode, setEntry, stringOfEntries, toString

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

prevEntries

public JMLObjectSequence prevEntries

Specifications:
is in groups: entries
datagroup contains: prevNode

nextDL

public DLNode nextDL

Specifications:
is in groups: nextNode

prevNode

public DLNode prevNode

Specifications:
is in groups: prevEntries
datagroup contains: prevNode_

prevNode_

protected DLNode prevNode_

Specifications:
is in groups: prevNode

DLNode

public DLNode(Object ent)

Specifications:

public normal_behavior
assignable entries;
ensures this.theEntry == ent&&this.entries.itemAt(0) == ent&&this.allButFirst.isEmpty()&&this.prevEntries.isEmpty();

DLNode

protected DLNode(Object ent,
                 DLNode prvNode,
                 DLNode nxtNode)

Specifications:

protected normal_behavior
requires (prvNode == null||prvNode.nextNode == null||prvNode.nextNode == nxtNode)&&(nxtNode == null||nxtNode.prevNode == null||nxtNode.prevNode == prvNode);
assignable entries;
ensures this.theEntry == ent&&this.entries.itemAt(0) == ent&&this.prevNode == prvNode&&this.nextNode == nxtNode;

insertAfter

public void insertAfter(Object newEntry)

Overrides:

insertAfter in class SLNode

Specifications:

     also

public normal_behavior
assignable entries;
ensures \not_modified(prevEntries);

Specifications inherited from overridden method insertAfter(Object newEntry) in class SLNode:

public normal_behavior
assignable allButFirst;
ensures this.allButFirst.equals(\old(this.allButFirst).insertFront(newEntry));

removeNextNode

public void removeNextNode()

Overrides:

removeNextNode in class SLNode

Specifications:

     also

public normal_behavior
assignable entries;
ensures \not_modified(prevEntries);

Specifications inherited from overridden method in class SLNode:

public normal_behavior
requires !this.allButFirst.isEmpty();
assignable allButFirst;
ensures this.allButFirst.equals(\old(this.allButFirst).trailer());

     also

requires this.allButFirst.isEmpty();
assignable \nothing;
ensures this.allButFirst.isEmpty();

getPrevNode

public DLNode getPrevNode()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.prevNode;

insertBefore

public void insertBefore(Object newEntry)

Specifications:

public normal_behavior
assignable prevEntries;
ensures this.prevEntries.equals(\old(this.prevEntries).insertBack(newEntry))&&\not_modified(allButFirst);

clone

public Object clone()

Overrides:

clone in class SLNode

Specifications: non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.node.DLNode&&((org.jmlspecs.samples.list.list1.node.DLNode)\result ).entries.equals(this.entries)&&((org.jmlspecs.samples.list.list1.node.DLNode)\result ).prevEntries.equals(this.prevEntries);

Specifications inherited from overridden method in class SLNode:
       non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.node.SLNode&&((org.jmlspecs.samples.list.list1.node.SLNode)\result ).entries.equals(this.entries);

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

cloneNext

protected DLNode cloneNext()

Specifications:

protected normal_behavior
assignable \nothing;
ensures \result .entries.equals(this.entries);
ensures \result .prevEntries.isEmpty();

clonePrevious

protected DLNode clonePrevious()

Specifications:

protected normal_behavior
assignable \nothing;
ensures \result .allButFirst.isEmpty();
ensures \result .prevEntries.equals(this.prevEntries);

linkTo

protected void linkTo(DLNode nxtNode)

Specifications:

protected normal_behavior
requires nxtNode != null;
assignable nextNode, nxtNode.prevNode;
ensures this.nextNode == nxtNode&&this.nextDL.prevNode == this;

     also

requires nxtNode == null;
assignable nextNode;
ensures this.nextNode == null;