org.jmlspecs.samples.list.list1
Class E_SLList

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

Direct Known Subclasses:

DLList

public class E_SLList

extends SLList

Class Specifications

protected invariant this.length_ == this.theList.int_length(); public constraint this.changeLog >= \pre(this.changeLog); protected represents changeLog <- this.log_;

Specifications inherited from class SLList

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	changeLog

 

Model fields inherited from class org.jmlspecs.samples.list.list1.SLList

cursor, 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_
protected  int	log_

 

Fields inherited from class org.jmlspecs.samples.list.list1.SLList

cursorNode_, theListNode_

 

Constructor Summary
	E_SLList()
protected	E_SLList(E_SLList othLst)
protected	E_SLList(SLNode listNode, int len)

 

Model Method Summary

 

Model methods inherited from class org.jmlspecs.samples.list.list1.SLList

hasNode, indexOf, nodeAt

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	append(Object newEntry)
Object	clone()
ListIterator	createIterator()
void	insertAfterCursor(Object newEntry)
void	insertBeforeCursor(Object newEntry)
boolean	isEmpty()
protected  void	lastEntry()
int	length()
void	removeAllEntries()
void	removeEntry()
void	replaceEntry(Object newEntry)

 

Methods inherited from class org.jmlspecs.samples.list.list1.SLList

decreaseCursor, firstEntry, getEntry, incrementCursor, isOffEnd, isOffFront, toString

 

Methods inherited from class java.lang.Object

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

 

Model Field Detail

changeLog

public int changeLog

Specifications:
is in groups: theList
datagroup contains: log_

length_

protected int length_

Specifications:
is in groups: theList

log_

protected int log_

Specifications:
is in groups: changeLog

E_SLList

public E_SLList()

Specifications:

public normal_behavior

{|

assignable theList, cursor;
ensures this.theList.isEmpty()&&this.cursor == 0;

also

assignable changeLog;
ensures this.changeLog == 0;

|}

     also

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

E_SLList

protected E_SLList(E_SLList othLst)

Specifications:

protected normal_behavior
requires othLst != null;
assignable theList, cursor, changeLog;
ensures this.theList.equals(othLst.theList)&&this.cursor == 0&&this.changeLog == othLst.changeLog;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable super(org.jmlspecs.samples.list.list1.SLList), firstEntry();
captures othLst.theList;

E_SLList

protected E_SLList(SLNode listNode,
                   int len)

Specifications:

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

     also

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

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_;
callable \nothing;
captures \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_;
callable \nothing;
captures \nothing;

createIterator

public ListIterator createIterator()

Specifications:

public normal_behavior
assignable \nothing;
ensures \result .listPtr.theList.equals(this.theList)&&\result .currIndex == 0;

     also

protected code normal_behavior
requires \same ;
accessible length_;
callable new org.jmlspecs.samples.list.list1.ListIterator(org.jmlspecs.samples.list.list1.E_SLList);
captures \nothing;

removeEntry

public void removeEntry()

Overrides:

removeEntry in class SLList

Specifications:

     also

public normal_behavior
requires !this.isOffFront()&&!this.isOffEnd();
assignable changeLog;
ensures this.changeLog == \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable super.removeEntry();
captures \nothing;

Specifications inherited from overridden method in class SLList:

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

insertAfterCursor

public void insertAfterCursor(Object newEntry)

Overrides:

insertAfterCursor in class SLList

Specifications:

     also

public normal_behavior
requires newEntry != null&&!this.isOffEnd();
assignable changeLog;
ensures this.changeLog == \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible length_, log_;
callable super.insertAfterCursor(java.lang.Object);
captures newEntry;

Specifications inherited from overridden method insertAfterCursor(Object newEntry) in class SLList:

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)

Overrides:

insertBeforeCursor in class SLList

Specifications:

     also

public normal_behavior
requires newEntry != null&&!this.isOffFront();
assignable changeLog;
ensures this.changeLog >= \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible log_;
callable decreaseCursor(), insertAfterCursor(java.lang.Object), incrementCursor();
captures newEntry;

Specifications inherited from overridden method insertBeforeCursor(Object newEntry) in class SLList:

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 ;

replaceEntry

public void replaceEntry(Object newEntry)

Overrides:

replaceEntry in class SLList

Specifications:

     also

public normal_behavior
requires !this.isOffFront()&&!this.isOffEnd()&&newEntry != null;
assignable changeLog;
ensures this.changeLog == \pre(this.changeLog)+1;

     also

protected normal_behavior
requires !this.isOffFront()&&!this.isOffEnd()&&newEntry != null;
assignable changeLog;
ensures \not_modified(length_);

     also

protected code normal_behavior
requires \same ;
accessible log_;
callable super.replaceEntry(java.lang.Object);
captures newEntry;

Specifications inherited from overridden method replaceEntry(Object newEntry) in class SLList:

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

append

public void append(Object newEntry)

Specifications:

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

     also

requires newEntry != null;
assignable changeLog;
ensures this.changeLog >= \pre(this.changeLog)+1;

     also

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

removeAllEntries

public void removeAllEntries()

Specifications:

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

     also

public normal_behavior
assignable changeLog;
ensures this.changeLog >= \pre(this.changeLog)+1;

     also

protected code normal_behavior
requires \same ;
accessible log_;
callable firstEntry(), isOffEnd(), removeEntry(), incrementCursor();
captures \nothing;

clone

public Object clone()

Overrides:

clone in class SLList

Specifications: non_null

     also

public normal_behavior
assignable \nothing;
ensures \result instanceof org.jmlspecs.samples.list.list1.E_SLList&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).theList.equals(this.theList)&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).cursor == 0&&((org.jmlspecs.samples.list.list1.E_SLList)\result ).changeLog == 0&&\fresh(\result );

     also

protected code normal_behavior
requires \same ;
accessible this;
callable new org.jmlspecs.samples.list.list1.E_SLList(org.jmlspecs.samples.list.list1.node.SLNode,int);
captures \nothing;

Specifications inherited from overridden method in class SLList:
       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]);

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 cursorNode_;
callable isOffEnd(), decreaseCursor(), incrementCursor();
captures \nothing;