JML

org.jmlspecs.models
Class JMLListObjectNode

java.lang.Object
  extended byorg.jmlspecs.models.JMLListObjectNode
All Implemented Interfaces:
Cloneable, JMLType, Serializable

class JMLListObjectNode
extends Object
implements JMLType

An implementation class used in various models. These are singly-linked list nodes containing objects. The empty list is represented by null, which makes dealing with these lists tricky. Normal users should use JMLObjectSequence instead of this type to avoid these difficulties.

This type uses "==" to compare elements. The cons method does not clone elements that are passed into the list.

Version:
$Revision: 1.56 $
Author:
Gary T. Leavens, Albert L. Baker
See Also:
JMLObjectSequence, JMLObjectBag, JMLObjectSet

Class Specifications
public invariant ( \forall org.jmlspecs.models.JMLListObjectNode l2; ; ( \forall java.lang.Object e1, e2; ; ( \forall \bigint n; ; this.equational_theory(this,l2,e1,e2,n))));
public invariant this.elementType <: \type(java.lang.Object);
public invariant this.val != null ==> \typeof(this.val) <: this.elementType;
public invariant this.val == null ==> \type(java.lang.Object) == this.elementType;
public invariant_redundantly this.containsNull ==> \type(java.lang.Object) == this.elementType;
public invariant this.next != null ==> this.next.elementType <: this.elementType;
public invariant this.containsNull <==> this.has(null);
protected invariant this.containsNull <==> this.val == null||(this.next != null&&this.next.containsNull);
public invariant this.owner == null;
public constraint this.elementType == \old(this.elementType);
public constraint this.containsNull == \old(this.containsNull);

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
 JMLDataGroup elementState
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 boolean containsNull
          Whether this list can contain null elements;
 Class elementType
          The type of the elements in this list.
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
 JMLListObjectNode next
          The next node in this list.
 Object val
          The data contained in this list node.
 
Constructor Summary
JMLListObjectNode(Object item, JMLListObjectNode nxt)
          Initialize this list to have the given item as its first element followed by the given list.
 
