org.jmlspecs.models.resolve
Class StringOfObject

java.lang.Object
  org.jmlspecs.models.resolve.StringOfObject

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, Serializable

public class StringOfObject

extends Object

implements JMLCollection

Sequences of non-null object identities. Objects in the sequence are not cloned coming in or going out, and this type uses "==" to compare object identities.

The names in this type are based prnimarily on the RESOLVE design, but are also chosen to be understandable to someone familiar with Collection. However, note that none of the operations does any mutation.

Many of the specifications are translated from William Ogden's notes for CIS 680 at Ohio State University. (Thanks Bill!) This is especially true for the ones specified recursively. Specifications written using the #size and get(int) operations are an alternative, and often given in the redundant parts.

Version:

$Revision: 1.33 $

Author:

Gary T. Leavens

See Also:

JMLObjectSequence, JMLCollection, TotallyOrderedCompareTo

Field Summary
protected  JMLObjectSequence	elements           The sequence of objects that represent this string of objects.
static StringOfObject	EMPTY           The empty string of objects.
private static String	ILLEGAL_ARG_MSG           Message used in exceptions.

 

Constructor Summary
	StringOfObject()           Initialize this object to be empty string of objects.
	StringOfObject(Object elem)           Initialize this object to string containing just the given object.
protected	StringOfObject(JMLObjectSequence os)           Initialize this object from the given representation.

 

Method Summary
StringOfObject	add(Object elem)           Add an element to a string at the end.
StringOfObject	addAfterIndex(int afterThisOne, Object elem)           Add an element to a string after the given index.
StringOfObject	addAll(Object[] c)           Add all the elements of c at the end of this string, in order from the smallest to the largest index.
StringOfObject	addAll(Collection c)           Add all the elements of c, at the end of this string, in the order determined by c's iterator.
StringOfObject	addBeforeIndex(int beforeThisOne, Object elem)           Add an element to a string before the given index.
StringOfObject	addFront(Object elem)           Add an element to a string at the front.
Object	clone()           Return a clone of this object.
StringOfObject	composedWith(StringOfObject s)           Compose this with s.
StringOfObject	concat(StringOfObject s)           Concatenate this with s.
JMLObjectSequenceEnumerator	elements()           Return an enumerator for this string of objects.
boolean	equals(Object x)           Tell if this object is equal to the given argument.
StringOfObject	ext(Object elem)           Extend a string with a new element at the end.
static StringOfObject	ext(StringOfObject s, Object elem)           Extend the given string by placing the given element at the end.
static StringOfObject	from(Object[] a)           Make an array of objects into a string.
static StringOfObject	from(Collection c)           Make a collection into a string.
Object	get(int index)           Return the element in the string at the given index.
boolean	has(Object elem)           Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.
int	hashCode()           Return a hash code for this object.
int	int_size()           Tell the size of this string.
boolean	isEmpty()           Tell whether this string is empty.
boolean	isPrefix(StringOfObject s2)           Tell whether this string occurs as a prefix of the given argument string.
boolean	isProperPrefix(StringOfObject s2)           Tell whether this string occurs as a proper prefix of the given argument string.
boolean	isProperSuffix(StringOfObject s2)           Tell whether this string occurs as a proper suffix of the given argument string.
boolean	isSuffix(StringOfObject s2)           Tell whether this string occurs as a suffix of the given argument string.
JMLIterator	iterator()           Return an iterator for this string of objects.
int	length()           Tell the length (= size) of this string.
int	occurs_ct(Object y)           Tell how many times the given object appears in this string.
StringOfObject	pow(int n)           Compose this string with itself the given number of times.
static StringOfObject	product(StringOfObject[] a)           Compose all the elements of a in order.
static StringOfObject	productFrom(StringOfObject[] a, int fromIndex)           Compose all the elements of a in order, starting at the given index.
static StringOfObject	productFromTo(StringOfObject[] a, int fromIndex, int toIndex)           Compose all the elements of a in order, starting with fromIndex, and including elements up to but not including toIndex.
StringOfObject	rev()           Return the reverse of the string.
StringOfObject	reverse()           Return the reverse of the string.
static StringOfObject	singleton(Object elem)           Make a singleton string of objects containing just the given object.
String	toString()

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

elements

protected final JMLObjectSequence elements

