org.jmlspecs.models
Class JMLEqualsBagEntryNode

java.lang.Object
  org.jmlspecs.models.JMLListValueNode
      org.jmlspecs.models.JMLEqualsBagEntryNode

All Implemented Interfaces:

Cloneable, JMLType, JMLValueType, Serializable

class JMLEqualsBagEntryNode

extends JMLListValueNode

Internal class used in the implementation of JMLEqualsBag.

Author:

Gary T. Leavens

See Also:

JMLEqualsBag, JMLEqualsBagEntry, JMLListValueNode

Class Specifications

public invariant this.elementType == \type(org.jmlspecs.models.JMLEqualsBagEntry)&&!this.containsNull; public invariant this.val != null&&this.val instanceof org.jmlspecs.models.JMLEqualsBagEntry; public invariant this.next != null ==> this.next instanceof org.jmlspecs.models.JMLEqualsBagEntryNode; public invariant this.entryElementType <: \type(java.lang.Object); public invariant this.val != null&&this.val instanceof org.jmlspecs.models.JMLEqualsBagEntry&&((org.jmlspecs.models.JMLEqualsBagEntry)this.val).elementType <: this.entryElementType; public invariant (this.next != null ==> ((org.jmlspecs.models.JMLEqualsBagEntryNode)this.next).entryElementType <: this.entryElementType); public invariant this.containsNullElements ==> this.entryElementType == \type(java.lang.Object); protected invariant this.containsNullElements <==> ((org.jmlspecs.models.JMLEqualsBagEntry)this.val).theElem == null||(this.next != null&&((org.jmlspecs.models.JMLEqualsBagEntryNode)this.next).containsNullElements); public constraint this.entryElementType == \old(this.entryElementType); public constraint this.containsNullElements == \old(this.containsNullElements);

Specifications inherited from class JMLListValueNode

public invariant ( \forall org.jmlspecs.models.JMLListValueNode l2; ; ( \forall org.jmlspecs.models.JMLType e1, e2; ; ( \forall \bigint n; ; this.equational_theory(this,l2,e1,e2,n)))); public invariant this.elementType <: \type(org.jmlspecs.models.JMLType); public invariant this.val != null ==> \typeof(this.val) <: this.elementType; public invariant this.val == null ==> \type(org.jmlspecs.models.JMLType) == this.elementType; public invariant_redundantly this.containsNull ==> \type(org.jmlspecs.models.JMLType) == 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;
boolean	containsNullElements           Whether this list can contain null elements in its bag entries;
Class	elementType           The type of the elements in this list.
Class	entryElementType           The type of the elements contained in the entries in this list.

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
JMLListValueNode	next           The next node in this list.
JMLType	val           The data contained in this list node.

 

Constructor Summary

JMLEqualsBagEntryNode(non_null JMLEqualsBagEntry entry, JMLEqualsBagEntryNode nxt)           Initialize this list to have the given bag entry as its first element followed by the given list.

 

