FlexOr.container
Class DLList

java.lang.Object
  FlexOr.container.DLList

All Implemented Interfaces:

Container, Sequence, java.lang.Cloneable

public class DLList
extends java.lang.Object
implements Sequence

Implementation of a sequence of objects as a doubly linked list.

Version:

1.0 1999 Jan 16

Author:

Gunnar Gotshalks

See Also:

Sequence

Constructor Summary

DLList()
Establish the class invariant on an empty list.

Method Summary

void	add(java.lang.Object obj) Adds obj after the last element of the list.
java.lang.Object	clone() Return a copy of the list with new nodes that point to the same objects as in the original list.
boolean	contains(java.lang.Object obj) Determines whether an element is in the sequence[first..last].
boolean	contains(java.lang.Object obj, int startIndex) Determines whether an element is in sequence[startIndex..last].
java.lang.Object	elementAt(int index) Return the element at the specified index.
java.util.Enumeration<java.lang.Object>	elements() Returns an enumerator from the current position.
boolean	equals(java.lang.Object list) Check for equality of contents of two lists.
java.lang.Object	firstElement() Return the first element in the list.
int	indexOf(java.lang.Object obj) Return the index of the specified element.
int	indexOf(java.lang.Object obj, int startIndex) Return the index of the specified element between the start index and the end of the sequence.
void	insertAt(java.lang.Object obj, int index) Insert the element at the specified index.
boolean	isEmpty() Returns true if the list is empty.
boolean	isFull() Returns false as a list can never become full.
java.lang.Object	lastElement() Return the last element in the list.
java.lang.Object	remove() Remove the first element in the sequence.
boolean	remove(java.lang.Object obj) If obj is found remove it from the container.
void	removeAll() Empty the container.
void	removeAt(int index) Remove the element at the specified index.
void	setAt(java.lang.Object obj, int index) Replace the object at the specified index.
int	size() Return the number of elements in the list.
java.lang.String	toString() Return a string representation of the contents of the list.

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

DLList

public DLList()

Establish the class invariant on an empty list.

Class invariant
To simplify assertions we assume sequence[-1] exists for all sequences. It is implemented by a dummy header node. Also we assume sequence[size] exists for all sequences. It is implemented by a dummy trailer node.

  header.previous = trailer.next = null
  length = 0 <=>  current = header.next = trailer && trailer.previous = header
  sequence[-1] = header
  sequence[size] = trailer

Method Detail

contains

public boolean contains(java.lang.Object obj)

Determines whether an element is in the sequence[first..last]. It is O(length) as the list must be searched sequentially.

Requires: True
Ensures: contains(obj) => result = true
            not contains(obj) => result = false

Specified by:

contains in interface Container

contains

public boolean contains(java.lang.Object obj,
                        int startIndex)

Determines whether an element is in sequence[startIndex..last]. It is O(length) as the list must be searched.

Requires: True
Ensures:
       sequence[startIndex..length-1].contains(obj) => result = true
   not sequence[startIndex..length-1].contains(obj) => result = false

elements

public java.util.Enumeration<java.lang.Object> elements()

Returns an enumerator from the current position. The enumeration class is anonymous as we only need a single instance.

Requires: True
Ensures: enumeration over the elements first to last. 

Specified by:

elements in interface Container

Throws:

java.util.NoSuchElementException - when nextElement is called with an empty enumeration sequence.

elementAt

public java.lang.Object elementAt(int index)

Return the element at the specified index. It is O(length) due to the neead to sequentially scan the list.

Requires: 0 <= index < size
Ensures: result = sequence[index]

Specified by:

elementAt in interface Sequence

Throws:

SequenceIndexException - when index is out of bounds.

firstElement

public java.lang.Object firstElement()

Return the first element in the list.

Requires: True
Ensures: length > 0 => result = sequence[first]
                length = 0 => result = null

Specified by:

firstElement in interface Sequence

