JML

org.jmlspecs.models
Class JMLValueSequence

java.lang.Object
  extended byorg.jmlspecs.models.JMLValueSequenceSpecs
      extended byorg.jmlspecs.models.JMLValueSequence
All Implemented Interfaces:
Cloneable, JMLCollection, JMLType, JMLValueType, Serializable

public class JMLValueSequence
extends JMLValueSequenceSpecs
implements JMLCollection

Sequences of values. This type uses ".equals" to compare elements, and clones elements that are passed into and returned from the sequence's methods.

The informal model for a JMLValueSequence is a finite mathematical sequence of elements (of type JMLType). In some examples, we will write <a,b,c> for a mathematical sequence of length 3, containing elements a, b, and c. Elements of sequences are "indexed" from 0, so the length of a sequence is always 1 more than the index of the last element in the sequence.

Version:
$Revision: 1.81 $
Author:
Gary T. Leavens, Albert L. Baker
See Also:
JMLCollection, JMLType, JMLObjectSequence, JMLValueSequenceEnumerator, JMLValueSequenceSpecs

Class Specifications
public invariant ( \forall org.jmlspecs.models.JMLValueSequence s2; ; ( \forall org.jmlspecs.models.JMLType e1, e2; ; ( \forall \bigint n; ; this.equational_theory(this,s2,e1,e2,n))));
public invariant this.elementType <: \type(org.jmlspecs.models.JMLType);
public invariant ( \forall org.jmlspecs.models.JMLType o; o != null&&this.has(o); \typeof(o) <: this.elementType);
public invariant_redundantly this.isEmpty() ==> !this.containsNull;
invariant this.theSeq != null ==> this.theSeq.owner == this;
protected invariant this.theSeq == null <==> this.length == 0;
protected invariant this.length >= 0;
protected invariant this.theSeq != null ==> this.length == this.theSeq.length();
protected invariant this.length == this.length();
public invariant this.owner == null;
protected represents length <- bigIntegerToBigint(this._length);

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

Specifications inherited from interface JMLCollection
instance public constraint this.elementType == \old(this.elementType);
instance public constraint this.containsNull == \old(this.containsNull);

Model Field Summary
 \bigint length
           
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Model fields inherited from interface org.jmlspecs.models.JMLCollection
elementState
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Ghost fields inherited from interface org.jmlspecs.models.JMLCollection
containsNull, elementType
 
Field Summary
protected  BigInteger _length
          This sequence's length.
static JMLValueSequence EMPTY
          The empty JMLValueSequence.
private static String IS_NOT_FOUND
           
private static String ITEM_PREFIX
           
protected  JMLListValueNode theSeq
          The list representing this sequence's elements, in order.
private static String TOO_BIG_TO_INSERT
           
 
Model Constructor Summary
protected JMLValueSequence(JMLListValueNode ls, \bigint len)
          Initialize this sequence based on the given representation.
 
Constructor Summary
  JMLValueSequence()
          Initialize this to be the empty sequence.
protected JMLValueSequence(JMLListValueNode ls, int len)
          Initialize this sequence based on the given representation.
  JMLValueSequence(JMLType e)
          Initialize this to be the sequence containing just the given element.
 
Model Method Summary
 \bigint bi_count(JMLType item)
          Tells the number of times a given element occurs in the sequence.
 \bigint bi_indexOf(JMLType item)
          Return the zero-based index of the first occurrence of the given element in the sequence, if there is one
static \bigint bigIntegerToBigint(BigInteger oBi)
           
static BigInteger bigintToBigInteger(\bigint biValue)
           
 boolean equational_theory(JMLValueSequence s, JMLValueSequence s2, JMLType e1, JMLType e2, \bigint n)
          An equational specification of the properties of sequences.
 JMLType get(\bigint i)
          Return the element at the given zero-based index; a synonym for itemAt(int).
 JMLValueSequence insertAfterIndex(\bigint afterThisOne, JMLType item)
          Return a sequence like this, but with item put immediately after the given index.
 JMLValueSequence insertBeforeIndex(\bigint beforeThisOne, JMLType item)
          Return a sequence like this, but with item put immediately before the given index.
 JMLType itemAt(\bigint i)
          Return the element at the given zero-based index.
 \bigint length()
          Tells the number of elements in the sequence; a synonym for #length.
 JMLValueSequence prefix(\bigint n)
          Return a sequence containing the first n elements in this sequence.
 JMLValueSequence removeItemAt(\bigint index)
          Return a sequence like this, but without the element at the given zero-based index.
 JMLValueSequence removePrefix(\bigint n)
          Return a sequence containing all but the first n elements in this.
 JMLValueSequence replaceItemAt(\bigint index, JMLType item)
          Return a sequence 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.
 JMLValueSequence subsequence(\bigint from, \bigint to)
          Returns a subsequence of this containing the elements beginning with index from (inclusive) and ending with index to (exclusive).
 
Model methods inherited from class org.jmlspecs.models.JMLValueSequenceSpecs
objectAt
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
          Return a clone of this object.
 JMLValueSequence concat(non_null JMLValueSequence s2)
          Return a sequence that is the concatenation of this with the given sequence.
 boolean containsAll(non_null Collection c)
          Tell whether, for each element in the given collection, there is a ".equals" element in this sequence.
static JMLValueSequence convertFrom(non_null Collection c)
          Return the sequence containing all the value in the given collection in the same order as the elements appear in the collection.
static JMLValueSequence convertFrom(non_null JMLCollection c)
          Return the sequence containing all the value in the given JMLCollection in the same order as the elements appear in the collection.
static JMLValueSequence convertFrom(non_null JMLType[] a)
          Return the sequence containing all the elements in the given array in the same order as the elements appear in the array.
