JML

org.jmlspecs.models.resolve
Class StringOfObject

java.lang.Object
  extended byorg.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()
Constructor Detail

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
Method Detail

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)

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.