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

Class Specifications

public invariant this.owner == null; public invariant !this.containsNull; public invariant ( \forall java.lang.Object o; o != null&&this.has(o); \typeof(o) <: this.elementType); protected invariant !this.elements.containsNull; public invariant_redundantly org.jmlspecs.models.resolve.StringOfObject.EMPTY != null&&org.jmlspecs.models.resolve.StringOfObject.EMPTY.isEmpty(); public constraint_redundantly org.jmlspecs.models.resolve.StringOfObject.EMPTY == \old(org.jmlspecs.models.resolve.StringOfObject.EMPTY);

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

 

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
[spec_public] 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(non_null Object elem)           Initialize this object to string containing just the given object.
protected	StringOfObject(non_null JMLObjectSequence os)           Initialize this object from the given representation.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Model methods inherited from interface org.jmlspecs.models.JMLCollection

size

 

Method Summary
StringOfObject	add(non_null Object elem)           Add an element to a string at the end.
StringOfObject	addAfterIndex(int afterThisOne, non_null Object elem)           Add an element to a string after the given index.
StringOfObject	addAll(non_null 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(non_null 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, non_null Object elem)           Add an element to a string before the given index.
StringOfObject	addFront(non_null Object elem)           Add an element to a string at the front.
Object	clone()           Return a clone of this object.
StringOfObject	composedWith(non_null StringOfObject s)           Compose this with s.
StringOfObject	concat(non_null StringOfObject s)           Concatenate this with s.
JMLObjectSequenceEnumerator	elements()           Return an enumerator for this string of objects.
boolean	equals(nullable Object x)           Tell if this object is equal to the given argument.
StringOfObject	ext(non_null Object elem)           Extend a string with a new element at the end.
static StringOfObject	ext(non_null StringOfObject s, non_null Object elem)           Extend the given string by placing the given element at the end.
static StringOfObject	from(non_null Object[] a)           Make an array of objects into a string.
static StringOfObject	from(non_null Collection c)           Make a collection into a string.
Object	get(int index)           Return the element in the string at the given index.
boolean	has(nullable 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(non_null StringOfObject s2)           Tell whether this string occurs as a prefix of the given argument string.
boolean	isProperPrefix(non_null StringOfObject s2)           Tell whether this string occurs as a proper prefix of the given argument string.
boolean	isProperSuffix(non_null StringOfObject s2)           Tell whether this string occurs as a proper suffix of the given argument string.
boolean	isSuffix(non_null 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(non_null StringOfObject[] a)           Compose all the elements of a in order.
static StringOfObject	productFrom(non_null StringOfObject[] a, int fromIndex)           Compose all the elements of a in order, starting at the given index.
static StringOfObject	productFromTo(non_null 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(non_null 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.

Specifications: spec_public non_null
is in groups: objectState

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

Specifications: non_null

StringOfObject

public StringOfObject()

Initialize this object to be empty string of objects.

See Also:

EMPTY, StringOfObject(Object)

Specifications: (class)pure

public normal_behavior
assignable objectState, owner, containsNull, elementType;
ensures this.elements.isEmpty();

StringOfObject

public StringOfObject(non_null Object elem)
               throws IllegalArgumentException

Initialize this object to string containing just the given object.

Throws:

IllegalArgumentException

See Also:

StringOfObject(), singleton(Object)

Specifications: (class)pure

public normal_behavior
requires elem != null;
assignable objectState, owner, containsNull, elementType;
ensures this.elements.equals(new org.jmlspecs.models.JMLObjectSequence(elem));

    implies_that

requires elem != null;

StringOfObject

protected StringOfObject(non_null JMLObjectSequence os)
                  throws IllegalArgumentException

Initialize this object from the given representation.

Throws:

IllegalArgumentException

Specifications: (class)pure

protected normal_behavior
requires os != null&&!os.containsNull&&os.owner == null;
assignable objectState, owner, containsNull, elementType;
ensures this.elements != null&&this.elements.equals(os);

    implies_that

requires os != null&&!os.containsNull;

singleton

public static StringOfObject singleton(non_null Object elem)
                                throws IllegalArgumentException

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

Throws:

IllegalArgumentException

See Also:

StringOfObject(Object)

Specifications: pure non_null

public normal_behavior
requires elem != null;
ensures \result != null&&\result .int_size() == 1&&\result .get(0) == elem;

ext

public static StringOfObject ext(non_null StringOfObject s,
                                 non_null 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)

Specifications: pure non_null

public normal_behavior
requires s != null&&elem != null;
ensures \result != null&&\result .elements.equals(s.elements.insertBack(elem));

from

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

Make an array of objects into a string.

Throws:

IllegalArgumentException

See Also:

from(Collection), addAll(Object[])

Specifications: pure non_null

public normal_behavior
requires \nonnullelements(a);
ensures \result != null&&\result .equals(org.jmlspecs.models.resolve.StringOfObject.EMPTY.addAll(a));

from

public static StringOfObject from(non_null Collection c)
                           throws IllegalArgumentException

Make a collection into a string.

Throws:

IllegalArgumentException

See Also:

from(Object[]), addAll(Collection)

Specifications: pure non_null

public normal_behavior
requires c != null&&!c.contains(null);
ensures \result != null&&\result .equals(org.jmlspecs.models.resolve.StringOfObject.EMPTY.addAll(c));

product

public static StringOfObject product(non_null StringOfObject[] a)

Compose all the elements of a in order.

See Also:

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

Specifications: pure non_null

public normal_behavior
requires \nonnullelements(a);
ensures \result .equals(productFrom(a,0));

    implies_that

requires \nonnullelements(a);

productFrom

public static StringOfObject productFrom(non_null 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)

Specifications: pure non_null

public normal_behavior
requires \nonnullelements(a)&&0 <= fromIndex&&fromIndex <= a.length;
ensures \result .equals(productFromTo(a,fromIndex,a.length));

    implies_that

requires \nonnullelements(a)&&a != null&&0 <= fromIndex&&fromIndex <= a.length;

productFromTo

public static StringOfObject productFromTo(non_null 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)

Specifications: pure non_null

public normal_behavior
requires \nonnullelements(a)&&a != null&&0 <= fromIndex&&fromIndex <= toIndex&&toIndex <= a.length;

{|

requires fromIndex == toIndex;
ensures \result != null&&\result .isEmpty();

also

requires fromIndex < toIndex;
ensures \result != null&&\result .equals(new org.jmlspecs.models.resolve.StringOfObject(a[fromIndex]).concat(productFromTo(a,(int)(fromIndex+1),toIndex)));

|}

    implies_that

requires \nonnullelements(a)&&a != null&&0 <= fromIndex&&fromIndex <= toIndex&&toIndex <= a.length;

get

public Object get(int index)
           throws IndexOutOfBoundsException

Return the element in the string at the given index.

Throws:

IndexOutOfBoundsException

Specifications: non_null (class)pure

public normal_behavior
requires 0 <= index&&index < this.elements.int_size();
ensures \result == this.elements.itemAt(index);

     also

public exceptional_behavior
requires !(0 <= index&&index < this.elements.int_size());
signals_only java.lang.IndexOutOfBoundsException;

    for_example

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x))&&index == 0;
ensures \result == x;

       also

public exceptional_example
requires this.isEmpty();
signals_only java.lang.IndexOutOfBoundsException;

int_size

public int int_size()

Tell the size of this string.

Specified by:

int_size in interface JMLCollection

See Also:

length()

Specifications: (class)pure

     also

public normal_behavior
ensures \result == this.elements.int_size();
ensures_redundantly \result >= 0;

    implies_that

public normal_behavior
requires this.isEmpty();
ensures \result == 0;

     also

public normal_behavior
forall java.lang.Object x;
forall org.jmlspecs.models.resolve.StringOfObject beta;
requires beta != null&&this.equals(beta.ext(x));
ensures \result == beta.int_size()+1;

Specifications inherited from overridden method in interface JMLCollection:
       pure

public normal_behavior
requires this.size() <= 2147483647;
ensures \result == this.size();

length

public int length()

Tell the length (= size) of this string.

See Also:

int_size()

Specifications: (class)pure

public normal_behavior
ensures \result == this.elements.int_size();
ensures_redundantly \result == this.int_size();

    implies_that

public normal_behavior
requires this.isEmpty();
ensures \result == 0;

ext

public StringOfObject ext(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires elem != null;
ensures \result != null&&\result .elements.equals(this.elements.insertBack(elem));

    implies_that

public normal_behavior
ensures \result != null&&\result .int_size() == this.int_size()+1&&( \forall int i; 0 <= i&&i < this.int_size(); \result .get(i) == this.get(i))&&\result .get(this.int_size()) == elem;

    for_example

public normal_example
requires this.equals(org.jmlspecs.models.resolve.StringOfObject.EMPTY);
ensures \result != null&&\result .equals(new org.jmlspecs.models.resolve.StringOfObject(elem));

       also

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x));
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == x&&\result .get(1) == elem;

add

public StringOfObject add(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires elem != null;
ensures \result != null&&\result .equals(this.ext(elem));

addFront

public StringOfObject addFront(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&\result .elements.equals(this.elements.insertFront(elem));

    implies_that

public normal_behavior
ensures \result != null&&\result .int_size() == this.int_size()+1&&\result .get(0) == elem&&( \forall int i; 0 <= i&&i < this.int_size(); \result .get((int)(i+1)) == this.get(i));

    for_example

public normal_example
requires this.equals(org.jmlspecs.models.resolve.StringOfObject.EMPTY);
ensures \result != null&&\result .equals(new org.jmlspecs.models.resolve.StringOfObject(elem));

       also

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x));
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == elem&&\result .get(1) == x;

addAfterIndex

public StringOfObject addAfterIndex(int afterThisOne,
                                    non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires -1 <= afterThisOne&&afterThisOne < this.int_size();
ensures \result != null&&\result .elements.equals(this.elements.insertAfterIndex(afterThisOne,elem));

     also

public exceptional_behavior
requires !(-1 <= afterThisOne&&afterThisOne < this.int_size());
signals_only java.lang.IndexOutOfBoundsException;

    for_example

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x))&&afterThisOne == -1;
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == elem&&\result .get(1) == x;

       also

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x))&&afterThisOne == 0;
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == x&&\result .get(1) == elem;

