JML

org.jmlspecs.models
Class JMLEqualsBagEntryNode

java.lang.Object
  extended byorg.jmlspecs.models.JMLListValueNode
      extended byorg.jmlspecs.models.JMLEqualsBagEntryNode
All Implemented Interfaces:
Cloneable, JMLType, JMLValueType, Serializable

class JMLEqualsBagEntryNode
extends JMLListValueNode

Internal class used in the implementation of JMLEqualsBag.

Author:
Gary T. Leavens
See Also:
JMLEqualsBag, JMLEqualsBagEntry, JMLListValueNode

Field Summary
 JMLListValueNode next
          The next node in this list.
 JMLType val
          An `equational' specification of lists, for use in the invariant.
 
Constructor Summary
JMLEqualsBagEntryNode(JMLEqualsBagEntry entry, JMLEqualsBagEntryNode nxt)
          The type of the elements contained in the entries in this list.
 
Method Summary
 JMLListValueNode append(JMLType item)
          Return a list that consists of this list and the given element.
 Object clone()
          Return a clone of this object.
 JMLListValueNode concat(JMLListValueNode ls2)
          Return a list that is the concatenation of this with the given lists.
static JMLEqualsBagEntryNode cons(JMLEqualsBagEntry hd, JMLEqualsBagEntryNode tl)
          Return a JMLEqualsBagEntryNode containing the given entry followed by the given list.
static JMLListValueNode cons(JMLType hd, JMLListValueNode tl)
          Return a JMLListValueNode containing the given element followed by the given list.
 boolean equals(Object ls2)
          Test whether this object's value is equal to the given argument.
 JMLType getItem(JMLType item)
          Return the zero-based index of the first occurrence of the given element in the list, if there is one
 boolean has(JMLType item)
          Tells whether the given element is ".equals" to an element in the list.
 int hashCode()
          Return a hash code for this object.
 JMLType head()
          Return the first element in this list.
 boolean headEquals(JMLType item)
          Tell if the head of the list is ".equals" to the given item.
 int indexOf(JMLType item)
          Return the zero-based index of the first occurrence of the given element in the list, if there is one
 JMLListValueNode insertBefore(int n, JMLType item)
          Return a list that is like this list but with the given item inserted before the given index.
 int int_length()
          Tells the number of elements in the list; a synonym for size.
 int int_size()
          Tells the number of elements in the sequence; a synonym for length Tells the number of elements in the sequence; a synonym for length Tells the number of elements in the list; a synonym for length.
 boolean isPrefixOf(JMLListValueNode ls2)
          Tells whether the elements of this list occur, in order, at the beginning of the given list, using ".equals" for comparisons.
 JMLType itemAt(int i)
          Return the ith element of a list.
 JMLType last()
          Return the last element in this list.
 JMLListValueNode prefix(int n)
          Return a list containing the first n elements in this list.
 JMLListValueNode prepend(JMLType item)
          Return a list that is like this, but with the given item at the front.
 JMLListValueNode remove(JMLType item)
          Return a list that is like this list but without the first occurrence of the given item.
 JMLEqualsBagEntryNode removeBE(JMLEqualsBagEntry entry)
          Return a list that is like this list but without the first occurrence of the given bag entry.
 JMLListValueNode removeItemAt(int n)
          Return a list like this list, but without the element at the given zero-based index.
 JMLListValueNode removeLast()
          Return a list containing all but the last element in this.
 JMLListValueNode removePrefix(int n)
          Return a list containing all but the first n elements in this list.
 JMLListValueNode replaceItemAt(int n, JMLType item)
          Return a list like this, but with item replacing the element at the given zero-based index.
 JMLListValueNode reverse()
          Return a list that is the reverse of this list.
 String toString()
          Return a string representation for this list.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

val

public final JMLType val
An `equational' specification of lists, for use in the invariant. The data contained in this list node.


next

public final JMLListValueNode next
The next node in this list.

Constructor Detail

JMLEqualsBagEntryNode

public JMLEqualsBagEntryNode(JMLEqualsBagEntry entry,
                             JMLEqualsBagEntryNode nxt)
The type of the elements contained in the entries in this list. Whether this list can contain null elements in its bag entries; Initialize this list to have the given bag entry as its first element followed by the given list. This does not do any cloning.

Parameters:
entry - the JMLEqualsBagEntry to place at the head of this list.
nxt - the JMLEqualsBagEntryNode to make the tail of this list.
See Also:
cons(org.jmlspecs.models.JMLEqualsBagEntry, org.jmlspecs.models.JMLEqualsBagEntryNode)
Method Detail

cons

public static JMLEqualsBagEntryNode cons(JMLEqualsBagEntry hd,
                                         JMLEqualsBagEntryNode tl)
Return a JMLEqualsBagEntryNode containing the given entry followed by the given list. This method handles any necessary cloning for value lists and it handles inserting null elements.