Model Method Summary
\bigint	bi_indexOf(JMLType item)           Return the zero-based index of the first occurrence of the given element in the list, if there is one
boolean	equational_theory(JMLListValueNode ls, JMLListValueNode ls2, JMLType e1, JMLType e2, \bigint n)           An `equational' specification of lists, for use in the invariant.
JMLListValueNode	insertBefore(\bigint n, JMLType item)           Return a list that is like this list but with the given item inserted before the given index.
JMLType	itemAt(\bigint i)           Return the ith element of a list.
\bigint	length()           Tells the number of elements in the sequence; a synonym for length
JMLListValueNode	prefix(\bigint n)           Return a list containing the first n elements in this list.
JMLListValueNode	removeItemAt(\bigint n)           Return a list like this list, but without the element at the given zero-based index.
JMLListValueNode	removePrefix(\bigint n)           Return a list containing all but the first n elements in this list.
JMLListValueNode	replaceItemAt(\bigint n, JMLType 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
JMLListValueNode	append(JMLType item)           Return a list that consists of this list and the given element.
Object	clone()           Return a clone of this object.
JMLListValueNode	concat(non_null JMLListValueNode ls2)           Return a list that is the concatenation of this with the given lists.
static JMLEqualsBagEntryNode	cons(non_null JMLEqualsBagEntry hd, JMLEqualsBagEntryNode tl)           Return a JMLEqualsBagEntryNode containing the given entry followed by the given list.
static JMLListValueNode	cons(nullable JMLType hd, nullable JMLListValueNode tl)           Return a JMLListValueNode containing the given element followed by the given list.
boolean	equals(nullable Object ls2)           Test whether this object's value is equal to the given argument.
JMLType	getItem(JMLType item)           Return the zero-based index of the first occurrence of the given element in the list, if there is one
boolean	has(JMLType item)           Tells whether the given element is ".equals" to an element in the list.
int	hashCode()           Return a hash code for this object.
JMLType	head()           Return the first element in this list.
boolean	headEquals(JMLType item)           Tell if the head of the list is ".equals" to the given item.
int	indexOf(JMLType item)           Return the zero-based index of the first occurrence of the given element in the list, if there is one
JMLListValueNode	insertBefore(int n, JMLType 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(JMLListValueNode ls2)           Tells whether the elements of this list occur, in order, at the beginning of the given list, using ".equals" for comparisons.
JMLType	itemAt(int i)           Return the ith element of a list.
JMLType	last()           Return the last element in this list.
JMLListValueNode	prefix(int n)           Return a list containing the first n elements in this list.
JMLListValueNode	prepend(JMLType item)           Return a list that is like this, but with the given item at the front.
JMLListValueNode	remove(JMLType item)           Return a list that is like this list but without the first occurrence of the given item.
JMLEqualsBagEntryNode	removeBE(non_null JMLEqualsBagEntry entry)           Return a list that is like this list but without the first occurrence of the given bag entry.
JMLListValueNode	removeItemAt(int n)           Return a list like this list, but without the element at the given zero-based index.
JMLListValueNode	removeLast()           Return a list containing all but the last element in this.
JMLListValueNode	removePrefix(int n)           Return a list containing all but the first n elements in this list.
JMLListValueNode	replaceItemAt(int n, JMLType item)           Return a list like this, but with item replacing the element at the given zero-based index.
JMLListValueNode	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

entryElementType

public Class entryElementType

The type of the elements contained in the entries in this list.

containsNullElements

public boolean containsNullElements

Whether this list can contain null elements in its bag entries;

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 JMLType as the type of the list's elements.

containsNull

public boolean containsNull

Whether this list can contain null elements;

val

public final JMLType val

The data contained in this list node.

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

next

public final JMLListValueNode next

The next node in this list.

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

JMLEqualsBagEntryNode

public JMLEqualsBagEntryNode(non_null JMLEqualsBagEntry entry,
                             JMLEqualsBagEntryNode nxt)

Initialize this list to have the given bag entry as its first element followed by the given list. This does not do any cloning.

Parameters:

entry - the JMLEqualsBagEntry to place at the head of this list.

nxt - the JMLEqualsBagEntryNode to make the tail of this list.

See Also:

cons(org.jmlspecs.models.JMLEqualsBagEntry, org.jmlspecs.models.JMLEqualsBagEntryNode)

Specifications: (class)pure

public normal_behavior
requires entry != null;
assignable val, next, elementType, containsNull, owner;
assignable entryElementType, containsNullElements;
ensures this.val.equals(entry);
ensures this.next == nxt;
ensures this.entryElementType == (nxt == null ? entry.elementType : (nxt.entryElementType <: entry.elementType ? entry.elementType : ((entry.elementType <: nxt.entryElementType) ? nxt.entryElementType : \type(java.lang.Object))));
ensures this.containsNullElements == (((org.jmlspecs.models.JMLEqualsBagEntry)this.val).theElem == null||(this.next != null&&((org.jmlspecs.models.JMLEqualsBagEntryNode)this.next).containsNullElements));

equational_theory

public boolean equational_theory(JMLListValueNode ls,
                                 JMLListValueNode ls2,
                                 JMLType e1,
                                 JMLType e2,
                                 \bigint n)

An `equational' specification of lists, for use in the invariant.