static JMLValueSequence convertFrom(non_null JMLType[] a, int size)
          Return the sequence containing the first 'size' elements in the given array in the same order as the elements appear in the array.
 int count(JMLType item)
          Tells the number of times a given element occurs in the sequence.
 JMLValueSequenceEnumerator elements()
          Return a enumerator for this.
 boolean equals(nullable Object obj)
          Test whether this object's value is equal to the given argument.
 JMLType first()
          Return the first element in this sequence.
 JMLType get(int i)
          Return the element at the given zero-based index; a synonym for itemAt(int).
 boolean has(JMLType elem)
          Tells whether the given element is ".equals" to an element in the sequence.
 int hashCode()
          Return a hash code for this object.
 JMLValueSequence header()
          Return a sequence containing all but the last element in this.
 int indexOf(JMLType item)
          Return the zero-based index of the first occurrence of the given element in the sequence, if there is one
 JMLValueSequence insertAfterIndex(int afterThisOne, JMLType item)
          Return a sequence like this, but with item put immediately after the given index.
 JMLValueSequence insertBack(JMLType item)
          Return a sequence like this, but with the given item put an the end.
 JMLValueSequence insertBeforeIndex(int beforeThisOne, JMLType item)
          Return a sequence like this, but with item put immediately before the given index.
 JMLValueSequence insertFront(JMLType item)
          Return a sequence like this, but with the given item put an the front.
 int int_length()
          Tells the number of elements in the sequence; a synonym for #size.
 int int_size()
          Tells the number of elements in the sequence; a synonym for #length.
 boolean isDeletionFrom(non_null JMLValueSequence s2, JMLType elem)
          Tells whether this sequence is the result of deleting the given element once from the given sequence.
 boolean isEmpty()
          Tells whether this sequence is empty.
 boolean isInsertionInto(non_null JMLValueSequence s2, JMLType elem)
          Tells whether this sequence is the result of inserting the given element once into the given sequence.
 boolean isPrefix(non_null JMLValueSequence s2)
          Tells whether the elements of the this sequence occur, in order, at the beginning of the given sequence, using ".equals" for comparisons.
 boolean isProperPrefix(non_null JMLValueSequence s2)
          Tells whether this sequence is shorter than the given sequence, and also if the elements of this sequence occur, in order, at the beginning of the given sequence, using ".equals" for comparisons.
 boolean isProperSubsequence(non_null JMLValueSequence s2)
          Tells whether this sequence is strictly shorter than the given sequence and a subsequence of it.
 boolean isProperSuffix(non_null JMLValueSequence s2)
          Tells whether the this sequence is shorter than the given object, and also if the elements of this sequence occur, in order, at the end of the given sequence, using ".equals" for comparisons.
 boolean isProperSupersequence(non_null JMLValueSequence s2)
          Tells whether the given sequence is both longer than and a supersequence of this sequence.
 boolean isSubsequence(non_null JMLValueSequence s2)
          Tells whether this sequence is a subsequence of the given sequence.
 boolean isSuffix(non_null JMLValueSequence s2)
          Tells whether the elements of this sequence occur, in order, at the end of the given sequence, using ".equals" for comparisons.
 boolean isSupersequence(non_null JMLValueSequence s2)
          Tells whether the given sequence is a supersequence of this sequence.
 JMLType itemAt(int i)
          Return the element at the given zero-based index.
 JMLIterator iterator()
          Returns an iterator over this sequence.
 JMLType last()
          Return the last element in this sequence.
 JMLValueSequence prefix(int n)
          Return a sequence containing the first n elements in this sequence.
 JMLValueSequence removeItemAt(int index)
          Return a sequence like this, but without the element at the given zero-based index.
 JMLValueSequence removePrefix(int n)
          Return a sequence containing all but the first n elements in this.
 JMLValueSequence replaceItemAt(int index, JMLType item)
          Return a sequence like this, but with item replacing the element at the given zero-based index.
 JMLValueSequence reverse()
          Return a sequence that is the reverse of this sequence.
static JMLValueSequence singleton(JMLType e)
          Return the singleton sequence containing the given element.
 JMLValueSequence subsequence(int from, int to)
          Returns a subsequence of this containing the elements beginning with index from (inclusive) and ending with index to (exclusive).
 JMLType[] toArray()
          Return a new array containing all the elements of this in order.
 JMLValueBag toBag()
          Return a new JMLValueBag containing all the elements of this.
 JMLValueSet toSet()
          Return a new JMLValueSet containing all the elements of this.
 String toString()
          Return a string representation of this object.
 JMLValueSequence trailer()
          Return a sequence containing all but the first element in this.
 
Methods inherited from class org.jmlspecs.models.JMLValueSequenceSpecs
count, has
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.jmlspecs.models.JMLCollection
has
 

Model Field Detail

length

public \bigint length
Field Detail

theSeq

protected final JMLListValueNode theSeq
The list representing this sequence's elements, in order.

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

_length

protected final BigInteger _length
This sequence's length.

Specifications:
is in groups: objectState

EMPTY

public static final JMLValueSequence EMPTY
The empty JMLValueSequence.

See Also:
JMLValueSequence()
Specifications: non_null

ITEM_PREFIX

private static final String ITEM_PREFIX

IS_NOT_FOUND

private static final String IS_NOT_FOUND

TOO_BIG_TO_INSERT

private static final String TOO_BIG_TO_INSERT
Model Constructor Detail

JMLValueSequence

protected JMLValueSequence(JMLListValueNode ls,
                           \bigint len)
Initialize this sequence based on the given representation.

Specifications: (class)pure
requires ls == null <==> len == 0;
requires len >= 0;
assignable objectState, elementType, containsNull, owner;
ensures ls != null ==> this.elementType == ls.elementType;
ensures ls != null ==> this.containsNull == ls.containsNull;
ensures ls == null ==> this.elementType <: \type(org.jmlspecs.models.JMLType);
ensures ls == null ==> !this.containsNull;
Constructor Detail

JMLValueSequence

public JMLValueSequence()
Initialize this to be the empty sequence.

See Also:
EMPTY
Specifications: (class)pure
public normal_behavior
assignable objectState, elementType, containsNull, owner;
ensures this.isEmpty();
ensures_redundantly this.size() == 0;
ensures_redundantly (* this is an empty sequence *);
    implies_that
ensures this.elementType <: \type(org.jmlspecs.models.JMLType)&&!this.containsNull;

JMLValueSequence

public JMLValueSequence(JMLType e)
Initialize this to be the sequence containing just the given element.

Parameters:
e - the element that is the first element in this sequence.
See Also:
singleton(org.jmlspecs.models.JMLType)
Specifications: (class)pure
public normal_behavior
assignable objectState, elementType, containsNull, owner;
ensures this.int_length() == 1;
ensures (e == null ==> this.itemAt(0) == null)&&(e != null ==> this.itemAt(0).equals(e));
ensures_redundantly (* this is a sequence containing just e *);
     also
public model_program { ... }

JMLValueSequence

protected JMLValueSequence(JMLListValueNode ls,
                           int len)
Initialize this sequence based on the given representation.

Specifications: (class)pure
requires ls == null <==> len == 0;
requires len >= 0;
assignable objectState, elementType, containsNull, owner;
ensures ls != null ==> this.elementType == ls.elementType;
ensures ls != null ==> this.containsNull == ls.containsNull;
ensures ls == null ==> this.elementType <: \type(org.jmlspecs.models.JMLType);
ensures ls == null ==> !this.containsNull;
Model Method Detail

equational_theory

public boolean equational_theory(JMLValueSequence s,
                                 JMLValueSequence s2,
                                 JMLType e1,
                                 JMLType e2,
                                 \bigint n)
An equational specification of the properties of sequences.

Specifications: pure
public normal_behavior
{|
ensures \result <==> !(new org.jmlspecs.models.JMLValueSequence()).has(e1);
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence()).size() == 0;
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence(e1)).size() == 1;
also
ensures \result <==> e1 != null ==> (new org.jmlspecs.models.JMLValueSequence(e1)).itemAt(0).equals(e1);
also
ensures \result <==> e1 != null ==> s.insertFront(e1).first().equals(e1);
also
ensures \result <==> e1 != null ==> s.insertBack(e1).last().equals(e1);
also
ensures \result <==> e1 != null ==> s.insertFront(e1).itemAt(0).equals(e1);
also
ensures \result <==> s.insertFront(e1).size() == s.size()+1;
also
ensures \result <==> e1 != null ==> s.insertBack(e1).itemAt(s.size()).equals(e1);
also
ensures \result <==> s.insertBack(e1).size() == s.size()+1;
also
ensures \result <==> -1 <= n&&n < s.size()&&e1 != null ==> s.insertAfterIndex(n,e1).itemAt(n+1).equals(e1);
also
ensures \result <==> -1 <= n&&n < s.size() ==> s.insertAfterIndex(n,e1).size() == s.size()+1;
also
ensures \result <==> 0 <= n&&n <= s.size()&&e1 != null ==> s.insertBeforeIndex(n,e1).itemAt(n).equals(e1);
also
ensures \result <==> 0 <= n&&n <= s.size() ==> s.insertBeforeIndex(n,e1).size() == s.size()+1;
also
ensures \result <==> s.isPrefix(s2) == ( \forall int i; 0 <= i&&i < s.int_length(); (s2.itemAt(i) != null&&s2.itemAt(i).equals(s.itemAt(i)))||(s2.itemAt(i) == null&&s.itemAt(i) == null));
also
ensures \result <==> s.isSubsequence(s2) == s.int_length() <= s2.int_length()&&(s.isPrefix(s2)||s.isSubsequence(s2.trailer()));
also
ensures \result <==> s.isEmpty() == (s.size() == 0);
also
ensures \result <==> s.isEmpty() == (s.length == 0);
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence(e1)).equals(new org.jmlspecs.models.JMLValueSequence().insertFront(e1));
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence(e1)).equals(new org.jmlspecs.models.JMLValueSequence().insertBack(e1));
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence(e1)).equals(new org.jmlspecs.models.JMLValueSequence().insertAfterIndex(-1,e1));
also
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence(e1)).equals(new org.jmlspecs.models.JMLValueSequence().insertBeforeIndex(0,e1));
also
ensures \result <==> (s.size() >= 1 ==> s.equals(s.trailer().insertFront(s.first())));
also
ensures \result <==> (s.size() >= 1 ==> s.equals(s.header().insertBack(s.last())));
also
ensures \result <==> s.isProperSubsequence(s2) == (s.isSubsequence(s2)&&!s.equals(s2));
also
ensures \result <==> s.isSupersequence(s2) == s2.isSubsequence(s);
also
ensures \result <==> s.isProperSupersequence(s2) == s2.isProperSubsequence(s);
|}
    implies_that