The sequence of objects that represent this string of objects.

ILLEGAL_ARG_MSG

private static final String ILLEGAL_ARG_MSG

Message used in exceptions.

EMPTY

public static final StringOfObject EMPTY

The empty string of objects.

See Also:

StringOfObject()

StringOfObject

public StringOfObject()

Initialize this object to be empty string of objects.

See Also:

EMPTY, StringOfObject(Object)

StringOfObject

public StringOfObject(Object elem)
               throws IllegalArgumentException

Initialize this object to string containing just the given object.

Throws:

IllegalArgumentException

See Also:

StringOfObject(), singleton(Object)

StringOfObject

protected StringOfObject(JMLObjectSequence os)
                  throws IllegalArgumentException

Initialize this object from the given representation.

Throws:

IllegalArgumentException

singleton

public static StringOfObject singleton(Object elem)
                                throws IllegalArgumentException

Make a singleton string of objects containing just the given object.

Throws:

IllegalArgumentException

See Also:

StringOfObject(Object)

ext

public static StringOfObject ext(StringOfObject s,
                                 Object elem)
                          throws IllegalArgumentException

Extend the given string by placing the given element at the end.

Throws:

IllegalArgumentException

See Also:

ext(Object), add(Object), addFront(Object), addAfterIndex(int, java.lang.Object), addBeforeIndex(int, java.lang.Object)

from

public static StringOfObject from(Object[] a)
                           throws IllegalArgumentException

Make an array of objects into a string.

Throws:

IllegalArgumentException

See Also:

from(Collection), addAll(Object[])

from

public static StringOfObject from(Collection c)
                           throws IllegalArgumentException

Make a collection into a string.

Throws:

IllegalArgumentException

See Also:

from(Object[]), addAll(Collection)

product

public static StringOfObject product(StringOfObject[] a)

Compose all the elements of a in order.

See Also:

productFrom(StringOfObject[], int), productFromTo(StringOfObject[], int, int), composedWith(StringOfObject)

productFrom

public static StringOfObject productFrom(StringOfObject[] a,
                                         int fromIndex)

Compose all the elements of a in order, starting at the given index.

See Also:

#productFrom(StringOfObject[]), productFromTo(StringOfObject[], int, int), composedWith(StringOfObject)

productFromTo

public static StringOfObject productFromTo(StringOfObject[] a,
                                           int fromIndex,
                                           int toIndex)

Compose all the elements of a in order, starting with fromIndex, and including elements up to but not including toIndex.

Parameters:

fromIndex - the index of the first string of elements to compose with.

toIndex - one past the index of the elements to compose with.

See Also:

productFrom(StringOfObject[], int), productFromTo(StringOfObject[], int, int), composedWith(StringOfObject)

get

public Object get(int index)
           throws IndexOutOfBoundsException

Return the element in the string at the given index.

Throws:

IndexOutOfBoundsException

int_size

public int int_size()

Tell the size of this string.

Specified by:

int_size in interface JMLCollection

See Also:

length()

length

public int length()

Tell the length (= size) of this string.

See Also:

int_size()

ext

public StringOfObject ext(Object elem)
                   throws IllegalArgumentException

Extend a string with a new element at the end.

Throws:

IllegalArgumentException

See Also:

ext(StringOfObject, Object), add(Object), addFront(Object), addAfterIndex(int, java.lang.Object), addBeforeIndex(int, java.lang.Object)

add

public StringOfObject add(Object elem)
                   throws IllegalArgumentException

Add an element to a string at the end. This is a synonym for ext.

Throws:

IllegalArgumentException

See Also:

ext(Object), ext(StringOfObject, Object), addFront(Object), addAfterIndex(int, java.lang.Object), addBeforeIndex(int, java.lang.Object)

addFront

public StringOfObject addFront(Object elem)
                        throws IllegalArgumentException

Add an element to a string at the front.

Throws:

IllegalArgumentException

See Also:

add(Object), ext(Object), ext(StringOfObject, Object), addAfterIndex(int, java.lang.Object), addBeforeIndex(int, java.lang.Object)

addAfterIndex

public StringOfObject addAfterIndex(int afterThisOne,
                                    Object elem)
                             throws IndexOutOfBoundsException,
                                    IllegalArgumentException