Model Method Summary
 \bigint bi_indexOf(Object item)
          Return the zero-based index of the first occurrence of the given element in the list, if there is one
 boolean equational_theory(JMLListObjectNode ls, JMLListObjectNode ls2, Object e1, Object e2, \bigint n)
          An `equational' specification of lists, for use in the invariant.
 JMLListObjectNode insertBefore(\bigint n, Object item)
          Return a list that is like this list but with the given item inserted before the given index.
 Object itemAt(\bigint i)
          Return the ith element of a list.
 \bigint length()
          Tells the number of elements in the sequence; a synonym for length
 JMLListObjectNode prefix(\bigint n)
          Return a list containing the first n elements in this list.
 JMLListObjectNode removeItemAt(\bigint n)
          Return a list like this list, but without the element at the given zero-based index.
 JMLListObjectNode removePrefix(\bigint n)
          Return a list containing all but the first n elements in this list.
 JMLListObjectNode replaceItemAt(\bigint n, Object item)
          Return a list like this, but with item replacing the element at the given zero-based index.
 \bigint size()
          Tells the number of elements in the sequence; a synonym for length
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 JMLListObjectNode append(Object item)
          Return a list that consists of this list and the given element.
 Object clone()
          Return a clone of this object.
 JMLListObjectNode concat(non_null JMLListObjectNode ls2)
          Return a list that is the concatenation of this with the given lists.
static JMLListObjectNode cons(nullable Object hd, nullable JMLListObjectNode tl)
          Return a JMLListObjectNode containing the given element followed by the given list.
private static boolean elem_equals(Object item1, Object item2)
          Tell if the given elements are equal, taking null into account.
 boolean equals(nullable Object ls2)
          Test whether this object's value is equal to the given argument.
 Object getItem(Object item)
          Return the zero-based index of the first occurrence of the given element in the list, if there is one
 boolean has(Object item)
          Tells whether the given element is "==" to an element in the list.
 int hashCode()
          Return a hash code for this object.
 Object head()
          Return the first element in this list.
 boolean headEquals(Object item)
          Tell if the head of the list is "==" to the given item.
 int indexOf(Object item)
          Return the zero-based index of the first occurrence of the given element in the list, if there is one
 JMLListObjectNode insertBefore(int n, Object item)
          Return a list that is like this list but with the given item inserted before the given index.
 int int_length()
          Tells the number of elements in the list; a synonym for size.
 int int_size()
          Tells the number of elements in the list; a synonym for length.
 boolean isPrefixOf(JMLListObjectNode ls2)
          Tells whether the elements of this list occur, in order, at the beginning of the given list, using "==" for comparisons.
 Object itemAt(int i)
          Return the ith element of a list.
 Object last()
          Return the last element in this list.
 JMLListObjectNode prefix(int n)
          Return a list containing the first n elements in this list.
 JMLListObjectNode prepend(Object item)
          Return a list that is like this, but with the given item at the front.
 JMLListObjectNode remove(Object item)
          Return a list that is like this list but without the first occurrence of the given item.
 JMLListObjectNode removeItemAt(int n)
          Return a list like this list, but without the element at the given zero-based index.
 JMLListObjectNode removeLast()
          Return a list containing all but the last element in this.
 JMLListObjectNode removePrefix(int n)
          Return a list containing all but the first n elements in this list.
 JMLListObjectNode replaceItemAt(int n, Object item)
          Return a list like this, but with item replacing the element at the given zero-based index.
 JMLListObjectNode reverse()
          Return a list that is the reverse of this list.
 String toString()
          Return a string representation for this list.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Model Field Detail

elementState

public JMLDataGroup elementState
Specifications:
datagroup contains: val.objectState next.elementState
Ghost Field Detail

elementType

public Class elementType
The type of the elements in this list. This type is an upper bound on the element's types. The type is computed pessimistically, so that the order of adding elements does not matter; that is, if any element in the list is null, then we use Object as the type of the list's elements.


containsNull

public boolean containsNull
Whether this list can contain null elements;

Field Detail

val

public final Object val
The data contained in this list node.

Specifications:
is in groups: objectState
maps val.objectState \into elementState

next

public final JMLListObjectNode next
The next node in this list.

Specifications:
is in groups: objectState
maps next.elementState \into elementState
Constructor Detail

JMLListObjectNode

public JMLListObjectNode(Object item,
                         JMLListObjectNode nxt)
Initialize this list to have the given item as its first element followed by the given list. This does not do any cloning.

Parameters:
item - the object to place at the head of this list.
nxt - the _JMLListObjectNode to make the tail of this list.
Specifications: (class)pure
public normal_behavior
requires item != null;
assignable val, next, elementType, containsNull, owner;
ensures this.val == item&&this.next == nxt&&\typeof(item) <: this.elementType&&(nxt != null ==> nxt.elementType <: this.elementType)&&(nxt == null ==> this.elementType == \typeof(item))&&this.containsNull == (nxt == null ? false : nxt.containsNull);
     also
public normal_behavior
requires item == null;
assignable val, next, elementType, containsNull, owner;
ensures this.val == null&&this.next == nxt&&this.elementType == \type(java.lang.Object)&&this.containsNull;
    implies_that
ensures this.val == item&&this.next == nxt;
ensures item == null ==> this.containsNull;
ensures item != null&&nxt != null ==> this.containsNull == nxt.containsNull;
Model Method Detail

equational_theory

public boolean equational_theory(JMLListObjectNode ls,
                                 JMLListObjectNode ls2,
                                 Object e1,
                                 Object e2,
                                 \bigint n)
An `equational' specification of lists, for use in the invariant.