ensures \result <==> (new org.jmlspecs.models.JMLValueSequence()).isEmpty();

itemAt

public JMLType itemAt(\bigint i)
               throws JMLSequenceException
Return the element at the given zero-based index.

Parameters:
i - the zero-based index into the sequence.
Throws:
JMLSequenceException - if the index oBiI is out of range.
See Also:
get(int), has(JMLType), count(JMLType)
Specifications: (class)pure
public normal_behavior
requires 0 <= i&&i < this.length;
ensures (* \result == null, if the ith element of this is null; otherwise, \result ".equals" the ith element of this *);
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;
     also
public exceptional_behavior
requires !(0 <= i&&i < this.length);
signals_only org.jmlspecs.models.JMLSequenceException;
    for_example
public normal_example
requires (* this is <w,x,y,z> and i is 0 *);
ensures (* \result is w.clone() *);
       also
public normal_example
requires (* this is <w,x,y,z> and i is 3 *);
ensures (* \result is z.clone() *);

get

public JMLType get(\bigint i)
            throws IndexOutOfBoundsException
Return the element at the given zero-based index; a synonym for itemAt(int).

Parameters:
i - the zero-based index into the sequence.
Throws:
IndexOutOfBoundsException - if the index i is out of range.
See Also:
#itemAt(\bigint)
Specifications: (class)pure
public normal_behavior
requires 0 <= i&&i < this.length;
ensures (* \result == null, if the ith element of this is null; otherwise, \result ".equals" the ith element of this *);
     also
public exceptional_behavior
requires !(0 <= i&&i < this.length);
signals_only java.lang.IndexOutOfBoundsException;
    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.

See Also:
#length(), isEmpty()
Specifications: pure
Specifications inherited from overridden method in interface JMLCollection:
       pure
public normal_behavior
ensures \result >= 0&&(* \result is the size of this collection *);

length

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

See Also:
#size(), isEmpty()
Specifications: pure

bi_count

public \bigint bi_count(JMLType item)
Tells the number of times a given element occurs in the sequence.

See Also:
has(JMLType), itemAt(int)
Specifications: (class)pure
public normal_behavior
requires item != null;
ensures \result == ( \num_of \bigint i; 0 <= i&&i < this.length(); this.itemAt(i) != null&&this.itemAt(i).equals(item));
     also
public normal_behavior
requires item == null;
ensures \result == ( \num_of \bigint i; 0 <= i&&i < this.length(); this.itemAt(i) == null);
    for_example
public normal_example
requires (* this is <a,b,c,d,c> and item is c *);
ensures \result == 2;
       also
public normal_example
requires (* this is <a,b,c,d,a> and item is q *);
ensures \result == 0;

bi_indexOf

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

Parameters:
item - the JMLType sought in this.
Returns:
the first index at which item occurs.
Throws:
JMLSequenceException - if item is not a member of the sequence.
See Also:
itemAt(int)
Specifications: (class)pure
public normal_behavior
requires this.has(item);
{|
requires item != null;
ensures this.itemAt(\result ).equals(item)&&( \forall \bigint i; 0 <= i&&i < \result ; !(this.itemAt(i).equals(item)));
ensures_redundantly (* \result is the first index at which item occurs in this *);
also
requires item == null;
ensures this.itemAt(\result ) == null&&( \forall \bigint i; 0 <= i&&i < \result ; this.itemAt(i) != null);
|}
     also
public exceptional_behavior
requires !this.has(item);
signals_only org.jmlspecs.models.JMLSequenceException;
    for_example
public normal_example
requires (* this is <w,x,y,z,x> and item is x *);
ensures (* \result is 1 *);

prefix

public JMLValueSequence prefix(\bigint n)
                        throws JMLSequenceException
Return a sequence containing the first n elements in this sequence.

Parameters:
n - the number of elements in the result.
Throws:
JMLSequenceException - if n is negative or greater than the length of the sequence.
See Also:
trailer(), removePrefix(int), subsequence(int, int)
Specifications: (class)pure
public normal_behavior
requires 0 <= n&&n <= this.length;
ensures \result .length == n&&( \forall \bigint i; 0 <= i&&i < n; (\result .itemAt(i) != null ==> \result .itemAt(i).equals(this.itemAt(i)))||(\result .itemAt(i) == null ==> this.itemAt(i) == null));
ensures_redundantly (* \result is the same as this, but with the last length-n items removed *);
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.length);
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !this.containsNull ==> !\result .containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and n is 0 *);
ensures (* \result is <> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 3 *);
ensures (* \result is <a,b,c> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 5 *);
ensures (* \result is <a,b,c,d,e> *);
       also
public normal_example
requires n == this.length;
ensures \result .equals(this);

removePrefix

public JMLValueSequence removePrefix(\bigint n)
                              throws JMLSequenceException
Return a sequence containing all but the first n elements in this.

Parameters:
n - the number of elements to remove
Throws:
JMLSequenceException - if n is negative or greater than the length of the sequence.
See Also:
header(), prefix(int), subsequence(int, int)
Specifications: (class)pure
public normal_behavior
requires 0 <= n&&n <= this.length;
ensures \result .length == this.length-n&&( \forall \bigint i; n <= i&&i < this.length; (\result .itemAt(i-n) != null&&\result .itemAt(i-n).equals(this.itemAt(i)))||(\result .itemAt(i-n) == null&&this.itemAt(i) == null));
ensures_redundantly (* \result is the same as this, but with the first n items removed *);
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.length);
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !this.containsNull ==> !\result .containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and n is 1 *);
ensures (* \result is <b,c,d,e> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 5 *);
ensures (* \result is <> *);
       also
public normal_example
requires n == this.length;
ensures \result .isEmpty();

removeItemAt

public JMLValueSequence removeItemAt(\bigint index)
                              throws JMLSequenceException
Return a sequence like this, but without the element at the given zero-based index.

Parameters:
index - the zero-based index into the sequence.
Throws:
JMLSequenceException - if the index is out of range.
See Also:
itemAt(int), removeItemAt(int), prefix(int), removePrefix(int), subsequence(int, int), concat(org.jmlspecs.models.JMLValueSequence)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= index&&index < this.length();
ensures \result .equals(this.prefix(index).concat(this.removePrefix(index+1)));
ensures_redundantly (* \result is the same as this, but with the item at position index removed *);
     also
