JML

org.jmlspecs.models
Class JMLValueSequenceSpecs

java.lang.Object
  extended byorg.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.18 $
Author:
Gary T. Leavens, with help from Clyde Ruby, and others.
See Also:
JMLValueType, JMLValueBag

Constructor Summary
JMLValueSequenceSpecs()
           
 
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)
          Return the representative at the given index.
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()
Method Detail

has

public abstract boolean has(JMLType elem)
Return the representative at the given index.

See Also:
Is the argument ".equals" to one of the values in this sequence., has(Object), #int_count(JMLType)

has

public boolean has(Object elem)
Is the argument ".equals" to one of the values in this sequence.

See Also:
has(JMLType), count(Object)

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)

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)

int_length

public abstract int int_length()
This sequence's length.


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.

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

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

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

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)

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)

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)

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)

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.