org.jmlspecs.models
Class JMLValueSequence

java.lang.Object
  org.jmlspecs.models.JMLValueSequenceSpecs
      org.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.80 $

Author:

Gary T. Leavens, Albert L. Baker

See Also:

JMLCollection, JMLType, JMLObjectSequence, JMLValueSequenceEnumerator, JMLValueSequenceSpecs

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           An equational specification of the properties of sequences.
private static String	TOO_BIG_TO_INSERT

 

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.

 

Method Summary
Object	clone()           Return a clone of this object.
JMLValueSequence	concat(JMLValueSequence s2)           Return a sequence that is the concatenation of this with the given sequence.
boolean	containsAll(Collection c)           Tell whether, for each element in the given collection, there is a ".equals" element in this sequence.
static JMLValueSequence	convertFrom(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(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(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(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(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(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(JMLValueSequence s2, JMLType elem)           Tells whether this sequence is the result of inserting the given element once into the given sequence.
boolean	isPrefix(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(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(JMLValueSequence s2)           Tells whether this sequence is strictly shorter than the given sequence and a subsequence of it.
boolean	isProperSuffix(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(JMLValueSequence s2)           Tells whether the given sequence is both longer than and a supersequence of this sequence.
boolean	isSubsequence(JMLValueSequence s2)           Tells whether this sequence is a subsequence of the given sequence.
boolean	isSuffix(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(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

 

Field Detail

theSeq

protected final JMLListValueNode theSeq

An equational specification of the properties of sequences. The list representing this sequence's elements, in order.

_length

protected final BigInteger _length

This sequence's length.

EMPTY

public static final JMLValueSequence EMPTY

The empty JMLValueSequence.

See Also:

JMLValueSequence()

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

JMLValueSequence

public JMLValueSequence()

Initialize this to be the empty sequence.

See Also:

EMPTY

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)

JMLValueSequence

protected JMLValueSequence(JMLListValueNode ls,
                           int len)

Initialize this sequence based on the given representation. Initialize this sequence based on the given representation.

singleton

public static JMLValueSequence singleton(JMLType e)

Return the singleton sequence containing the given element.

See Also:

JMLValueSequence(JMLType)

convertFrom

public static JMLValueSequence convertFrom(JMLType[] a)

Return the sequence containing all the elements in the given array in the same order as the elements appear in the array.

convertFrom

public static JMLValueSequence convertFrom(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.

convertFrom

public static JMLValueSequence convertFrom(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)

convertFrom

public static JMLValueSequence convertFrom(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.

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 oBiI is out of range.

JMLSequenceException - if the index i is out of range.

See Also:

get(int), has(JMLType), Return the element at the given zero-based index., get(int), has(JMLType), count(JMLType), #itemAt(\bigint)

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.

IndexOutOfBoundsException - if the index i is out of range.

See Also:

Return the element at the given zero-based index; a synonym for {@link #itemAt}., itemAt(int)

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(), Tells the number of elements in the sequence; a synonym for {@link #length}., #size(), Tells the number of elements in the sequence; a synonym for {@link #length}., #length(), isEmpty()

int_length

public int int_length()

Tells the number of elements in the sequence; a synonym for #size.

See Also:

int_size()

count

public int count(JMLType item)

Tells the number of times a given element occurs in the sequence.

See Also:

has(JMLType), Tells the number of times a given element occurs in the sequence., has(JMLType), itemAt(int)

has

public boolean has(JMLType elem)

Tells whether the given element is ".equals" to an element in the sequence.

See Also:

count(JMLType)

containsAll

public boolean containsAll(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.

isPrefix

public boolean isPrefix(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)

isProperPrefix

public boolean isProperPrefix(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)

isSuffix

public boolean isSuffix(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)

isProperSuffix

public boolean isProperSuffix(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)

equals

public boolean equals(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()

hashCode

public int hashCode()

Return a hash code for this object.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object

isEmpty

public boolean isEmpty()

Tells whether this sequence is empty.

See Also:

int_size(), int_length()

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.

JMLSequenceException - if item is not a member of the sequence.

See Also:

Return the zero-based index of the first occurrence of the given element in the sequence, if there is one, itemAt(int)

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

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

isSubsequence

public boolean isSubsequence(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)

isProperSubsequence

public boolean isProperSubsequence(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)

isSupersequence

public boolean isSupersequence(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)

isProperSupersequence

public boolean isProperSupersequence(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)

isInsertionInto

public boolean isInsertionInto(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)

isDeletionFrom

public boolean isDeletionFrom(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)

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

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.

JMLSequenceException - if n is negative or greater than the length of the sequence.

See Also:

trailer(), removePrefix(int), Return a sequence containing the first n elements in this sequence., trailer(), removePrefix(int), subsequence(int, int)

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.

JMLSequenceException - if n is negative or greater than the length of the sequence.

See Also:

header(), prefix(int), Return a sequence containing all but the first n elements in this., header(), prefix(int), subsequence(int, int)

concat

public JMLValueSequence concat(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.

reverse

public JMLValueSequence reverse()

Return a sequence that is the reverse of this sequence.

Returns:

the reverse of this sequence.

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.

JMLSequenceException - if the index is out of range.

See Also:

itemAt(int), removeItemAt(int), prefix(int), removePrefix(int), subsequence(int, int), Return a sequence like this, but without the element at the given zero-based index., itemAt(int), removeItemAt(int), prefix(int), removePrefix(int), subsequence(int, int), concat(org.jmlspecs.models.JMLValueSequence)

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.

JMLSequenceException - if the index is out of range.

See Also:

itemAt(int), Return a sequence like this, but with item replacing the element at the given zero-based index., itemAt(int), replaceItemAt(int, org.jmlspecs.models.JMLType)

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)

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)

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.

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), Return a sequence like this, but with item put immediately after the given index., insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)

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.

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), Return a sequence like this, but with item put immediately before the given index., insertAfterIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), removeItemAt(int)

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

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

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.

JMLSequenceException - if (from < 0 or from > to or to > length of this.

See Also:

prefix(int), removePrefix(int), header(), trailer(), Returns a subsequence of this containing the elements beginning with index from (inclusive) and ending with index to (exclusive)., prefix(int), removePrefix(int), header(), trailer(), concat(org.jmlspecs.models.JMLValueSequence)

toBag

public JMLValueBag toBag()

Return a new JMLValueBag containing all the elements of this.

See Also:

toSet(), toArray()

toSet

public JMLValueSet toSet()

Return a new JMLValueSet containing all the elements of this.

See Also:

toBag(), toArray()

toArray

public JMLType[] toArray()

Return a new array containing all the elements of this in order.

See Also:

toSet(), toBag()

elements

public JMLValueSequenceEnumerator elements()

Return a enumerator for this.

See Also:

iterator(), #itemAt()

iterator

public JMLIterator iterator()

Returns an iterator over this sequence.

Specified by:

iterator in interface JMLCollection

See Also:

elements()

toString

public String toString()

Return a string representation of this object.

Overrides:

toString in class Object