|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectpt.ua.base.Listable<T>
pt.ua.base.Indexable<T>
public abstract class Indexable<T>
Generic indexable list.
invariant: Listable
This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.
Constructor Summary | |
---|---|
Indexable()
|
Method Summary | |
---|---|
abstract Indexable<T> |
deepClone()
Clones current list. |
ImmutableList<T> |
headList(int end)
Extracts the elements contained in the interval [0, end[ . |
abstract T |
itemAt(int idx)
Returns the element of the list at the idx position. |
ImmutableList<T> |
subList(int start,
int end)
Extracts the elements contained in the interval [start, end[ . |
ImmutableList<T> |
tailList(int start)
Extracts the elements contained in the interval [start, size()[ . |
Array<T> |
toArray()
Extracts all the elements of the list. |
ImmutableList<T> |
toList()
Extracts all the elements of the list. |
java.lang.String |
toString()
Returns a String with all the list elements separated with a space. |
Methods inherited from class pt.ua.base.Listable |
---|
isEmpty, isFull, isLimited, maxSize, size |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
Constructor Detail |
---|
public Indexable()
Method Detail |
---|
public abstract T itemAt(int idx)
idx
position.
requires: idx >= 0 && idx < size()
idx
- the index
public abstract Indexable<T> deepClone()
Listable
ensures: \result.size() == size()
deepClone
in class Listable<T>
public ImmutableList<T> toList()
Listable
ensures: \result.size == size()
toList
in class Listable<T>
public Array<T> toArray()
Listable
ensures: \result.size() == size()
toArray
in class Listable<T>
public ImmutableList<T> subList(int start, int end)
[start, end[
.
requires: start >= 0 && start <= size()
requires: end >= 0 && end <= size()
ensures: \result.size == end-start
start
- the start indexend
- the first index after the last selected element
public ImmutableList<T> headList(int end)
[0, end[
.
requires: end >= 0 && end <= size()
ensures: \result.size == end
end
- the first index after the last selected element
public ImmutableList<T> tailList(int start)
[start, size()[
.
requires: start >= 0 && start <= size()
ensures: \result.size == size()-start
start
- the start index
public java.lang.String toString()
String
with all the list elements separated with a space.
toString
in class java.lang.Object
|
||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES All Classes | |||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |