|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectpt.ua.base.ImmutableList<T>
public class ImmutableList<T>
Generic immutable list module.
This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.
Field Summary | |
---|---|
T |
head
The list head element |
int |
size
The list total number of elements. |
ImmutableList<T> |
tail
The list tail list |
Constructor Summary | |
---|---|
ImmutableList()
Creates an empty list. |
|
ImmutableList(T head,
ImmutableList<T> tail)
Creates a new list by appending tail list to head element. |
Method Summary | |
---|---|
boolean |
equals(ImmutableList<T> other)
Queries equality with other list. |
T |
itemAt(int idx)
Returns the element of the list at the idx position. |
java.lang.String |
toString()
Returns a String with all list's elements separated with a space. |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Field Detail |
---|
public final int size
public final T head
public final ImmutableList<T> tail
Constructor Detail |
---|
public ImmutableList()
ensures: size == 0
ensures: head == null
ensures: tail == null
public ImmutableList(T head, ImmutableList<T> tail)
tail
list to head
element.
requires: tail != null
ensures: size == \old(size)+1
ensures: this.head == head
ensures: this.tail == tail
head
- the elementtail
- an immutable listMethod Detail |
---|
public boolean equals(ImmutableList<T> other)
other
list.
requires: other != null
true
if lists are equal, false
otherwisepublic T itemAt(int idx)
idx
position.
requires: idx >= 0 && idx < size
idx
- the index
public java.lang.String toString()
String
with all list's elements separated with a space.
toString
in class java.lang.Object
|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |