
JML  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object org.jmlspecs.models.JMLValueSequenceSpecs org.jmlspecs.models.JMLValueSequence
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.
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 zerobased 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 zerobased 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 zerobased 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 zerobased 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 zerobased 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 
protected final JMLListValueNode theSeq
protected final BigInteger _length
public static final JMLValueSequence EMPTY
JMLValueSequence()
private static final String ITEM_PREFIX
private static final String IS_NOT_FOUND
private static final String TOO_BIG_TO_INSERT
Constructor Detail 
public JMLValueSequence()
EMPTY
public JMLValueSequence(JMLType e)
e
 the element that is the first element in this sequence.singleton(org.jmlspecs.models.JMLType)
protected JMLValueSequence(JMLListValueNode ls, int len)
Method Detail 
public static JMLValueSequence singleton(JMLType e)
JMLValueSequence(JMLType)
public static JMLValueSequence convertFrom(JMLType[] a)
public static JMLValueSequence convertFrom(JMLType[] a, int size)
public static JMLValueSequence convertFrom(Collection c) throws ClassCastException
ClassCastException
 if some element in c is not an instance of
JMLType.containsAll(java.util.Collection)
public static JMLValueSequence convertFrom(JMLCollection c) throws ClassCastException
ClassCastException
 if some element in c is not an instance of
JMLType.public JMLType itemAt(int i) throws JMLSequenceException
i
 the zerobased index into the sequence.
JMLSequenceException
 if the index oBiI is out of range.
JMLSequenceException
 if the index i is out of range.get(int)
,
has(JMLType)
,
Return the element at the given zerobased index.
,
get(int)
,
has(JMLType)
,
count(JMLType)
,
#itemAt(\bigint)
public JMLType get(int i) throws IndexOutOfBoundsException
itemAt(int)
.
i
 the zerobased index into the sequence.
IndexOutOfBoundsException
 if the index i is out of range.
IndexOutOfBoundsException
 if the index i is out of range.Return the element at the given zerobased index; a synonym