indexOf

public int indexOf(java.lang.Object obj)

Return the index of the specified element. The operation is O(length). the last.

Requires: True
Ensures: contains(obj) => obj = sequence[result]
            not contains(obj) => result = -1

Specified by:

indexOf in interface Sequence

indexOf

public int indexOf(java.lang.Object obj,
                   int startIndex)

Return the index of the specified element between the start index and the end of the sequence.

Requires: True
Ensures: 
       sequence[startIndex..size-1].contains(obj) => obj = sequence[result]
   not sequence[startIndex..size-1].contains(obj) => result = -1

Specified by:

indexOf in interface Sequence

isEmpty

public boolean isEmpty()

Returns true if the list is empty.

Requires: True
Ensures: isEmpty = (length = 0)

Specified by:

isEmpty in interface Container

isFull

public boolean isFull()

Returns false as a list can never become full.

Requires: True
Ensures: isFull = false

Specified by:

isFull in interface Container

lastElement

public java.lang.Object lastElement()

Return the last element in the list.

Requires: True
Ensures: isEmpty => result = null
            ~isEmpty => result = sequence[last]

Specified by:

lastElement in interface Sequence

size

public int size()

Return the number of elements in the list.

Requires: True
Ensures: result = length

Specified by:

size in interface Container

add

public void add(java.lang.Object obj)

Adds obj after the last element of the list.

Requires: True
Ensures: sequence = old sequence ^ obj

Specified by:

add in interface Container

insertAt

public void insertAt(java.lang.Object obj,
                     int index)

Insert the element at the specified index. We permit index to be size -- instead of size - 1 -- to specify adding at the end of the list.

Requires: 0 <= index < old size + 1
Ensures:
    sequence = old sequence[first..index-1] ^ obj ^ old sequence[index..last]

Specified by:

insertAt in interface Sequence

Throws:

SequenceIndexException - when index is out of bounds.

removeAll

public void removeAll()

Empty the container.

Requires: True
Ensures: sequence = null // the empty sequence.

Specified by:

removeAll in interface Container

remove

public java.lang.Object remove()

Remove the first element in the sequence.

Requires: isEmpty = false
Ensures: old sequence = obj ^ sequence

Specified by:

remove in interface Container

remove

public boolean remove(java.lang.Object obj)

If obj is found remove it from the container.

Requires: True
Ensures:
    old sequence.contains(obj) => sequence = old sequence / obj and result = true 
not old sequence.contains(obj) => sequence = old sequence and result = false

Specified by:

remove in interface Sequence

removeAt

public void removeAt(int index)

Remove the element at the specified index.

Requires: 0 <= index < size
Ensures:
    sequence = old sequence[first..index-1] ^ old sequence[index+1..last]

Specified by:

removeAt in interface Sequence

Throws:

SequenceIndexException - when index is out of bounds.

setAt

public void setAt(java.lang.Object obj,
                  int index)

Replace the object at the specified index.

Requires: 0 <= index < size
Ensures: sequence[index].datum = obj

Specified by:

setAt in interface Sequence

Throws:

SequenceIndexException - when index is out of bounds.

clone

public java.lang.Object clone()

Return a copy of the list with new nodes that point to the same objects as in the original list. Part way between a shallow and deep copy. This is equivalent to how a Vector is cloned.

Requires: True
Ensures: result = copy of sequence

Specified by:

clone in interface Container

Overrides:

clone in class java.lang.Object

toString

public java.lang.String toString()

Return a string representation of the contents of the list.

Requires: True
Ensures: result = string representation of list

Specified by:

toString in interface Container

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object list)

Check for equality of contents of two lists. By equality we mean and equal sequence of elements as returned by the Enumerator for each list.

Requires: True
Ensures: result = true => sequences are equal
                result = false => sequences are not equal

Specified by:

equals in interface Container

Overrides:

equals in class java.lang.Object