Specifications: pure
public normal_behavior
{|
ensures \result <==> (new org.jmlspecs.models.JMLListObjectNode(e1, null)).size() == 1;
also
ensures \result <==> (ls != null) ==> (new org.jmlspecs.models.JMLListObjectNode(e1, ls)).size() == 1+ls.size();
also
ensures \result <==> (ls != null) ==> (ls.next == null) == (ls.size() == 1);
also
ensures \result <==> ls != null&&ls.next != null ==> ls.size() == 1+ls.next.size();
also
ensures \result <==> (ls != null&&ls.val != null) ==> ls.val == (ls.head());
also
ensures \result <==> (e1 != null) ==> cons(e1,ls).head() == e1;
also
ensures \result <==> (ls != null&&ls.val != null) ==> ls.itemAt(0) == (ls.head());
also
ensures \result <==> ls != null&&0 < n&&n < ls.size() ==> ls.itemAt(n) == (ls.next.itemAt(n-1));
|}

itemAt

public Object itemAt(\bigint i)
              throws JMLListException
Return the ith element of a list.

Throws:
JMLListException
See Also:
#getItem(\bigint)
Specifications: (class)pure
public normal_behavior
requires 0 <= i&&i < this.length();
ensures \result != null ==> (* \result "==" the ith element of this *);
     also
public exceptional_behavior
requires !(0 <= i&&i < this.length());
signals_only org.jmlspecs.models.JMLListException;
    implies_that
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

size

public \bigint size()
Tells the number of elements in the sequence; a synonym for length

Specifications: pure
public normal_behavior
ensures (* \result is the number of JMLListObjectNode(s) in this *);
    implies_that
ensures \result > 0;

length

public \bigint length()
Tells the number of elements in the sequence; a synonym for length

Specifications: pure
public normal_behavior
ensures \result == this.size();
    implies_that
ensures \result > 0;

bi_indexOf

public \bigint bi_indexOf(Object item)
Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:
item - the Object sought in this.
Returns:
the first index at which item occurs or -1 if it does not.
Specifications: (class)pure
public normal_behavior
requires this.has(item)&&item != null;
ensures this.itemAt(\result ) == item&&( \forall \bigint i; 0 <= i&&i < \result ; !(this.itemAt(i) != null&&this.itemAt(i) == item));
ensures_redundantly (* \result is the first index at which item occurs in this *);
     also
public normal_behavior
requires this.has(item)&&item == null;
ensures this.itemAt(\result ) == null&&( \forall \bigint i; 0 <= i&&i < \result ; this.itemAt(i) != null);
ensures_redundantly (* \result is the first index at which null occurs in this *);
     also
public normal_behavior
requires !this.has(item);
ensures \result == -1;
    implies_that
ensures \result >= -1;

prefix

public JMLListObjectNode prefix(\bigint n)
Return a list containing the first n elements in this list.

Parameters:
n - the number of elements to leave in the result.
Returns:
null if n is not positive or greater than the length of this list.
Specifications: (class)pure
public normal_behavior
{|
requires 0 < n&&n <= this.length();
ensures \result != null&&\result .length() == n&&( \forall \bigint i; 0 <= i&&i < n; \result .itemAt(i) == this.itemAt(i));
also
requires n <= 0;
ensures \result == null;
also
requires this.length() < n;
ensures this.equals(\result );
|}
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

removePrefix

public JMLListObjectNode removePrefix(\bigint n)
Return a list containing all but the first n elements in this list.

Parameters:
n - the number of elements to remove
Returns:
null if n is negative or greater than the length of this list.
Specifications: (class)pure
public normal_behavior
{|
requires 0 < n&&n < this.length();
ensures \result != null&&\result .length() == this.length()-n&&( \forall \bigint i; n <= i&&i < this.length(); \result .itemAt(i-n) == this.itemAt(i));
also
requires n <= 0;
ensures this.equals(\result );
also
requires this.length() <= n;
ensures \result == null;
|}
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

removeItemAt

public JMLListObjectNode removeItemAt(\bigint n)
Return a list like this list, but without the element at the given zero-based index.

Parameters:
n - the zero-based index into the list.
Returns:
null if the index is out of range or if the list was of size 1.
Specifications: (class)pure
public normal_behavior
requires n == 0&&this.length() == 1;
ensures \result == null;
     also