Parameters:
hd - the JMLEqualsBagEntry to place at the head of the result.
tl - the JMLEqualsBagEntryNode to make the tail of the result.
See Also:
JMLEqualsBagEntryNode(org.jmlspecs.models.JMLEqualsBagEntry, org.jmlspecs.models.JMLEqualsBagEntryNode)

clone

public Object clone()
Return a clone of this object.

Specified by:
clone in interface JMLValueType
Overrides:
clone in class JMLListValueNode

removeBE

public JMLEqualsBagEntryNode removeBE(JMLEqualsBagEntry entry)
Return a list that is like this list but without the first occurrence of the given bag entry.


cons

public static JMLListValueNode cons(JMLType hd,
                                    JMLListValueNode tl)
Return a JMLListValueNode containing the given element followed by the given list. Note that cons() adds elements to the front of a list. It handles any necessary cloning for value lists and it handles inserting null elements.

Parameters:
hd - the value to place at the head of the result.
tl - the JMLListValueNode to make the tail of the result.

head

public JMLType head()
Return the first element in this list. Note that head() handles any cloning necessary for value lists.


headEquals

public boolean headEquals(JMLType item)
Tell if the head of the list is ".equals" to the given item.

See Also:
JMLListValueNode.has(JMLType)

itemAt

public JMLType itemAt(int i)
               throws JMLListException
Return the ith element of a list.

Throws:
JMLListException
See Also:
Return the ith element of a list., #getItem(int)

int_size

public int int_size()
Tells the number of elements in the sequence; a synonym for length Tells the number of elements in the sequence; a synonym for length Tells the number of elements in the list; a synonym for length.


int_length

public int int_length()
Tells the number of elements in the list; a synonym for size.


has

public boolean has(JMLType item)
Tells whether the given element is ".equals" to an element in the list.


isPrefixOf

public boolean isPrefixOf(JMLListValueNode ls2)
Tells whether the elements of this list occur, in order, at the beginning of the given list, using ".equals" for comparisons.


equals

public boolean equals(Object ls2)
Test whether this object's value is equal to the given argument.

Specified by:
equals in interface JMLValueType
Overrides:
equals in class Object

hashCode

public int hashCode()
Return a hash code for this object.

Specified by:
hashCode in interface JMLType
Overrides:
hashCode in class Object

indexOf

public int indexOf(JMLType item)
Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:
item - the JMLType sought in this.
Returns:
the first index at which item occurs or -1 if it does not. Return the zero-based index of the first occurrence of the given element in the list, if there is one

last

public JMLType last()
Return the last element in this list.


getItem

public JMLType getItem(JMLType item)
                throws JMLListException
Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:
item - the JMLType sought in this list.
Returns:
the first zero-based index at which item occurs.
Throws:
JMLListException - if the item does not occur in this list.
See Also:
JMLListValueNode.itemAt(int)

prefix

public JMLListValueNode prefix(int n)
Return a list containing the first n elements in this list.

Parameters:
n - the number of elements to leave in the result.
Returns:
null if n is not positive or greater than the length of this list. Return a list containing the first n elements in this list.

removePrefix

public JMLListValueNode removePrefix(int n)
Return a list containing all but the first n elements in this list.

Parameters:
n - the number of elements to remove
Returns:
null if n is negative or greater than the length of this list. Return a list containing all but the first n elements in this list.

removeItemAt

public JMLListValueNode removeItemAt(int n)
Return a list like this list, but without the element at the given zero-based index.

Parameters:
n - the zero-based index into the list.
Returns:
null if the index is out of range or if the list was of size 1. Return a list like this list, but without the element at the given zero-based index.

replaceItemAt

public JMLListValueNode replaceItemAt(int n,
                                      JMLType item)
Return a list like this, but with item replacing the element at the given zero-based index.

Parameters:
n - the zero-based index into this list.
item - the item to put at index index Return a list like this, but with item replacing the element at the given zero-based index.

removeLast

public JMLListValueNode removeLast()
Return a list containing all but the last element in this.


concat

public JMLListValueNode concat(JMLListValueNode ls2)
Return a list that is the concatenation of this with the given lists.

Parameters:
ls2 - the list to place at the end of this list in the result.
Returns:
the concatenation of this list and ls2.

prepend

public JMLListValueNode prepend(JMLType item)
Return a list that is like this, but with the given item at the front. Note that this clones the item if necessary.

Parameters:
item - the element to place at the front of the result.

append

public JMLListValueNode append(JMLType item)
Return a list that consists of this list and the given element.


reverse

public JMLListValueNode reverse()
Return a list that is the reverse of this list.


insertBefore

public JMLListValueNode insertBefore(int n,
                                     JMLType item)
                              throws JMLListException
Return a list that is like this list but with the given item inserted before the given index. Return a list that is like this list but with the given item inserted before the given index.

Throws:
JMLListException

remove

public JMLListValueNode remove(JMLType item)
Return a list that is like this list but without the first occurrence of the given item.


toString

public String toString()
Return a string representation for this list. The output is ML style.

Overrides:
toString in class Object

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.