addBeforeIndex

public StringOfObject addBeforeIndex(int beforeThisOne,
                                     non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires 0 <= beforeThisOne&&beforeThisOne <= this.int_size();
ensures \result != null&&\result .elements.equals(this.elements.insertBeforeIndex(beforeThisOne,elem));

     also

public exceptional_behavior
requires !(0 <= beforeThisOne&&beforeThisOne <= this.int_size());
signals_only java.lang.IndexOutOfBoundsException;

    for_example

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x))&&beforeThisOne == 0;
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == elem&&\result .get(1) == x;

       also

public normal_example
forall java.lang.Object x;
requires this.equals(new org.jmlspecs.models.resolve.StringOfObject(x))&&beforeThisOne == 1;
ensures \result != null&&\result .int_size() == 2&&\result .get(0) == x&&\result .get(1) == elem;

concat

public StringOfObject concat(non_null StringOfObject s)

Concatenate this with s.

See Also:

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

Specifications: non_null (class)pure

public normal_behavior
requires s != null;

{|

requires s.isEmpty();
ensures \result != null&&\result .equals(this);

also

requires !s.isEmpty();
ensures \result != null&&( \forall org.jmlspecs.models.resolve.StringOfObject beta; beta != null; ( \forall java.lang.Object x; s.equals(beta.ext(x)); \result .equals(this.concat(beta).ext(x))));

|}

composedWith

public StringOfObject composedWith(non_null StringOfObject s)

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

See Also:

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

Specifications: non_null (class)pure

public normal_behavior
requires s != null;
ensures \result != null&&\result .equals(this.concat(s));

addAll

public StringOfObject addAll(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires c != null;
ensures \result != null&&\result .int_size() == this.int_size()+c.size()&&( \forall int i; 0 <= i&&i < \result .int_size(); (i < this.int_size() ==> \result .get(i) == this.get(i))&&(this.int_size() <= i ==> \result .get(i) == c.iterator().nthNextElement((int)(i-this.int_size()))));

    implies_that

public normal_behavior
requires c != null;
ensures \result .equals(this);

addAll

public StringOfObject addAll(non_null 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)

Specifications: non_null (class)pure

public normal_behavior
requires \nonnullelements(c);
ensures \result != null&&\result .int_size() == this.int_size()+c.length&&( \forall int i; 0 <= i&&i < \result .int_size(); (i < this.int_size() ==> \result .get(i) == this.get(i))&&(this.int_size() <= i ==> \result .get(i) == c[(int)(i-this.int_size())]));

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

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&\result .elements.equals(this.elements.reverse());

    implies_that

public normal_behavior
ensures \result != null&&\result .int_size() == this.int_size()&&( \forall int i; 0 <= i&&i < this.int_size(); this.get(i) == \result .get((int)(this.int_size()-i)));

     also

public normal_behavior
requires this.elements.isEmpty();
ensures \result != null&&\result .equals(this);
ensures \result != null&&\result .isEmpty();

     also

public normal_behavior
forall org.jmlspecs.models.resolve.StringOfObject alpha;
forall java.lang.Object x;
requires !this.elements.isEmpty();
ensures \result != null&&(alpha != null&&this.equals(alpha.ext(x)) ==> \result .equals(singleton(x).concat(alpha.rev())));

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

Specifications: non_null (class)pure

public normal_behavior
ensures \result != null&&\result .equals(this.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)

Specifications: non_null (class)pure

public normal_behavior
requires n >= 0;

{|

requires n == 0;
ensures \result != null&&\result .isEmpty();

also

requires n > 0;
ensures \result != null&&\result .equals(this.pow((int)(n-1)).concat(this));

|}

equals

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

Specifications: (class)pure

     also

public normal_behavior
ensures \result ==> x != null&&x instanceof org.jmlspecs.models.resolve.StringOfObject&&this.int_size() == ((org.jmlspecs.models.resolve.StringOfObject)x).int_size()&&( \forall int i; 0 <= i&&i < this.int_size(); this.get(i) == ((org.jmlspecs.models.resolve.StringOfObject)x).get(i));

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;

|}

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