public normal_behavior
requires n == 0&&this.length() > 1;
ensures \result .equals(this.removePrefix(1));
     also
public normal_behavior
requires 0 < n&&n < this.length();
ensures \result != null&&\result .length() == this.length()-1&&\result .equals(this.prefix(n).concat(this.removePrefix(n+1)));
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

replaceItemAt

public JMLListObjectNode replaceItemAt(\bigint n,
                                       Object item)
Return a list like this, but with item replacing the element at the given zero-based index.

Parameters:
n - the zero-based index into this list.
item - the item to put at index index
Specifications: (class)pure
public normal_behavior
requires 0 <= n&&n < this.length();
ensures \result != null&&\result .length() == this.length();
     also
public normal_behavior
requires n == 0&&this.length() == 1;
ensures \result != null&&\result .equals(cons(item,this.next));
     also
public normal_behavior
requires n == 0&&this.length() > 1;
ensures \result != null&&\result .equals(this.removePrefix(1).prepend(item));
     also
public normal_behavior
requires 0 < n&&n == this.length()-1;
ensures \result != null&&\result .equals(this.prefix(n).append(item));
     also
public normal_behavior
requires 0 < n&&n < this.length()-1;
ensures \result != null&&\result .length() == this.length()&&\result .equals(this.prefix(n).concat(this.removePrefix(n+1).prepend(item)));
    implies_that
requires 0 <= n;
ensures n == 0 ==> \result != null;
ensures item == null&&\result != null ==> \result .containsNull;
ensures item != null&&!this.containsNull&&\result != null ==> !\result .containsNull;

insertBefore

public JMLListObjectNode insertBefore(\bigint n,
                                      Object item)
                               throws JMLListException
Return a list that is like this list but with the given item inserted before the given index.

Throws:
JMLListException
Specifications: non_null (class)pure
public normal_behavior
requires 0 < n&&n <= this.length();
ensures \result != null&&\result .equals(this.prefix(n).concat(cons(item,this.removePrefix(n))));
     also
public normal_behavior
requires n == 0;
ensures \result != null&&\result .equals(cons(item,this));
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.length());
signals_only org.jmlspecs.models.JMLListException;
Method Detail

cons

public static JMLListObjectNode cons(nullable Object hd,
                                     nullable JMLListObjectNode tl)
Return a JMLListObjectNode containing the given element followed by the given list. Note that cons() adds elements to the front of a list. It handles any necessary cloning for value lists and it handles inserting null elements.

Parameters:
hd - the object to place at the head of the result.
tl - the JMLListObjectNode to make the tail of the result.
Specifications: pure
public normal_behavior
ensures \result .headEquals(hd)&&\result .next == tl;
ensures \result .equals(new org.jmlspecs.models.JMLListObjectNode(hd, tl));
    implies_that
public normal_behavior
ensures \result != null&&\result .containsNull <==> hd == null||(tl != null&&tl.containsNull);

head

public Object head()
Return the first element in this list. Note that head() handles any cloning necessary for value lists.

Specifications: (class)pure
public normal_behavior
requires this.val != null;
ensures \result != null&&\result == this.val;
     also
public normal_behavior
requires this.val == null;
ensures \result == null;
    implies_that
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

headEquals

public boolean headEquals(Object item)
Tell if the head of the list is "==" to the given item.

See Also:
has(Object)
Specifications: (class)pure
public normal_behavior
requires this.val != null;
ensures \result == (this.val == item);
     also
public normal_behavior
requires this.val == null;
ensures \result == (item == null);

elem_equals

private static boolean elem_equals(Object item1,
                                   Object item2)
Tell if the given elements are equal, taking null into account.

Specifications: pure

itemAt

public Object itemAt(int i)
              throws JMLListException
Return the ith element of a list.

Throws:
JMLListException
See Also:
#getItem(int)
Specifications: (class)pure
public normal_behavior
requires 0 <= i&&i < this.int_length();
ensures \result != null ==> (* \result "==" the ith element of this *);
     also