for {@link #itemAt}.
,
itemAt(int)
public int int_size()
#length
.
int_size
in interface JMLCollection
#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()
public int int_length()
#size
.
int_size()
public int count(JMLType item)
has(JMLType)
,
Tells the number of times a given element occurs in the sequence.
,
has(JMLType)
,
itemAt(int)
public boolean has(JMLType elem)
count(JMLType)
public boolean containsAll(Collection c)
c
 the collection whose elements are sought.public boolean isPrefix(JMLValueSequence s2)
isProperPrefix(org.jmlspecs.models.JMLValueSequence)
,
isSuffix(org.jmlspecs.models.JMLValueSequence)
public boolean isProperPrefix(JMLValueSequence s2)
isPrefix(org.jmlspecs.models.JMLValueSequence)
,
isProperSuffix(org.jmlspecs.models.JMLValueSequence)
public boolean isSuffix(JMLValueSequence s2)
isProperSuffix(org.jmlspecs.models.JMLValueSequence)
,
isPrefix(org.jmlspecs.models.JMLValueSequence)
public boolean isProperSuffix(JMLValueSequence s2)
isSuffix(org.jmlspecs.models.JMLValueSequence)
,
isProperPrefix(org.jmlspecs.models.JMLValueSequence)
public boolean equals(Object obj)
equals
in interface JMLType
equals
in class Object
isSuffix(org.jmlspecs.models.JMLValueSequence)
,
int_size()
public int hashCode()
hashCode
in interface JMLType
hashCode
in class Object
public boolean isEmpty()
int_size()
,
int_length()
public int indexOf(JMLType item) throws JMLSequenceException
item
 the JMLType sought in this.
JMLSequenceException
 if item is not a member of the sequence.
JMLSequenceException
 if item is not a member of the sequence.Return the zerobased index of the first occurrence of the given
element in the sequence, if there is one
,
itemAt(int)
public JMLType first() throws JMLSequenceException
JMLSequenceException
 if the sequence is empty.itemAt(int)
,
last()
,
trailer()
,
header()
public JMLType last() throws JMLSequenceException
JMLSequenceException
 if the sequence is empty.itemAt(int)
,
first()
,
header()
,
trailer()
public boolean isSubsequence(JMLValueSequence s2)
s2
 the sequence to search for within this sequence.
isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
,
isSupersequence(org.jmlspecs.models.JMLValueSequence)
public boolean isProperSubsequence(JMLValueSequence s2)
s2
 the sequence to search for within this sequence.
isSubsequence(org.jmlspecs.models.JMLValueSequence)
,
isProperSupersequence(org.jmlspecs.models.JMLValueSequence)
public boolean isSupersequence(JMLValueSequence s2)
s2
 the sequence to search within for this sequence.
isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
,
isSubsequence(org.jmlspecs.models.JMLValueSequence)
public boolean isProperSupersequence(JMLValueSequence s2)
s2
 the sequence to search within for this sequence.
isSupersequence(org.jmlspecs.models.JMLValueSequence)
,
isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
public boolean isInsertionInto(JMLValueSequence s2, JMLType elem)
s2
 the shorter sequence, which we see if the elem is
inserted intoelem
 the given element
isDeletionFrom(org.jmlspecs.models.JMLValueSequence, org.jmlspecs.models.JMLType)
,
isProperSupersequence(org.jmlspecs.models.JMLValueSequence)
,
isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
,
subsequence(int, int)
public boolean isDeletionFrom(JMLValueSequence s2, JMLType elem)
s2
 the longer sequence, in which we see if the elem is
deleted fromelem
 the given element
isInsertionInto(org.jmlspecs.models.JMLValueSequence, org.jmlspecs.models.JMLType)
,
isProperSupersequence(org.jmlspecs.models.JMLValueSequence)
,
isProperSubsequence(org.jmlspecs.models.JMLValueSequence)
,
subsequence(int, int)
public Object clone()
clone
in interface JMLType
clone
in class JMLValueSequenceSpecs
public JMLValueSequence prefix(int n) throws JMLSequenceException
n
 the number of elements in the result.
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.trailer()
,
removePrefix(int)
,
Return a sequence containing the first n elements in this sequence.
,
trailer()
,
removePrefix(int)
,
subsequence(int, int)
public JMLValueSequence removePrefix(int n) throws JMLSequenceException
n
 the number of elements to remove
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.header()
,
prefix(int)
,
Return a sequence containing all but the first n elements in this.
,
header()
,
prefix(int)
,
subsequence(int, int)
public JMLValueSequence concat(JMLValueSequence s2)
s2
 the sequence to place at the end of this sequence in
the result.
public JMLValueSequence reverse()
public JMLValueSequence removeItemAt(int index) throws JMLSequenceException
index
 the zerobased index into the sequence.
JMLSequenceException
 if the index is out of range.
JMLSequenceException
 if the index is out of range.itemAt(int)
,
removeItemAt(int)
,
prefix(int)
,
removePrefix(int)
,
subsequence(int, int)
,
Return a sequence like this, but without the element at the
given zerobased index.
,
itemAt(int)
,
removeItemAt(int)
,
prefix(int)
,
removePrefix(int)
,
subsequence(int, int)
,
concat(org.jmlspecs.models.JMLValueSequence)
public JMLValueSequence replaceItemAt(int index, JMLType item) throws JMLSequenceException
index
 the zerobased index into the sequence.item
 the item to put at index index
JMLSequenceException
 if the index is out of range.
JMLSequenceException
 if the index is out of range.itemAt(int)
,
Return a sequence like this, but with item replacing the element at the
given zerobased index.
,
itemAt(int)
,
replaceItemAt(int, org.jmlspecs.models.JMLType)
public JMLValueSequence header() throws JMLSequenceException
JMLSequenceException
 if this is empty.prefix(int)
,
first()
,
last()
,
trailer()
,
subsequence(int, int)
public JMLValueSequence trailer() throws JMLSequenceException
JMLSequenceException
 if this is empty.removePrefix(int)
,
last()
,
first()
,
header()
,
subsequence(int, int)
public JMLValueSequence insertAfterIndex(int afterThisOne, JMLType item) throws JMLSequenceException, IllegalStateException
afterThisOne
 a zerobased index into the sequence, or 1.item
 the item to put after index afterThisOne
JMLSequenceException
 if the index is out of range.
JMLSequenceException
 if the index is out of range.
IllegalStateException
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)
public JMLValueSequence insertBeforeIndex(int beforeThisOne, JMLType item) throws JMLSequenceException, IllegalStateException
beforeThisOne
 a zerobased index into the sequence,
or the length of this.item
 the item to put before index beforeThisOne
JMLSequenceException
 if the index is out of range.
JMLSequenceException
 if the index is out of range.
IllegalStateException
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)
public JMLValueSequence insertBack(JMLType item) throws IllegalStateException
item
 the item to put at the end of the result.
IllegalStateException
insertAfterIndex(int, org.jmlspecs.models.JMLType)
,
insertBeforeIndex(int, org.jmlspecs.models.JMLType)
,
insertFront(org.jmlspecs.models.JMLType)
,
removeItemAt(int)
,
header()
,
last()
public JMLValueSequence insertFront(JMLType item) throws IllegalStateException
item
 the item to put at the front of the result.
IllegalStateException
insertAfterIndex(int, org.jmlspecs.models.JMLType)
,
insertBeforeIndex(int, org.jmlspecs.models.JMLType)
,
insertBack(org.jmlspecs.models.JMLType)
,
removeItemAt(int)
,
trailer()
,
first()
public JMLValueSequence subsequence(int from, int to) throws JMLSequenceException
from
 the inclusive, zerobased element of the first
element in the subsequence.to
 the zerobased element of the first element that
should not be in the subsequence.
JMLSequenceException
 if (from < 0 or from > to
or to > length of this.
JMLSequenceException
 if (from < 0 or from > to
or to > length of this.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)
public JMLValueBag toBag()
toSet()
,
toArray()
public JMLValueSet toSet()
toBag()
,
toArray()
public JMLType[] toArray()
toSet()
,
toBag()
public JMLValueSequenceEnumerator elements()
iterator()
,
#itemAt()
public JMLIterator iterator()
iterator
in interface JMLCollection
elements()
public String toString()
toString
in class Object

JML  
PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 