Specifications: (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);

occurs_ct

public int occurs_ct(Object y)

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

Specifications: (class)pure

public normal_behavior

{|

requires this.isEmpty();
ensures \result == 0;

also

forall org.jmlspecs.models.resolve.StringOfObject alpha;
requires alpha != null&&this.equals(alpha.ext(y));
ensures \result == alpha.occurs_ct(y)+1;

also

forall org.jmlspecs.models.resolve.StringOfObject alpha;
forall java.lang.Object x;
requires alpha != null&&this.equals(alpha.ext(x))&&x != y;
ensures \result == alpha.occurs_ct(y);

|}

    implies_that

public normal_behavior
ensures \result == ( \num_of int i; 0 <= i&&i < this.int_size(); this.get(i) == y);

has

public boolean has(nullable 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

Specifications: (class)pure

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 ;

isEmpty

public boolean isEmpty()

Tell whether this string is empty.

See Also:

int_size(), length()

Specifications: (class)pure

public normal_behavior
ensures \result <==> this.elements.isEmpty();
ensures_redundantly \result <==> this.equals(org.jmlspecs.models.resolve.StringOfObject.EMPTY);

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

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

toString

public String toString()

Overrides:

toString in class Object

Specifications: (class)pure

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;

iterator

public JMLIterator iterator()

Return an iterator for this string of objects.

Specified by:

iterator in interface JMLCollection

See Also:

elements()

Specifications: (class)pure

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;

elements

public JMLObjectSequenceEnumerator elements()

Return an enumerator for this string of objects.

See Also:

iterator()

Specifications: (class)pure

public normal_behavior
ensures \result != null&&this.elements.equals(\result .uniteratedElems);

isPrefix

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

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists org.jmlspecs.models.resolve.StringOfObject s; s != null; this.concat(s).equals(s2));
ensures_redundantly \result <==> this.elements.isPrefix(s2.elements);

isProperPrefix

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

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists org.jmlspecs.models.resolve.StringOfObject s; s != null&&s.int_size() > 0; this.concat(s).equals(s2));
ensures_redundantly \result <==> this.elements.isProperPrefix(s2.elements);

isProperSuffix

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

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists org.jmlspecs.models.resolve.StringOfObject r; r != null&&r.int_size() > 0; r.concat(this).equals(s2));
ensures_redundantly \result <==> this.elements.isProperSuffix(s2.elements);

isSuffix

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

Specifications: (class)pure

public normal_behavior
requires s2 != null;
ensures \result <==> ( \exists org.jmlspecs.models.resolve.StringOfObject r; r != null; r.concat(this).equals(s2));
ensures_redundantly \result <==> this.elements.isSuffix(s2.elements);