org.jmlspecs.models
Class JMLListEqualsNode

java.lang.Object
  org.jmlspecs.models.JMLListEqualsNode

All Implemented Interfaces:

Cloneable, JMLType, Serializable

class JMLListEqualsNode

extends Object

implements JMLType

An implementation class used in various models. These are singly-linked list nodes containing objects. The empty list is represented by null, which makes dealing with these lists tricky. Normal users should use JMLEqualsSequence instead of this type to avoid these difficulties.

This type uses ".equals" to compare elements. The cons method does not clone elements that are passed into the list.

Version:

$Revision: 1.56 $

Author:

Gary T. Leavens, Albert L. Baker

See Also:

JMLEqualsSequence, JMLEqualsBag, JMLEqualsSet

Field Summary
JMLListEqualsNode	next           The next node in this list.
Object	val           An `equational' specification of lists, for use in the invariant.

 

Constructor Summary

JMLListEqualsNode(Object item, JMLListEqualsNode nxt)           The type of the elements in this list.

 

Method Summary
JMLListEqualsNode	append(Object item)           Return a list that consists of this list and the given element.
Object	clone()           Return a clone of this object.
JMLListEqualsNode	concat(JMLListEqualsNode ls2)           Return a list that is the concatenation of this with the given lists.
static JMLListEqualsNode	cons(Object hd, JMLListEqualsNode tl)           Return a JMLListEqualsNode containing the given element followed by the given list.
private static boolean	elem_equals(Object item1, Object item2)           Tell if the given elements are equal, taking null into account.
boolean	equals(Object ls2)           Test whether this object's value is equal to the given argument.
Object	getItem(Object item)           Return the zero-based index of the first occurrence of the given element in the list, if there is one
boolean	has(Object item)           Tells whether the given element is ".equals" to an element in the list.
int	hashCode()           Return a hash code for this object.
Object	head()           Return the first element in this list.
boolean	headEquals(Object item)           Tell if the head of the list is ".equals" to the given item.
int	indexOf(Object item)           Return the zero-based index of the first occurrence of the given element in the list, if there is one
JMLListEqualsNode	insertBefore(int n, Object 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(JMLListEqualsNode ls2)           Tells whether the elements of this list occur, in order, at the beginning of the given list, using ".equals" for comparisons.
Object	itemAt(int i)           Return the ith element of a list.
Object	last()           Return the last element in this list.
JMLListEqualsNode	prefix(int n)           Return a list containing the first n elements in this list.
JMLListEqualsNode	prepend(Object item)           Return a list that is like this, but with the given item at the front.
JMLListEqualsNode	remove(Object item)           Return a list that is like this list but without the first occurrence of the given item.
JMLListEqualsNode	removeItemAt(int n)           Return a list like this list, but without the element at the given zero-based index.
JMLListEqualsNode	removeLast()           Return a list containing all but the last element in this.
JMLListEqualsNode	removePrefix(int n)           Return a list containing all but the first n elements in this list.
JMLListEqualsNode	replaceItemAt(int n, Object item)           Return a list like this, but with item replacing the element at the given zero-based index.
JMLListEqualsNode	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 Object val

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

next

public final JMLListEqualsNode next

The next node in this list.

JMLListEqualsNode

public JMLListEqualsNode(Object item,
                         JMLListEqualsNode nxt)

The type of the elements in this list. This type is an upper bound on the element's types. The type is computed pessimistically, so that the order of adding elements does not matter; that is, if any element in the list is null, then we use Object as the type of the list's elements. Whether this list can contain null elements; Initialize this list to have the given item as its first element followed by the given list. This does not do any cloning.

Parameters:

item - the object to place at the head of this list.

nxt - the _JMLListEqualsNode to make the tail of this list.

cons

public static JMLListEqualsNode cons(Object hd,
                                     JMLListEqualsNode tl)

Return a JMLListEqualsNode 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 object to place at the head of the result.

tl - the JMLListEqualsNode to make the tail of the result.

head

public Object head()

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

headEquals

public boolean headEquals(Object item)

Tell if the head of the list is ".equals" to the given item.

See Also:

has(Object)

elem_equals

private static boolean elem_equals(Object item1,
                                   Object item2)

Tell if the given elements are equal, taking null into account.

itemAt

public Object 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(Object item)

Tells whether the given element is ".equals" to an element in the list.

isPrefixOf

public boolean isPrefixOf(JMLListEqualsNode 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 JMLType

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

Return the zero-based index of the first occurrence of the given element in the list, if there is one

Parameters:

item - the Object 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 Object last()

Return the last element in this list.

getItem

public Object getItem(Object 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 Object 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:

itemAt(int)

clone

public Object clone()

Return a clone of this object.

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

prefix

public JMLListEqualsNode 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 JMLListEqualsNode 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 JMLListEqualsNode 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 JMLListEqualsNode replaceItemAt(int n,
                                       Object 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 JMLListEqualsNode removeLast()

Return a list containing all but the last element in this.

concat

public JMLListEqualsNode concat(JMLListEqualsNode 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 JMLListEqualsNode prepend(Object 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 JMLListEqualsNode append(Object item)

Return a list that consists of this list and the given element.

reverse

public JMLListEqualsNode reverse()

Return a list that is the reverse of this list.

insertBefore

public JMLListEqualsNode insertBefore(int n,
                                      Object 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 JMLListEqualsNode remove(Object 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