public exceptional_behavior
requires !(0 <= index&&index < this.length());
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and index is 1 *);
ensures (* \result is <a,c,d,e> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and index is 4 *);
ensures (* \result is <a,b,c,d> *);

replaceItemAt

public JMLValueSequence replaceItemAt(\bigint index,
                                      JMLType item)
                               throws JMLSequenceException
Return a sequence like this, but with item replacing the element at the given zero-based index.

Parameters:
index - the zero-based index into the sequence.
item - the item to put at index index
Throws:
JMLSequenceException - if the index is out of range.
See Also:
itemAt(int), replaceItemAt(int, org.jmlspecs.models.JMLType)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= index&&index < this.length();
ensures \result .equals(this.removeItemAt(index).insertBeforeIndex(index,item));
ensures_redundantly (* \result is the same as this, but with item replacing the one at position index *);
     also
public exceptional_behavior
requires !(0 <= index&&index < this.length());
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures item != null ==> \typeof(item) <: \result .elementType;
ensures !\result .containsNull <== !this.containsNull&&item != null;
    for_example
public normal_example
requires (* this is <a,b,c,d,e>, item is x and index is 1 *);
ensures (* \result is <a,x,c,d,e> *);

insertAfterIndex

public JMLValueSequence insertAfterIndex(\bigint afterThisOne,
                                         JMLType item)
                                  throws JMLSequenceException,
                                         IllegalStateException
Return a sequence like this, but with item put immediately after the given index.

Parameters:
afterThisOne - a zero-based index into the sequence, or -1.
item - the item to put after index afterThisOne
Returns:
if the index is in range
Throws:
JMLSequenceException - if the index is out of range.
IllegalStateException
See Also:
insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)
Specifications: non_null (class)pure
public normal_behavior
requires -1 <= afterThisOne&&afterThisOne < this.length;
requires this.length < 2147483647;
ensures \result .equals(this.insertBeforeIndex((int)(afterThisOne+1),item));
ensures_redundantly (* \result is the same sequence as this, but with item inserted after the index "afterThisOne" *);
     also
public exceptional_behavior
requires !(-1 <= afterThisOne&&afterThisOne < this.length);
signals (org.jmlspecs.models.JMLSequenceException) true;
    for_example
public normal_example
requires (* this is <a,b,c> and afterThisOne is 1 and item is d *);
ensures (* \result is <a,b,d,c> *);
       also
public normal_example
requires (* this is <a,b,c> and afterThisOne is -1 and item is d *);
ensures (* \result is <d,a,b,c> *);

insertBeforeIndex

public JMLValueSequence insertBeforeIndex(\bigint beforeThisOne,
                                          JMLType item)
                                   throws JMLSequenceException,
                                          IllegalStateException
Return a sequence like this, but with item put immediately before the given index.

Parameters:
beforeThisOne - a zero-based index into the sequence, or the length of this.
item - the item to put before index beforeThisOne
Returns:
if the index is in range
Throws:
JMLSequenceException - if the index is out of range.
IllegalStateException
See Also:
insertAfterIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= beforeThisOne&&beforeThisOne <= this.length;
requires this.length < 2147483647;
ensures \result .equals(this.prefix(beforeThisOne).concat(new org.jmlspecs.models.JMLValueSequence(item)).concat(this.removePrefix(beforeThisOne)));
     also
public exceptional_behavior
requires !(0 <= beforeThisOne&&beforeThisOne <= this.length);
signals (org.jmlspecs.models.JMLSequenceException) true;

subsequence

public JMLValueSequence subsequence(\bigint from,
                                    \bigint to)
                             throws JMLSequenceException
Returns a subsequence of this containing the elements beginning with index from (inclusive) and ending with index to (exclusive).

Parameters:
from - the inclusive, zero-based element of the first element in the subsequence.
to - the zero-based element of the first element that should not be in the subsequence.
Throws:
JMLSequenceException - if (from < 0 or from > to or to > length of this.
See Also:
prefix(int), removePrefix(int), header(), trailer(), concat(org.jmlspecs.models.JMLValueSequence)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= from&&from <= to&&to <= this.length();
ensures \result .equals(this.removePrefix(from).prefix((int)(to-from)));
ensures_redundantly (* \result contains the elements of this beginning with index from (inclusive) and ending with index to (exclusive) *)&&\result .length() == to-from;
     also
public exceptional_behavior
requires !(0 <= from&&from <= to&&to <= this.length());
signals (org.jmlspecs.models.JMLSequenceException) true;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and from is 1 and to is 3 *);
ensures (* \result is <b,c> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and from is 0 and to is 3 *);
ensures (* \result is <a,b,c> *);
       also
public normal_example
requires from == to;
ensures \result .isEmpty();

bigintToBigInteger

public static BigInteger bigintToBigInteger(\bigint biValue)
Specifications: pure

bigIntegerToBigint

public static \bigint bigIntegerToBigint(BigInteger oBi)
Specifications: pure
public normal_behavior
requires oBi.equals(java.math.BigInteger.ZERO);
ensures \result == 0;
Method Detail

singleton

public static JMLValueSequence singleton(JMLType e)
Return the singleton sequence containing the given element.

See Also:
JMLValueSequence(JMLType)
Specifications: pure non_null
public normal_behavior
assignable \nothing;
ensures \result != null&&\result .equals(new org.jmlspecs.models.JMLValueSequence(e));

convertFrom

public static JMLValueSequence convertFrom(non_null JMLType[] a)
Return the sequence containing all the elements in the given array in the same order as the elements appear in the array.

Specifications: pure non_null
public normal_behavior
requires a != null;
assignable \nothing;
ensures \result != null&&\result .size() == a.length&&( \forall int i; 0 <= i&&i < a.length; (\result .itemAt(i) == null ? a[i] == null : \result .itemAt(i).equals(a[i])));

convertFrom

public static JMLValueSequence convertFrom(non_null JMLType[] a,
                                           int size)
Return the sequence containing the first 'size' elements in the given array in the same order as the elements appear in the array.

Specifications: pure non_null
public normal_behavior
requires a != null&&0 <= size&&size < a.length;
assignable \nothing;
ensures \result != null&&\result .size() == size&&( \forall int i; 0 <= i&&i < size; (\result .itemAt(i) == null ? a[i] == null : \result .itemAt(i).equals(a[i])));
    implies_that
requires size < a.length;

convertFrom

public static JMLValueSequence convertFrom(non_null Collection c)
                                    throws ClassCastException
Return the sequence containing all the value in the given collection in the same order as the elements appear in the collection.

Throws:
ClassCastException - if some element in c is not an instance of JMLType.
See Also:
containsAll(java.util.Collection)
Specifications: pure non_null
public normal_behavior
requires c != null&&c.elementType <: \type(org.jmlspecs.models.JMLType);
requires c.size() < 2147483647;
assignable \nothing;
ensures \result != null&&\result .size() == c.size()&&( \forall org.jmlspecs.models.JMLType x; ; c.contains(x) <==> \result .has(x))&&(* the elements in \result are in the same order as c *);
     also
public exceptional_behavior
requires c != null&&( \exists java.lang.Object o; c.contains(o); !(o instanceof org.jmlspecs.models.JMLType));
assignable \nothing;
signals_only java.lang.ClassCastException;

convertFrom

public static JMLValueSequence convertFrom(non_null JMLCollection c)
                                    throws ClassCastException
Return the sequence containing all the value in the given JMLCollection in the same order as the elements appear in the collection.

Throws:
ClassCastException - if some element in c is not an instance of JMLType.
Specifications: pure non_null
public normal_behavior
requires c != null&&c.elementType <: \type(org.jmlspecs.models.JMLType);
requires c.size() < 2147483647;
assignable \nothing;
ensures \result != null&&( \forall org.jmlspecs.models.JMLType x; ; c.has(x) <==> \result .has(x))&&(* the elements in \result are in the same order as c *);
ensures_redundantly \result .size() == c.size();
     also
public exceptional_behavior
requires c != null&&( \exists java.lang.Object o; c.has(o); !(o instanceof org.jmlspecs.models.JMLType));
assignable \nothing;
signals_only java.lang.ClassCastException;

itemAt

public JMLType itemAt(int i)
               throws JMLSequenceException
Return the element at the given zero-based index.

Parameters:
i - the zero-based index into the sequence.
Throws:
JMLSequenceException - if the index i is out of range.
See Also:
get(int), has(JMLType), count(JMLType), #itemAt(\bigint)
Specifications: (class)pure
     also
public normal_behavior
requires 0 <= i&&i < this.int_size();
ensures (* \result == null, if the ith element of this is null; otherwise, \result ".equals" the ith element of this *);
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;
     also
public exceptional_behavior
requires !(0 <= i&&i < this.int_size());
signals_only org.jmlspecs.models.JMLSequenceException;
    for_example
public normal_example
requires (* this is <w,x,y,z> and i is 0 *);
ensures (* \result is w.clone() *);
       also
public normal_example
requires (* this is <w,x,y,z> and i is 3 *);
ensures (* \result is z.clone() *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       nullable (class)pure

get

public JMLType get(int i)
            throws IndexOutOfBoundsException
Return the element at the given zero-based index; a synonym for itemAt(int).

Parameters:
i - the zero-based index into the sequence.
Throws:
IndexOutOfBoundsException - if the index i is out of range.
See Also:
itemAt(int)
Specifications: (class)pure
public normal_behavior
requires 0 <= i&&i < this.length;
ensures (* \result == null, if the ith element of this is null; otherwise, \result ".equals" the ith element of this *);
     also
public exceptional_behavior
requires !(0 <= i&&i < this.length);
signals_only java.lang.IndexOutOfBoundsException;
    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 sequence; a synonym for #length.

Specified by:
int_size in interface JMLCollection
See Also:
#length(), isEmpty()
Specifications: (class)pure
     also
protected normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();
    for_example
public normal_example
requires (* this is <a,b,c,d> *);
ensures \result == 4;
       also
public normal_example
requires (* this is <> *);
ensures \result == 0;
Specifications inherited from overridden method in interface JMLCollection:
       pure
public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();

int_length

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

See Also:
int_size()
Specifications: (class)pure
     also
public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       (class)pure
public normal_behavior
ensures \result >= 0;

count

public int count(JMLType item)
Tells the number of times a given element occurs in the sequence.

See Also:
has(JMLType), itemAt(int)
Specifications: (class)pure
     also
public normal_behavior
requires item != null;
ensures \result == ( \num_of int i; 0 <= i&&i < this.int_length(); this.itemAt(i) != null&&this.itemAt(i).equals(item));
     also
public normal_behavior
requires item == null;
ensures \result == ( \num_of int i; 0 <= i&&i < this.int_length(); this.itemAt(i) == null);
    for_example
public normal_example
requires (* this is <a,b,c,d,c> and item is c *);
ensures \result == 2;
       also
public normal_example
requires (* this is <a,b,c,d,a> and item is q *);
ensures \result == 0;
Specifications inherited from overridden method count(JMLType elem) in class JMLValueSequenceSpecs:
       (class)pure
public normal_behavior
ensures \result >= 0&&(* \result is the number of times elem tests as ".equals" to one of the objects in this sequence *);

has

public boolean has(JMLType elem)
Tells whether the given element is ".equals" to an element in the sequence.

See Also:
count(JMLType)
Specifications: (class)pure
     also
public normal_behavior
{|
requires elem != null;
ensures \result <==> ( \exists int i; 0 <= i&&i < this.int_length(); this.itemAt(i).equals(elem));
also
requires elem == null;
ensures \result <==> ( \exists int i; 0 <= i&&i < this.int_length(); this.itemAt(i) == null);
|}
    for_example
public normal_example
requires (* this is <w,x,y,z> and elem is x *);
ensures (* \result is true *);
       also
public normal_example
requires this.isEmpty();
ensures !\result ;
Specifications inherited from overridden method has(JMLType elem) in class JMLValueSequenceSpecs:
       (class)pure
public normal_behavior
ensures \result <==> (* elem is ".equals" to one of the objects in this sequence *);
Specifications inherited from overridden method has(Object elem) in interface JMLCollection:
       pure
public normal_behavior
ensures (* \result <==> elem is equal to one of the elements in the collection. *);
ensures_redundantly !this.containsNull&&elem == null ==> !\result ;
ensures_redundantly elem != null&&!(\typeof(elem) <: this.elementType) ==> !\result ;

containsAll

public boolean containsAll(non_null Collection c)
Tell whether, for each element in the given collection, there is a ".equals" element in this sequence.

Parameters:
c - the collection whose elements are sought.
Specifications: (class)pure
public normal_behavior
requires c != null;
ensures \result <==> ( \forall java.lang.Object o; c.contains(o); this.has(o));

isPrefix

public boolean isPrefix(non_null JMLValueSequence s2)
Tells whether the elements of the this sequence occur, in order, at the beginning of the given sequence, using ".equals" for comparisons.

See Also:
isProperPrefix(org.jmlspecs.models.JMLValueSequence), isSuffix(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.int_length() <= s2.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); (s2.itemAt(i) != null&&s2.itemAt(i).equals(this.itemAt(i)))||(s2.itemAt(i) == null&&this.itemAt(i) == null));
    for_example
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c,d> and s2 is <a,b,c> *);
ensures (* \result is false *);

isProperPrefix

public boolean isProperPrefix(non_null JMLValueSequence s2)
Tells whether this sequence is shorter than the given sequence, and also if the elements of this sequence occur, in order, at the beginning of the given sequence, using ".equals" for comparisons.

See Also:
isPrefix(org.jmlspecs.models.JMLValueSequence), isProperSuffix(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.isPrefix(s2)&&!this.equals(s2);
    for_example
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c> *);
ensures (* \result is false *);

isSuffix

public boolean isSuffix(non_null JMLValueSequence s2)
Tells whether the elements of this sequence occur, in order, at the end of the given sequence, using ".equals" for comparisons.

See Also:
isProperSuffix(org.jmlspecs.models.JMLValueSequence), isPrefix(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.int_length() <= s2.int_length()&&this.equals(s2.removePrefix(s2.int_length()-this.int_length()));
    for_example
public normal_example
requires (* this is <b,c,d> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c,d> *);
ensures (* \result is false *);
       also
public normal_example
requires (* this is <> and s2 is <a,b,c,d> *);
ensures (* \result is true *);

isProperSuffix

public boolean isProperSuffix(non_null JMLValueSequence s2)
Tells whether the this sequence is shorter than the given object, and also if the elements of this sequence occur, in order, at the end of the given sequence, using ".equals" for comparisons.

See Also:
isSuffix(org.jmlspecs.models.JMLValueSequence), isProperPrefix(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.isSuffix(s2)&&!this.equals(s2);

equals

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

Specified by:
equals in interface JMLType
Overrides:
equals in class Object
See Also:
isSuffix(org.jmlspecs.models.JMLValueSequence), int_size()
Specifications: pure
     also
public normal_behavior
requires obj != null&&obj instanceof org.jmlspecs.models.JMLValueSequence;
ensures \result <==> this.isPrefix((org.jmlspecs.models.JMLValueSequence)obj)&&((org.jmlspecs.models.JMLValueSequence)obj).isPrefix(this);
ensures_redundantly \result ==> this.containsNull == ((org.jmlspecs.models.JMLValueSequence)obj).containsNull;
     also
public normal_behavior
requires obj == null||!(obj instanceof org.jmlspecs.models.JMLValueSequence);
ensures !\result ;
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;
|}
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) *);

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

isEmpty

public boolean isEmpty()
Tells whether this sequence is empty.

See Also:
int_size(), int_length()
Specifications: pure
public normal_behavior
ensures \result == (this.int_length() == 0);

indexOf

public int indexOf(JMLType item)
            throws JMLSequenceException
Return the zero-based index of the first occurrence of the given element in the sequence, if there is one

Parameters:
item - the JMLType sought in this.
Returns:
the first index at which item occurs.
Throws:
JMLSequenceException - if item is not a member of the sequence.
See Also:
itemAt(int)
Specifications: (class)pure
public normal_behavior
requires this.has(item);
{|
requires item != null;
ensures this.itemAt(\result ).equals(item)&&( \forall int i; 0 <= i&&i < \result ; !(this.itemAt(i).equals(item)));
ensures_redundantly (* \result is the first index at which item occurs in this *);
also
requires item == null;
ensures this.itemAt(\result ) == null&&( \forall int i; 0 <= i&&i < \result ; this.itemAt(i) != null);
|}
     also
public exceptional_behavior
requires !this.has(item);
signals_only org.jmlspecs.models.JMLSequenceException;
    for_example
public normal_example
requires (* this is <w,x,y,z,x> and item is x *);
ensures (* \result is 1 *);

first

public JMLType first()
              throws JMLSequenceException
Return the first element in this sequence.

Throws:
JMLSequenceException - if the sequence is empty.
See Also:
itemAt(int), last(), trailer(), header()
Specifications: pure
     also
public normal_behavior
requires this.int_length() > 0;
{|
requires this.itemAt(0) != null;
ensures \result .equals(this.itemAt(0));
also
requires this.itemAt(0) == null;
ensures \result == null;
|}
     also
public exceptional_behavior
requires this.int_length() == 0;
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
public normal_behavior
requires this.int_length() > 0;
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;
    for_example
public normal_example
requires (* this is <b,c,d> *);
ensures (* \result is b.clone() *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       nullable (class)pure

last

public JMLType last()
             throws JMLSequenceException
Return the last element in this sequence.

Throws:
JMLSequenceException - if the sequence is empty.
See Also:
itemAt(int), first(), header(), trailer()
Specifications: (class)pure
     also
public normal_behavior
requires this.int_length() >= 1;
{|
requires this.itemAt((int)(this.int_length()-1)) != null;
ensures \result .equals(this.itemAt((int)(this.int_length()-1)));
also
requires this.itemAt((int)(this.int_length()-1)) == null;
ensures \result == null;
|}
     also
public exceptional_behavior
requires this.int_length() == 0;
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
public normal_behavior
requires this.int_length() >= 1;
ensures \result != null ==> \typeof(\result ) <: this.elementType;
ensures !this.containsNull ==> \result != null;
    for_example
public normal_example
requires (* this is <b,c,d> *);
ensures (* \result is d.clone() *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       nullable (class)pure

isSubsequence

public boolean isSubsequence(non_null JMLValueSequence s2)
Tells whether this sequence is a subsequence of the given sequence.

Parameters:
s2 - the sequence to search for within this sequence.
Returns:
whether the elements of this occur (in order) within s2.
See Also:
isProperSubsequence(org.jmlspecs.models.JMLValueSequence), isSupersequence(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.int_length() <= s2.int_length()&&( \exists int i; 0 <= i&&i < s2.int_length()-this.int_length()+1; this.isPrefix(s2.removePrefix(i)));
    for_example
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c,d> and s2 is <a,b,c> *);
ensures (* \result is false *);

isProperSubsequence

public boolean isProperSubsequence(non_null JMLValueSequence s2)
Tells whether this sequence is strictly shorter than the given sequence and a subsequence of it.

Parameters:
s2 - the sequence to search for within this sequence.
Returns:
whether the elements of s2 occur (in order) within this.
See Also:
isSubsequence(org.jmlspecs.models.JMLValueSequence), isProperSupersequence(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> this.isSubsequence(s2)&&!this.equals(s2);
    for_example
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c,d> *);
ensures (* \result is true *);
       also
public normal_example
requires (* this is <a,b,c> and s2 is <a,b,c> *);
ensures (* \result is false *);
       also
public normal_example
requires (* this is <> and s2 is <a,b,c,d> *);
ensures (* \result is false *);

isSupersequence

public boolean isSupersequence(non_null JMLValueSequence s2)
Tells whether the given sequence is a supersequence of this sequence.

Parameters:
s2 - the sequence to search within for this sequence.
Returns:
whether the elements of this occur (in order) within s2.
See Also:
isProperSubsequence(org.jmlspecs.models.JMLValueSequence), isSubsequence(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> s2.isSubsequence(this);

isProperSupersequence

public boolean isProperSupersequence(non_null JMLValueSequence s2)
Tells whether the given sequence is both longer than and a supersequence of this sequence.

Parameters:
s2 - the sequence to search within for this sequence.
Returns:
whether the elements of this occur (in order) within s2.
See Also:
isSupersequence(org.jmlspecs.models.JMLValueSequence), isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> s2.isProperSubsequence(this);

isInsertionInto

public boolean isInsertionInto(non_null JMLValueSequence s2,
                               JMLType elem)
Tells whether this sequence is the result of inserting the given element once into the given sequence. That is, this sequence is exactly one element longer than the given sequence, and its elements are in the same order, except for the insertion of the given element.

Parameters:
s2 - the shorter sequence, which we see if the elem is inserted into
elem - the given element
Returns:
whether the elements of s2 occur in order in this sequence, with the insertion of elem somewhere.
See Also:
isDeletionFrom(org.jmlspecs.models.JMLValueSequence, org.jmlspecs.models.JMLType), isProperSupersequence(org.jmlspecs.models.JMLValueSequence), isProperSubsequence(org.jmlspecs.models.JMLValueSequence), subsequence(int, int)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists int i; 0 <= i&&i < this.int_length(); this.itemAt(i).equals(elem)&&this.subsequence(0,i).concat(this.subsequence((int)(i+1),this.int_length())).equals(s2));
ensures_redundantly \result ==> this.int_length() == s2.int_length()+1;
ensures_redundantly \result ==> this.has(elem);
ensures_redundantly \result <==> s2.isDeletionFrom(this,elem);

isDeletionFrom

public boolean isDeletionFrom(non_null JMLValueSequence s2,
                              JMLType elem)
Tells whether this sequence is the result of deleting the given element once from the given sequence. That is, this sequence is exactly one element shorter than the given sequence, and its elements are in the same order, except for the deletion of the given element from the given sequence.

Parameters:
s2 - the longer sequence, in which we see if the elem is deleted from
elem - the given element
Returns:
whether the elements of s2 occur in order in this sequence, with the deletion of elem somewhere.
See Also:
isInsertionInto(org.jmlspecs.models.JMLValueSequence, org.jmlspecs.models.JMLType), isProperSupersequence(org.jmlspecs.models.JMLValueSequence), isProperSubsequence(org.jmlspecs.models.JMLValueSequence), subsequence(int, int)
Specifications: (class)pure
public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists int i; 0 <= i&&i < s2.int_length(); s2.itemAt(i).equals(elem)&&this.equals(s2.removeItemAt(i)));
ensures_redundantly \result ==> this.int_length()+1 == s2.int_length();
ensures_redundantly \result ==> s2.has(elem);
ensures_redundantly \result <==> s2.isInsertionInto(this,elem);

clone

public Object clone()
Return a clone of this object. This method clones the elements of the sequence.

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

prefix

public JMLValueSequence prefix(int n)
                        throws JMLSequenceException
Return a sequence containing the first n elements in this sequence.

Parameters:
n - the number of elements in the result.
Throws:
JMLSequenceException - if n is negative or greater than the length of the sequence.
See Also:
trailer(), removePrefix(int), subsequence(int, int)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= n&&n <= this.length;
ensures \result .length == n&&( \forall int i; 0 <= i&&i < n; (\result .itemAt(i) != null ==> \result .itemAt(i).equals(this.itemAt(i)))||(\result .itemAt(i) == null ==> this.itemAt(i) == null));
ensures_redundantly (* \result is the same as this, but with the last length-n items removed *);
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.length);
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !this.containsNull ==> !\result .containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and n is 0 *);
ensures (* \result is <> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 3 *);
ensures (* \result is <a,b,c> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 5 *);
ensures (* \result is <a,b,c,d,e> *);
       also
public normal_example
requires n == this.length;
ensures \result .equals(this);

removePrefix

public JMLValueSequence removePrefix(int n)
                              throws JMLSequenceException
Return a sequence containing all but the first n elements in this.

Parameters:
n - the number of elements to remove
Throws:
JMLSequenceException - if n is negative or greater than the length of the sequence.
See Also:
header(), prefix(int), subsequence(int, int)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= n&&n <= this.length;
ensures \result .length == this.length-n&&( \forall \bigint i; n <= i&&i < this.length; (\result .itemAt((int)(i-n)) != null&&\result .itemAt((int)(i-n)).equals(this.itemAt(i)))||(\result .itemAt((int)(i-n)) == null&&this.itemAt(i) == null));
ensures_redundantly (* \result is the same as this, but with the first n items removed *);
     also
public exceptional_behavior
requires !(0 <= n&&n <= this.length);
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !this.containsNull ==> !\result .containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and n is 1 *);
ensures (* \result is <b,c,d,e> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and n is 5 *);
ensures (* \result is <> *);
       also
public normal_example
requires n == this.length;
ensures \result .isEmpty();

concat

public JMLValueSequence concat(non_null JMLValueSequence s2)
Return a sequence that is the concatenation of this with the given sequence.

Parameters:
s2 - the sequence to place at the end of this sequence in the result.
Returns:
the concatenation of this sequence and s2.
Specifications: non_null (class)pure
public normal_behavior
requires s2 != null;
ensures \result .int_length() == this.int_length()+s2.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); (\result .itemAt(i) != null&&\result .itemAt(i).equals(this.itemAt(i)))||(\result .itemAt(i) == null&&this.itemAt(i) == null))&&( \forall int i; 0 <= i&&i < s2.int_length(); (\result .itemAt((int)(this.int_length()+i)) != null&&\result .itemAt((int)(this.int_length()+i)).equals(s2.itemAt(i)))||(\result .itemAt((int)(this.int_length()+i)) == null&&s2.itemAt(i) == null));
ensures_redundantly (* \result is the concatenation of this followed by s2 *);
    implies_that
ensures this.containsNull||s2.containsNull <==> \result .containsNull;
    for_example
public normal_example
requires (* this is <a,b> and s2 is <c,d,e> *);
ensures (* \result is <a,b,c,d,e> *);

reverse

public JMLValueSequence reverse()
Return a sequence that is the reverse of this sequence.

Returns:
the reverse of this sequence.
Specifications: non_null (class)pure
public normal_behavior
old int len = this.int_length();
ensures \result .int_length() == len&&( \forall int i; 0 <= i&&i < len; (\result .itemAt((int)(len-i-1)) != null&&\result .itemAt((int)(len-i-1)).equals(this.itemAt(i)))||(\result .itemAt((int)(len-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;

removeItemAt

public JMLValueSequence removeItemAt(int index)
                              throws JMLSequenceException
Return a sequence like this, but without the element at the given zero-based index.

Parameters:
index - the zero-based index into the sequence.
Throws:
JMLSequenceException - if the index is out of range.
See Also:
itemAt(int), removeItemAt(int), prefix(int), removePrefix(int), subsequence(int, int), concat(org.jmlspecs.models.JMLValueSequence)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= index&&index < this.int_length();
ensures \result .equals(this.prefix(index).concat(this.removePrefix((int)(index+1))));
ensures_redundantly (* \result is the same as this, but with the item at position index removed *);
     also
public exceptional_behavior
requires !(0 <= index&&index < this.int_length());
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and index is 1 *);
ensures (* \result is <a,c,d,e> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and index is 4 *);
ensures (* \result is <a,b,c,d> *);

replaceItemAt

public JMLValueSequence replaceItemAt(int index,
                                      JMLType item)
                               throws JMLSequenceException
Return a sequence like this, but with item replacing the element at the given zero-based index.

Parameters:
index - the zero-based index into the sequence.
item - the item to put at index index
Throws:
JMLSequenceException - if the index is out of range.
See Also:
itemAt(int), replaceItemAt(int, org.jmlspecs.models.JMLType)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= index&&index < this.int_length();
ensures \result .equals(this.removeItemAt(index).insertBeforeIndex(index,item));
ensures_redundantly (* \result is the same as this, but with item replacing the one at position index *);
     also
public exceptional_behavior
requires !(0 <= index&&index < this.int_length());
signals_only org.jmlspecs.models.JMLSequenceException;
    implies_that
ensures item != null ==> \typeof(item) <: \result .elementType;
ensures !\result .containsNull <== !this.containsNull&&item != null;
    for_example
public normal_example
requires (* this is <a,b,c,d,e>, item is x and index is 1 *);
ensures (* \result is <a,x,c,d,e> *);

header

public JMLValueSequence header()
                        throws JMLSequenceException
Return a sequence containing all but the last element in this.

Throws:
JMLSequenceException - if this is empty.
See Also:
prefix(int), first(), last(), trailer(), subsequence(int, int)
Specifications: non_null (class)pure
public normal_behavior
requires this.int_length() >= 1;
ensures \result .equals(this.removeItemAt((int)(this.int_length()-1)));
ensures_redundantly \result .int_length() == this.int_length()-1&&(* \result is like this, but without the last item *);
     also
public exceptional_behavior
requires this.int_length() == 0;
signals (org.jmlspecs.models.JMLSequenceException) true;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d> *);
ensures (* \result is <a,b,c> *);

trailer

public JMLValueSequence trailer()
                         throws JMLSequenceException
Return a sequence containing all but the first element in this.

Throws:
JMLSequenceException - if this is empty.
See Also:
removePrefix(int), last(), first(), header(), subsequence(int, int)
Specifications: pure non_null
public normal_behavior
requires this.int_length() >= 1;
ensures \result .equals(this.removePrefix(1));
ensures_redundantly \result .int_length() == this.int_length()-1&&(* \result is like this, but without the first item *);
     also
public exceptional_behavior
requires this.int_length() == 0;
signals (org.jmlspecs.models.JMLSequenceException) true;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d> *);
ensures (* \result is <b,c,d> *);

insertAfterIndex

public JMLValueSequence insertAfterIndex(int afterThisOne,
                                         JMLType item)
                                  throws JMLSequenceException,
                                         IllegalStateException
Return a sequence like this, but with item put immediately after the given index.

Parameters:
afterThisOne - a zero-based index into the sequence, or -1.
item - the item to put after index afterThisOne
Returns:
if the index is in range
Throws:
JMLSequenceException - if the index is out of range.
IllegalStateException
See Also:
insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)
Specifications: non_null (class)pure
     also