public exceptional_behavior
requires !(0 <= i&&i < this.int_length());
signals_only org.jmlspecs.models.JMLListException;
    implies_that
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

int_size

public int int_size()
Tells the number of elements in the list; a synonym for length.

Specifications: (class)pure
public normal_behavior
ensures \result == this.size();
    implies_that
ensures \result > 0;

int_length

public int int_length()
Tells the number of elements in the list; a synonym for size.

Specifications: (class)pure
public normal_behavior
ensures \result == this.length();
    implies_that
ensures \result > 0;

has

public boolean has(Object item)
Tells whether the given element is "==" to an element in the list.

Specifications: (class)pure
public normal_behavior
requires item != null;
ensures \result <==> ( \exists int i; 0 <= i&&i < this.int_length(); (this.itemAt(i) == null ? item == null : this.itemAt(i) == item));
     also
public normal_behavior
requires item == null;
ensures \result <==> ( \exists int i; 0 <= i&&i < this.int_length(); this.itemAt(i) == null);

isPrefixOf

public boolean isPrefixOf(JMLListObjectNode ls2)
Tells whether the elements of this list occur, in order, at the beginning of the given list, using "==" for comparisons.

Specifications: (class)pure
public normal_behavior
requires ls2 != null;
ensures \result <==> this.int_length() <= ls2.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); (ls2.itemAt(i) == null&&this.itemAt(i) == null)||(ls2.itemAt(i) != null&&ls2.itemAt(i) == (this.itemAt(i))));
     also
public normal_behavior
requires ls2 == null;
ensures !\result ;

equals

public boolean equals(nullable Object ls2)
Test whether this object's value is equal to the given argument.

Specified by:
equals in interface JMLType
Overrides:
equals in class Object
Specifications: (class)pure
     also
public normal_behavior
requires ls2 != null&&ls2 instanceof org.jmlspecs.models.JMLListObjectNode;
ensures \result <==> this.isPrefixOf((org.jmlspecs.models.JMLListObjectNode)ls2)&&((org.jmlspecs.models.JMLListObjectNode)ls2).isPrefixOf(this);
     also
public normal_behavior
requires ls2 == null||!(ls2 instanceof org.jmlspecs.models.JMLListObjectNode);
ensures \result <==> false;
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 ;
Specifications inherited from overridden method equals(Object ob2) in interface JMLType:
       pure
     also
public normal_behavior
ensures \result ==> ob2 != null&&(* ob2 is not distinguishable from this, except by using mutation or == *);
    implies_that
public normal_behavior
{|
requires ob2 != null&&ob2 instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)ob2).equals(this) == \result ;
also
requires ob2 == this;
ensures \result <==> true;
|}

hashCode

public int hashCode()
Return a hash code for this object.

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object
Specifications: (class)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;
Specifications inherited from overridden method in interface JMLType:
       pure

indexOf

public int indexOf(Object item)
Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:
item - the Object sought in this.
Returns:
the first index at which item occurs or -1 if it does not.
Specifications: (class)pure
public normal_behavior
requires this.has(item)&&item != null;
ensures this.itemAt(\result ) == item&&( \forall int i; 0 <= i&&i < \result ; !(this.itemAt(i) != null&&this.itemAt(i) == item));
ensures_redundantly (* \result is the first index at which item occurs in this *);
     also
public normal_behavior
requires this.has(item)&&item == null;
ensures this.itemAt(\result ) == null&&( \forall int i; 0 <= i&&i < \result ; this.itemAt(i) != null);
ensures_redundantly (* \result is the first index at which null occurs in this *);
     also
public normal_behavior
requires !this.has(item);
ensures \result == -1;
    implies_that
ensures \result >= -1;

last

public Object last()
Return the last element in this list.

Specifications: (class)pure
public normal_behavior
ensures (\result == null&&this.itemAt((int)(this.int_length()-1)) == null)||\result == (this.itemAt((int)(this.int_length()-1)));
    implies_that
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

getItem