Specifications: pure

public normal_behavior

{|

ensures \result <==> (new org.jmlspecs.models.JMLListValueNode(e1, null)).size() == 1;

also

ensures \result <==> (ls != null) ==> (new org.jmlspecs.models.JMLListValueNode(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.equals(ls.head());

also

ensures \result <==> (e1 != null) ==> cons(e1,ls).head().equals(e1);

also

ensures \result <==> (ls != null&&ls.val != null) ==> ls.itemAt(0).equals(ls.head());

also

ensures \result <==> ls != null&&0 < n&&n < ls.size() ==> ls.itemAt(n).equals(ls.next.itemAt(n-1));

|}

itemAt

public JMLType 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 ".equals" 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 JMLListValueNode(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(JMLType item)

Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:

item - the JMLType 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 ).equals(item)&&( \forall \bigint i; 0 <= i&&i < \result ; !(this.itemAt(i) != null&&this.itemAt(i).equals(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 JMLListValueNode 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 JMLListValueNode 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 JMLListValueNode 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 JMLListValueNode replaceItemAt(\bigint n,
                                      JMLType 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 JMLListValueNode insertBefore(\bigint n,
                                     JMLType 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;

cons

public static JMLEqualsBagEntryNode cons(non_null JMLEqualsBagEntry hd,
                                         JMLEqualsBagEntryNode tl)

Return a JMLEqualsBagEntryNode containing the given entry followed by the given list. This method handles any necessary cloning for value lists and it handles inserting null elements.

Parameters:

hd - the JMLEqualsBagEntry to place at the head of the result.

tl - the JMLEqualsBagEntryNode to make the tail of the result.

See Also:

JMLEqualsBagEntryNode(org.jmlspecs.models.JMLEqualsBagEntry, org.jmlspecs.models.JMLEqualsBagEntryNode)

Specifications: pure non_null

public normal_behavior
requires hd != null;
ensures \result != null&&\result .headEquals(hd)&&\result .next == tl;
ensures \result .equals(new org.jmlspecs.models.JMLEqualsBagEntryNode(hd, tl));

    implies_that

requires hd != null;
ensures tl == null <==> \result .next == null;
ensures \result != null&&\result .val instanceof org.jmlspecs.models.JMLEqualsBagEntry&&\result .entryElementType == (\result .next == null ? ((org.jmlspecs.models.JMLEqualsBagEntry)\result .val).elementType : (((org.jmlspecs.models.JMLEqualsBagEntryNode)\result .next).entryElementType <: ((org.jmlspecs.models.JMLEqualsBagEntry)\result .val).elementType ? ((org.jmlspecs.models.JMLEqualsBagEntry)\result .val).elementType : ((((org.jmlspecs.models.JMLEqualsBagEntry)\result .val).elementType <: ((org.jmlspecs.models.JMLEqualsBagEntryNode)\result .next).entryElementType) ? ((org.jmlspecs.models.JMLEqualsBagEntryNode)\result .next).entryElementType : \type(java.lang.Object))));
ensures \result != null&&\result .containsNullElements == (((org.jmlspecs.models.JMLEqualsBagEntry)\result .val).theElem == null||(\result .next != null&&((org.jmlspecs.models.JMLEqualsBagEntryNode)\result .next).containsNullElements));

clone

public Object clone()

Return a clone of this object.

Specified by:

clone in interface JMLValueType

Overrides:

clone in class JMLListValueNode

Specifications: non_null (class)pure

     also

public normal_behavior
ensures \result != null&&\result instanceof org.jmlspecs.models.JMLEqualsBagEntryNode&&((org.jmlspecs.models.JMLEqualsBagEntryNode)\result ).equals(this);

Specifications inherited from overridden method in class JMLListValueNode:
       non_null (class)pure

     also

public normal_behavior
ensures \result != null&&\result instanceof org.jmlspecs.models.JMLListValueNode&&((org.jmlspecs.models.JMLListValueNode)\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 JMLValueType:
       pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueType&&(* all externally-visible mutable objects contained directly in "this" must be cloned in \result. *);

    implies_that

ensures (* no direct aliases are created between this and \result *);

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

removeBE

public JMLEqualsBagEntryNode removeBE(non_null JMLEqualsBagEntry entry)

Return a list that is like this list but without the first occurrence of the given bag entry.

Specifications: (class)pure

public normal_behavior
requires !this.has(entry);
ensures this.equals(\result );

     also

public normal_behavior
old int index = this.indexOf(entry);
requires this.has(entry);
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))));

cons

public static JMLListValueNode cons(nullable JMLType hd,
                                    nullable JMLListValueNode tl)

Return a JMLListValueNode 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 value to place at the head of the result.

tl - the JMLListValueNode 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.JMLListValueNode(hd, tl));

    implies_that

public normal_behavior
ensures \result != null&&\result .containsNull <==> hd == null||(tl != null&&tl.containsNull);

head

public JMLType 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 .equals(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(JMLType item)

Tell if the head of the list is ".equals" to the given item.

See Also:

JMLListValueNode.has(JMLType)

Specifications: (class)pure

public normal_behavior
requires this.val != null;
ensures \result == (this.val.equals(item));

     also

public normal_behavior
requires this.val == null;
ensures \result == (item == null);

itemAt

public JMLType 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 ".equals" 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(JMLType item)

Tells whether the given element is ".equals" 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).equals(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(JMLListValueNode ls2)

Tells whether the elements of this list occur, in order, at the beginning of the given list, using ".equals" 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).equals(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 JMLValueType

Overrides:

equals in class Object

Specifications: (class)pure

     also

public normal_behavior
requires ls2 != null&&ls2 instanceof org.jmlspecs.models.JMLListValueNode;
ensures \result <==> this.isPrefixOf((org.jmlspecs.models.JMLListValueNode)ls2)&&((org.jmlspecs.models.JMLListValueNode)ls2).isPrefixOf(this);

     also

public normal_behavior
requires ls2 == null||!(ls2 instanceof org.jmlspecs.models.JMLListValueNode);
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 JMLValueType:
       pure

     also

public normal_behavior
ensures \result ==> ob2 != null&&(* all externally-visible objects contained in ob2 test as ".equals()" to the corresponding object in this (and vice versa) *);

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(JMLType item)

Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:

item - the JMLType 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 ).equals(item)&&( \forall int i; 0 <= i&&i < \result ; !(this.itemAt(i) != null&&this.itemAt(i).equals(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 JMLType 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 .equals(this.itemAt((int)(this.int_length()-1)));

    implies_that

ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;

getItem

public JMLType getItem(JMLType 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 JMLType 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:

JMLListValueNode.itemAt(int)

Specifications: (class)pure

public normal_behavior
requires this.has(item);

{|

requires item != null;
ensures \result .equals(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;

prefix

public JMLListValueNode 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 JMLListValueNode 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 JMLListValueNode 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 JMLListValueNode replaceItemAt(int n,
                                      JMLType 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 JMLListValueNode 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 JMLListValueNode concat(non_null JMLListValueNode 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 JMLListValueNode prepend(JMLType 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 JMLListValueNode append(JMLType 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 JMLListValueNode 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)).equals(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 JMLListValueNode insertBefore(int n,
                                     JMLType 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 JMLListValueNode remove(JMLType 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;