public normal_behavior
requires -1 <= afterThisOne&&afterThisOne < this.length;
requires this.length < 2147483647;
ensures \result .equals(this.insertBeforeIndex((int)(afterThisOne+1),item));
ensures_redundantly (* \result is the same sequence as this, but with item inserted after the index "afterThisOne" *);
     also
public exceptional_behavior
requires !(-1 <= afterThisOne&&afterThisOne < this.length);
signals (org.jmlspecs.models.JMLSequenceException) true;
    for_example
public normal_example
requires (* this is <a,b,c> and afterThisOne is 1 and item is d *);
ensures (* \result is <a,b,d,c> *);
       also
public normal_example
requires (* this is <a,b,c> and afterThisOne is -1 and item is d *);
ensures (* \result is <d,a,b,c> *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       non_null (class)pure

insertBeforeIndex

public JMLValueSequence insertBeforeIndex(int beforeThisOne,
                                          JMLType item)
                                   throws JMLSequenceException,
                                          IllegalStateException
Return a sequence like this, but with item put immediately before the given index.

Parameters:
beforeThisOne - a zero-based index into the sequence, or the length of this.
item - the item to put before index beforeThisOne
Returns:
if the index is in range
Throws:
JMLSequenceException - if the index is out of range.
IllegalStateException
See Also:
insertAfterIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)
Specifications: non_null (class)pure
     also
public normal_behavior
requires 0 <= beforeThisOne&&beforeThisOne <= this.length;
requires this.length < 2147483647;
ensures \result .equals(this.prefix(beforeThisOne).concat(new org.jmlspecs.models.JMLValueSequence(item)).concat(this.removePrefix(beforeThisOne)));
     also
public exceptional_behavior
requires !(0 <= beforeThisOne&&beforeThisOne <= this.length);
signals (org.jmlspecs.models.JMLSequenceException) true;
     also
public model_program { ... }
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       non_null (class)pure

insertBack

public JMLValueSequence insertBack(JMLType item)
                            throws IllegalStateException
Return a sequence like this, but with the given item put an the end.

Parameters:
item - the item to put at the end of the result.
Returns:
a sequence the elements of this sequence followed by item.
Throws:
IllegalStateException
See Also:
insertAfterIndex(int, org.jmlspecs.models.JMLType), insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), removeItemAt(int), header(), last()
Specifications: non_null (class)pure
     also
public normal_behavior
requires this.int_length() < 2147483647;
ensures \result .equals(this.insertBeforeIndex(this.int_length(),item));
ensures_redundantly \result .int_length() == this.int_length()+1&&this.isProperPrefix(\result );
ensures_redundantly (* \result is the same sequence as this, but with item.clone() inserted at the back, after index int_length() - 1 *);
    for_example
public normal_example
requires (* this is <a,b,c> and item is d *);
ensures (* \result is <a,b,c,d> *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       non_null (class)pure

insertFront

public JMLValueSequence insertFront(JMLType item)
                             throws IllegalStateException
Return a sequence like this, but with the given item put an the front.

Parameters:
item - the item to put at the front of the result.
Returns:
a sequence with item followed by the elements of this sequence.
Throws:
IllegalStateException
See Also:
insertAfterIndex(int, org.jmlspecs.models.JMLType), insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int), trailer(), first()
Specifications: pure non_null
     also
public normal_behavior
requires this.int_length() < 2147483647;
ensures \result .equals(this.insertBeforeIndex(0,item));
ensures_redundantly \result .int_length() == this.int_length()+1&&\result .trailer().equals(this);
ensures_redundantly (* \result is the same sequence as this, but with item.clone() inserted at the front, before index 0 *);
    for_example
public normal_example
requires (* this is <a,b,c> and item is d *);
ensures (* \result is <d,a,b,c> *);
Specifications inherited from overridden method in class JMLValueSequenceSpecs:
       non_null (class)pure

subsequence

public JMLValueSequence subsequence(int from,
                                    int to)
                             throws JMLSequenceException
Returns a subsequence of this containing the elements beginning with index from (inclusive) and ending with index to (exclusive).

Parameters:
from - the inclusive, zero-based element of the first element in the subsequence.
to - the zero-based element of the first element that should not be in the subsequence.
Throws:
JMLSequenceException - if (from < 0 or from > to or to > length of this.
See Also:
prefix(int), removePrefix(int), header(), trailer(), concat(org.jmlspecs.models.JMLValueSequence)
Specifications: non_null (class)pure
public normal_behavior
requires 0 <= from&&from <= to&&to <= this.int_length();
ensures \result .equals(this.removePrefix(from).prefix((int)(to-from)));
ensures_redundantly (* \result contains the elements of this beginning with index from (inclusive) and ending with index to (exclusive) *)&&\result .int_length() == to-from;
     also
public exceptional_behavior
requires !(0 <= from&&from <= to&&to <= this.int_length());
signals (org.jmlspecs.models.JMLSequenceException) true;
    implies_that
ensures !\result .containsNull <== !this.containsNull;
    for_example
public normal_example
requires (* this is <a,b,c,d,e> and from is 1 and to is 3 *);
ensures (* \result is <b,c> *);
       also
public normal_example
requires (* this is <a,b,c,d,e> and from is 0 and to is 3 *);
ensures (* \result is <a,b,c> *);
       also
public normal_example
requires from == to;
ensures \result .isEmpty();

toBag

public JMLValueBag toBag()
Return a new JMLValueBag containing all the elements of this.

See Also:
toSet(), toArray()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall int i; 0 <= i&&i < this.int_length(); \result .count(this.itemAt(i)) == this.count(this.itemAt(i)));

toSet

public JMLValueSet toSet()
Return a new JMLValueSet containing all the elements of this.

See Also:
toBag(), toArray()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&( \forall org.jmlspecs.models.JMLType o; ; \result .has(o) == this.has(o));

toArray

public JMLType[] toArray()
Return a new array containing all the elements of this in order.

See Also:
toSet(), toBag()
Specifications: non_null (class)pure
public normal_behavior
ensures \result != null&&\result .length == this.int_length()&&( \forall int i; 0 <= i&&i < this.int_length(); (\result [i] == null ==> this.itemAt(i) == null)&&(\result [i] != null ==> \result [i].equals(this.itemAt(i))));

elements

public JMLValueSequenceEnumerator elements()
Return a enumerator for this.

See Also:
iterator(), #itemAt()
Specifications: non_null (class)pure
public normal_behavior
ensures \fresh(\result )&&(* \result is an enumerator for this *);

iterator

public JMLIterator iterator()
Returns an iterator over this sequence.

Specified by:
iterator in interface JMLCollection
See Also:
elements()
Specifications: non_null (class)pure
     also
public normal_behavior
ensures \fresh(\result )&&\result .equals(new org.jmlspecs.models.JMLEnumerationToIterator(this.elements()));
Specifications inherited from overridden method in interface JMLCollection:
       pure non_null
public normal_behavior
ensures \fresh(\result )&&\result .elementType == this.elementType;
ensures !this.containsNull ==> !\result .returnsNull;

toString

public String toString()
Return a string representation of this object.

Overrides:
toString in class Object
Specifications: non_null (class)pure
     also
public normal_behavior
ensures (* \result is a string representation of this *);
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.