public Object getItem(Object item)
               throws JMLListException
Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:
item - the Object sought in this list.
Returns:
the first zero-based index at which item occurs.
Throws:
JMLListException - if the item does not occur in this list.
See Also:
itemAt(int)
Specifications: (class)pure
public normal_behavior
requires this.has(item);
{|
requires item != null;
ensures \result == (this.itemAt(this.indexOf(item)));
also
requires item == null;
ensures \result == null;
|}
     also
public exceptional_behavior
requires !this.has(item);
signals_only org.jmlspecs.models.JMLListException;
    implies_that
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

clone

public Object clone()
Return a clone of this object.

Specified by:
clone in interface JMLType
Overrides:
clone in class Object
Specifications: non_null (class)pure
     also
public normal_behavior
ensures \result != null&&\result instanceof org.jmlspecs.models.JMLListObjectNode&&((org.jmlspecs.models.JMLListObjectNode)\result ).equals(this);
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]);
Specifications inherited from overridden method in interface JMLType:
       pure
     also
public normal_behavior
ensures \result != null;
ensures \result instanceof org.jmlspecs.models.JMLType;
ensures ((org.jmlspecs.models.JMLType)\result ).equals(this);
    implies_that
ensures \result != null&&\typeof(\result ) <: \type(org.jmlspecs.models.JMLType);

prefix

public JMLListObjectNode prefix(int n)
Return a list containing the first n elements in this list.

Parameters:
n - the number of elements to leave in the result.
Returns:
null if n is not positive or greater than the length of this list.
Specifications: (class)pure
public normal_behavior
{|
requires 0 < n&&n <= this.int_length();
ensures \result != null&&\result .int_length() == n&&( \forall int i; 0 <= i&&i < n; \result .itemAt(i) == this.itemAt(i));
also
requires n <= 0;
ensures \result == null;
also
requires this.int_length() < n;
ensures this.equals(\result );
|}
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

removePrefix

public JMLListObjectNode removePrefix(int n)
Return a list containing all but the first n elements in this list.

Parameters:
n - the number of elements to remove
Returns:
null if n is negative or greater than the length of this list.
Specifications: (class)pure
public normal_behavior
{|
requires 0 < n&&n < this.int_length();
ensures \result != null&&\result .int_length() == this.int_length()-n&&( \forall int i; n <= i&&i < this.int_length(); \result .itemAt((int)(i-n)) == this.itemAt(i));
also
requires n <= 0;
ensures this.equals(\result );
also
requires this.int_length() <= n;
ensures \result == null;
|}
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

removeItemAt

public JMLListObjectNode removeItemAt(int n)
Return a list like this list, but without the element at the given zero-based index.

Parameters:
n - the zero-based index into the list.
Returns:
null if the index is out of range or if the list was of size 1.
Specifications: (class)pure
public normal_behavior
requires n == 0&&this.int_length() == 1;
ensures \result == null;
     also
public normal_behavior
requires n == 0&&this.int_length() > 1;
ensures \result .equals(this.removePrefix(1));
     also
public normal_behavior
requires 0 < n&&n < this.int_length();
ensures \result != null&&\result .int_length() == this.int_length()-1&&\result .equals(this.prefix(n).concat(this.removePrefix((int)(n+1))));
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

replaceItemAt

public JMLListObjectNode replaceItemAt(int n,
                                       Object item)
Return a list like this, but with item replacing the element at the given zero-based index.

Parameters:
n - the zero-based index into this list.
item - the item to put at index index
Specifications: (class)pure
public normal_behavior
requires 0 <= n&&n < this.int_length();
ensures \result != null&&\result .int_length() == this.int_length();
     also
public normal_behavior
requires n == 0&&this.int_length() == 1;
ensures \result != null&&\result .equals(cons(item,this.next));
     also
public normal_behavior
requires n == 0&&this.int_length() > 1;
ensures \result != null&&\result .equals(this.removePrefix(1).prepend(item));
     also
public normal_behavior
requires 0 < n&&n == this.int_length()-1;
ensures \result != null&&\result .equals(this.prefix(n).append(item));
     also
