org.jmlspecs.models
Class JMLValueSequenceSpecs

java.lang.Object
  org.jmlspecs.models.JMLValueSequenceSpecs

All Implemented Interfaces:

Cloneable, JMLType, JMLValueType, Serializable

Direct Known Subclasses:

JMLValueSequence

public abstract class JMLValueSequenceSpecs

extends Object

implements JMLValueType

Specical behavior for JMLValueSequence not shared by JMLObjectSequence.

Version:

$Revision: 1.19 $

Author:

Gary T. Leavens, with help from Clyde Ruby, and others.

See Also:

JMLValueType, JMLValueBag

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Constructor Summary

JMLValueSequenceSpecs()

 

Model Method Summary
JMLType	objectAt(\bigint i)           Return the representative at the given index.

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
abstract  Object	clone()           Return a clone of this object, making clones of any contained objects in the sequence.
int	count(Object elem)           Tell many times the argument occurs ".equals" to one of the values in the bag.
abstract  int	count(JMLType elem)           Tell many times the argument occurs ".equals" to one of the values in this sequence.
abstract  JMLType	first()           Return a clone of the first element in this sequence.
boolean	has(Object elem)           Is the argument ".equals" to one of the values in this sequence.
abstract  boolean	has(JMLType elem)           Is the argument ".equals" to one of the values in this sequence.
abstract  JMLValueSequence	insertAfterIndex(int afterThisOne, JMLType item)           Return a sequence like this, but with a clone ofitem put immediately after the given index.
abstract  JMLValueSequence	insertBack(JMLType item)           Return a sequence like this, but with a clone of the given item put an the end.
abstract  JMLValueSequence	insertBeforeIndex(int beforeThisOne, JMLType item)           Return a sequence like this, but with a clone of item put immediately before the given index.
abstract  JMLValueSequence	insertFront(JMLType item)           Return a sequence like this, but with the given item put an the front.
abstract  int	int_length()           This sequence's length.
abstract  JMLType	itemAt(int i)           Return a clone of the element at the given zero-based index.
abstract  JMLType	last()           Return a clone of the last element in this sequence.

 

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Methods inherited from interface org.jmlspecs.models.JMLValueType

equals

 

Methods inherited from interface org.jmlspecs.models.JMLType

hashCode

 

Constructor Detail

JMLValueSequenceSpecs

public JMLValueSequenceSpecs()

objectAt

public JMLType objectAt(\bigint i)

Return the representative at the given index.

See Also:

itemAt(int)

Specifications: (class)pure

public normal_behavior
requires 0 <= i&&i < this.int_length();
ensures (* \result is the ith object of this *);

has

public abstract boolean has(JMLType elem)

Is the argument ".equals" to one of the values in this sequence.

See Also:

has(Object), #int_count(JMLType)

Specifications: (class)pure

public normal_behavior
ensures \result <==> (* elem is ".equals" to one of the objects in this sequence *);

has

public boolean has(Object elem)

Is the argument ".equals" to one of the values in this sequence.

See Also:

has(JMLType), count(Object)

Specifications: (class)pure

public normal_behavior
requires elem != null;
ensures \result <==> elem instanceof org.jmlspecs.models.JMLType&&this.has((org.jmlspecs.models.JMLType)elem);

     also

public normal_behavior
requires elem == null;
ensures \result == this.has(null);

count

public abstract int count(JMLType elem)

Tell many times the argument occurs ".equals" to one of the values in this sequence.

See Also:

count(Object), has(JMLType)

Specifications: (class)pure

public normal_behavior
ensures \result >= 0&&(* \result is the number of times elem tests as ".equals" to one of the objects in this sequence *);

count

public int count(Object elem)

Tell many times the argument occurs ".equals" to one of the values in the bag.

See Also:

count(JMLType), has(Object)

Specifications: (class)pure

public normal_behavior
requires elem != null;
ensures \result == (elem instanceof org.jmlspecs.models.JMLType ? this.count((org.jmlspecs.models.JMLType)elem) : 0);

     also

public normal_behavior
requires elem == null;
ensures \result == this.count(null);

int_length

public abstract int int_length()

This sequence's length.

Specifications: (class)pure

public normal_behavior
ensures \result >= 0;

itemAt

public abstract JMLType itemAt(int i)
                        throws JMLSequenceException

Return a clone of the element at the given zero-based index.

Parameters:

i - the zero-based index into the sequence.

Throws:

JMLSequenceException - if the index i is out of range.

Specifications: nullable (class)pure

first

public abstract JMLType first()
                       throws JMLSequenceException

Return a clone of the first element in this sequence.

Throws:

JMLSequenceException - if the sequence is empty.

See Also:

last()

Specifications: nullable (class)pure

last

public abstract JMLType last()
                      throws JMLSequenceException

Return a clone of the last element in this sequence.

Throws:

JMLSequenceException - if the sequence is empty.

See Also:

first()

Specifications: nullable (class)pure

clone

public abstract Object clone()

Return a clone of this object, making clones of any contained objects in the sequence.

Specified by:

clone in interface JMLValueType

Overrides:

clone in class Object

Specifications: non_null (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 JMLValueType:
       pure

     also

public normal_behavior
ensures \result instanceof org.jmlspecs.models.JMLValueType&&(* all externally-visible mutable objects contained directly in "this" must be cloned in \result. *);

    implies_that

ensures (* no direct aliases are created between this and \result *);

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

insertAfterIndex

public abstract JMLValueSequence insertAfterIndex(int afterThisOne,
                                                  JMLType item)
                                           throws JMLSequenceException

Return a sequence like this, but with a clone ofitem 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.

See Also:

insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

insertBeforeIndex

public abstract JMLValueSequence insertBeforeIndex(int beforeThisOne,
                                                   JMLType item)
                                            throws JMLSequenceException

Return a sequence like this, but with a clone of 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.

See Also:

insertAfterIndex(int, org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

insertBack

public abstract JMLValueSequence insertBack(JMLType item)

Return a sequence like this, but with a clone of 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.

See Also:

insertAfterIndex(int, org.jmlspecs.models.JMLType), insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertFront(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure

insertFront

public abstract JMLValueSequence insertFront(JMLType item)

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.

See Also:

insertAfterIndex(int, org.jmlspecs.models.JMLType), insertBeforeIndex(int, org.jmlspecs.models.JMLType), insertBack(org.jmlspecs.models.JMLType)

Specifications: non_null (class)pure