org.jmlspecs.samples.list.list3
Class E_OneWayList

java.lang.Object
  org.jmlspecs.samples.list.list3.OneWayList
      org.jmlspecs.samples.list.list3.E_OneWayList

Direct Known Subclasses:

TwoWayList

public class E_OneWayList

extends OneWayList

Class Specifications

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

 

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  int	length_

 

Fields inherited from class org.jmlspecs.samples.list.list3.OneWayList

cursorNode_, prevCursorNode_, theListNode_

 

Constructor Summary
	E_OneWayList()
protected	E_OneWayList(E_OneWayList othLst)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	append(Object newEntry)
Object	clone()
boolean	equals(nullable Object obj)
private  boolean	equalsNode(nullable OneWayNode nd1, nullable OneWayNode nd2)
int	hashCode()
void	insertAfterCursor(Object newEntry)
void	insertBeforeCursor(Object newEntry)
boolean	isEmpty()
protected  void	lastEntry()
int	length()
void	removeAllEntries()
void	removeEntry()

 

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

 

Field Detail

length_

protected int length_

Specifications:
is in groups: theList

E_OneWayList

public E_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 super();

E_OneWayList

protected E_OneWayList(E_OneWayList 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 length_, othLst.*;
captures othLst.theList;
callable super(org.jmlspecs.samples.list.list3.OneWayList), othLst.length();

length

public int length()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.theList.int_length();

     also

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

isEmpty

public boolean isEmpty()

Specifications: pure

public normal_behavior
assignable \nothing;
ensures \result == this.theList.isEmpty();

     also

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

equals

public boolean equals(nullable Object obj)

Overrides:

equals in class Object

Specifications: pure

     also

public normal_behavior
requires obj instanceof org.jmlspecs.samples.list.list3.OneWayList;
assignable \nothing;
ensures \result == ((org.jmlspecs.samples.list.list3.OneWayList)obj).theList.equals(this.theList);

     also

requires !(obj instanceof org.jmlspecs.samples.list.list3.OneWayList);
assignable \nothing;
ensures \result == false;

     also

protected code normal_behavior
requires \same ;
accessible obj.*, theListNode_.entries;
captures \nothing;
callable OneWayNode.getEntry(), OneWayNode.getNextNode();

Specifications inherited from overridden method equals(Object obj) in class Object:
       pure

public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);

     also

public normal_behavior
requires this == obj;
ensures \result ;

     also

public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;

     also

diverges false;
ensures obj == null ==> !\result ;

removeEntry

public void removeEntry()

Overrides:

removeEntry in class OneWayList

Specifications:

     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 OneWayList

Specifications:

     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 OneWayList

Specifications:

     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 ;

append

public void append(Object newEntry)

Specifications:

public normal_behavior
requires newEntry != null;
assignable theList, cursor;
ensures this.theList.equals(\old(this.theList).insertBack(newEntry))&&this.cursor == this.theList.int_length()-1;

     also

protected code normal_behavior
requires \same ;
accessible \nothing;
captures newEntry;
callable lastEntry(), isOffEnd(), insertBeforeCursor(java.lang.Object), firstEntry(), insertAfterCursor(java.lang.Object), incrementCursor();

removeAllEntries

public void removeAllEntries()

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 firstEntry(), isOffEnd(), removeEntry();

clone

public Object clone()

Overrides:

clone in class OneWayList

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

lastEntry

protected void lastEntry()

Specifications:

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

hashCode

public int hashCode()

Overrides:

hashCode in class Object

Specifications: pure

Specifications inherited from overridden method in class Object:

public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);

     also

public code normal_behavior
assignable \nothing;

equalsNode

private boolean equalsNode(nullable OneWayNode nd1,
                           nullable OneWayNode nd2)

Specifications: pure