public normal_behavior
requires 0 < n&&n < this.int_length()-1;
ensures \result != null&&\result .int_length() == this.int_length()&&\result .equals(this.prefix(n).concat(this.removePrefix(n+1).prepend(item)));
    implies_that
requires 0 <= n;
ensures n == 0 ==> \result != null;
ensures item == null&&\result != null ==> \result .containsNull;
ensures item != null&&!this.containsNull&&\result != null ==> !\result .containsNull;

removeLast

public JMLListObjectNode removeLast()
Return a list containing all but the last element in this.

Specifications: (class)pure
public normal_behavior
ensures \result == null ==> this.int_length() == 1;
ensures \result != null ==> \result .equals(this.prefix((int)(this.int_length()-1)));
    implies_that
ensures !this.containsNull&&\result != null ==> !\result .containsNull;

concat

public JMLListObjectNode concat(non_null JMLListObjectNode ls2)
Return a list that is the concatenation of this with the given lists.

Parameters:
ls2 - the list to place at the end of this list in the result.
Returns:
the concatenation of this list and ls2.
Specifications: non_null (class)pure
public normal_behavior
requires ls2 != null;
ensures \result != null&&\result .int_length() == this.int_length()+ls2.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); \result .itemAt(i) == this.itemAt(i))&&( \forall int i; 0 <= i&&i < ls2.int_length(); \result .itemAt((int)(this.int_length()+i)) == ls2.itemAt(i));
ensures (* \result is the concatenation of this followed by ls2 *);

prepend

public JMLListObjectNode prepend(Object item)
Return a list that is like this, but with the given item at the front. Note that this clones the item if necessary.

Parameters:
item - the element to place at the front of the result.
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .equals(cons(item,this));
ensures_redundantly \result != null&&\result .int_length() == this.int_length()+1;

append

public JMLListObjectNode append(Object item)
Return a list that consists of this list and the given element.

Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .equals(cons(item,this.reverse()).reverse());
ensures_redundantly \result != null&&\result .int_length() == this.int_length()+1;

reverse

public JMLListObjectNode reverse()
Return a list that is the reverse of this list.

Specifications: non_null (class)pure
public normal_behavior
ensures \result .int_length() == this.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); (\result .itemAt((int)(this.int_length()-i-1)) != null&&\result .itemAt((int)(this.int_length()-i-1)) == (this.itemAt(i)))||(\result .itemAt((int)(this.int_length()-i-1)) == null&&this.itemAt(i) == null));
ensures_redundantly (* \result has the same elements but with the items arranged in the reverse order *);
    implies_that
ensures this.elementType == \result .elementType;
ensures this.containsNull <==> \result .containsNull;

insertBefore

public JMLListObjectNode insertBefore(int n,
                                      Object item)
                               throws JMLListException
Return a list that is like this list but with the given item inserted before the given index.

Throws:
JMLListException
Specifications: non_null (class)pure
public normal_behavior
requires 0 < n&&n <= this.int_length();
ensures \result != null&&\result .equals(this.prefix(n).concat(cons(item,this.removePrefix(n))));
     also
public normal_behavior
requires n == 0;
ensures \result != null&&\result .equals(cons(item,this));
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.int_length());
signals_only org.jmlspecs.models.JMLListException;

remove

public JMLListObjectNode remove(Object item)
Return a list that is like this list but without the first occurrence of the given item.

Specifications: (class)pure
public normal_behavior
requires !this.has(item);
ensures this.equals(\result );
     also
public normal_behavior
old int index = this.indexOf(item);
requires this.has(item);
ensures \result == null <==> \old(this.int_size() == 1);
ensures \result != null&&index == 0 ==> \result .equals(this.removePrefix(1));
ensures \result != null&&index > 0 ==> \result .equals(this.prefix(index).concat(this.removePrefix((int)(index+1))));

toString

public String toString()
Return a string representation for this list. The output is ML style.

Overrides:
toString in class Object
Specifications: non_null (class)pure
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;

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.