An implementation class used in various models. These are
singly-linked list nodes containing values. The empty
list is represented by null, which makes dealing with these lists
tricky. Normal users should use
JMLValueSequence instead of this
type to avoid these difficulties.
This type uses ".equals" to compare elements. The cons method
clones elements that are passed into the list.
version: $Revision: 1.1.1.1 $ author: Gary T. Leavens author: Albert L. Baker See Also:JMLValueSequence See Also:JMLValueBag See Also:JMLValueSet
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 theresult.
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.
public boolean
equals(Object ls2) Test whether this object's value is equal to the given argument.
insertBefore(int n, JMLType item) Return a list that is like this list but with the given item
inserted before the given index.
public int
int_length() Tells the number of elements in the list; a synonym for size.
public int
int_size() Tells the number of elements in the list; a synonym for length.
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.
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 value to place at the head of this list. Parameters: nxt - the _JMLListValueNode to make the tail of this list.
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 theresult. the concatenation of this list and ls2.
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. Parameters: tl - the JMLListValueNode to make the tail of the result.
Return a list containing the first n elements in this list.
Parameters: n - the number of elements to leave in the result. null if n is not positive or greater than the length of this list.
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.
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. Parameters: item - the item to put at index index