Add an element to a string after the given index.

Throws:

IndexOutOfBoundsException

IllegalArgumentException

See Also:

addBeforeIndex(int, java.lang.Object), addFront(Object), add(Object), ext(Object), ext(StringOfObject, Object)

addBeforeIndex

public StringOfObject addBeforeIndex(int beforeThisOne,
                                     Object elem)
                              throws IndexOutOfBoundsException,
                                     IllegalArgumentException

Add an element to a string before the given index.

Throws:

IndexOutOfBoundsException

IllegalArgumentException

See Also:

addAfterIndex(int, java.lang.Object), addFront(Object), add(Object), ext(Object), ext(StringOfObject, Object)

concat

public StringOfObject concat(StringOfObject s)

Concatenate this with s.

See Also:

composedWith(org.jmlspecs.models.resolve.StringOfObject)

composedWith

public StringOfObject composedWith(StringOfObject s)

Compose this with s. This is a synonym for concat.

See Also:

concat(org.jmlspecs.models.resolve.StringOfObject)

addAll

public StringOfObject addAll(Collection c)
                      throws IllegalArgumentException

Add all the elements of c, at the end of this string, in the order determined by c's iterator.

Throws:

IllegalArgumentException

See Also:

addAll(Object[]), from(Collection)

addAll

public StringOfObject addAll(Object[] c)
                      throws IllegalArgumentException

Add all the elements of c at the end of this string, in order from the smallest to the largest index.

Throws:

IllegalArgumentException

See Also:

addAll(Collection)

rev

public StringOfObject rev()

Return the reverse of the string. That is, the same string with the elements in the opposite order.

See Also:

reverse()

reverse

public StringOfObject reverse()

Return the reverse of the string. That is, the same string with the elements in the opposite order.

See Also:

rev()

pow

public StringOfObject pow(int n)
                   throws IllegalArgumentException

Compose this string with itself the given number of times.

Throws:

IllegalArgumentException

See Also:

composedWith(org.jmlspecs.models.resolve.StringOfObject)

equals

public boolean equals(Object x)

Tell if this object is equal to the given argument.

Specified by:

equals in interface JMLType

Overrides:

equals in class Object

See Also:

#compareTo(Object), #compareTo(StringOfObject)

clone

public Object clone()

Description copied from interface: JMLType

Return a clone of this object.

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

occurs_ct

public int occurs_ct(Object y)

Tell how many times the given object appears in this string.

has

public boolean has(Object elem)

Description copied from interface: JMLCollection

Tell whether the argument is equal to one of the elements in this collection, using the notion of element equality appropriate for the collection.

Specified by:

has in interface JMLCollection

isEmpty

public boolean isEmpty()

Tell whether this string is empty.

See Also:

int_size(), length()

hashCode

public int hashCode()

Description copied from interface: JMLType

Return a hash code for this object.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object

iterator

public JMLIterator iterator()

Return an iterator for this string of objects.

Specified by:

iterator in interface JMLCollection

See Also:

elements()

elements

public JMLObjectSequenceEnumerator elements()

Return an enumerator for this string of objects.

See Also:

iterator()

isPrefix

public boolean isPrefix(StringOfObject s2)

Tell whether this string occurs as a prefix of the given argument string.

See Also:

isProperPrefix(org.jmlspecs.models.resolve.StringOfObject), isSuffix(org.jmlspecs.models.resolve.StringOfObject)

isProperPrefix

public boolean isProperPrefix(StringOfObject s2)

Tell whether this string occurs as a proper prefix of the given argument string.

See Also:

isPrefix(org.jmlspecs.models.resolve.StringOfObject), isProperSuffix(org.jmlspecs.models.resolve.StringOfObject)

isProperSuffix

public boolean isProperSuffix(StringOfObject s2)

Tell whether this string occurs as a proper suffix of the given argument string.

See Also:

isSuffix(org.jmlspecs.models.resolve.StringOfObject), isProperPrefix(org.jmlspecs.models.resolve.StringOfObject)

isSuffix

public boolean isSuffix(StringOfObject s2)

Tell whether this string occurs as a suffix of the given argument string.

See Also:

isProperSuffix(org.jmlspecs.models.resolve.StringOfObject), isPrefix(org.jmlspecs.models.resolve.StringOfObject)