pt.ua.base
Class ArrayedSet<T>

java.lang.Object
  pt.ua.base.Listable<T>
      pt.ua.base.Indexable<T>
          pt.ua.base.Set<T>
              pt.ua.base.ArrayedSet<T>

public class ArrayedSet<T>
extends Set<T>

Set module implemented with an array.

invariant: Set

This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.

Author:

Miguel Oliveira e Silva (mos@ua.pt)

Constructor Summary

ArrayedSet()
Creates an unbounded set.

ArrayedSet(int maxSize)
Creates an bounded set limited to maxSize elements.

Method Summary

void	add(T e) Adds an element to the set.
void	clear() Empties the set.
Set<T>	deepClone() Clones current list.
boolean	isFull() Queries the list fullness.
boolean	isLimited() Checks if list is unbounded.
T	itemAt(int idx) Returns the element of the list at the idx position.
int	maxSize() The list maximum number of elements.
void	remove(T e) Removes element from the set.
int	size() The list total number of elements.

Methods inherited from class pt.ua.base.Set

copy, exists

Methods inherited from class pt.ua.base.Indexable

headList, subList, tailList, toArray, toList, toString

Methods inherited from class pt.ua.base.Listable

isEmpty

Methods inherited from class java.lang.Object

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

Constructor Detail

ArrayedSet

public ArrayedSet()

Creates an unbounded set.

ArrayedSet

public ArrayedSet(int maxSize)

Creates an bounded set limited to maxSize elements.

requires: maxSize >= 0

Method Detail

isLimited

public boolean isLimited()

Description copied from class: Listable

Checks if list is unbounded.

Specified by:

isLimited in class Listable<T>

Returns:

true if list is unbounded, false otherwise

maxSize

public int maxSize()

Description copied from class: Listable

The list maximum number of elements.

requires: isLimited()

Specified by:

maxSize in class Listable<T>

Returns:

list's size

deepClone

public Set<T> deepClone()

Description copied from class: Listable

Clones current list.

ensures: \result.size() == size()

Specified by:

deepClone in class Set<T>

Returns:

a deep clone of current list

add

public void add(T e)

Description copied from class: Set

Adds an element to the set.

requires: !isFull() || exists(e)

ensures: !isEmpty() && exists(e)
ensures: \old(exists(e)) && size() == \old(size()) || !\old(exists(e)) && size() == \old(size()) + 1

Specified by:

add in class Set<T>

Parameters:

e - the element to insert in set

remove

public void remove(T e)

Description copied from class: Set

Removes element from the set.

requires: exists(e)

ensures: !isFull()

ensures: !exists(e)
ensures: size() == \old(size()) - 1

Specified by:

remove in class Set<T>

size

public int size()

Description copied from class: Listable

The list total number of elements.

Specified by:

size in class Listable<T>

Returns:

list's size

isFull

public boolean isFull()

Description copied from class: Listable

Queries the list fullness.

Specified by:

isFull in class Listable<T>

Returns:

true if list is full, false otherwise

itemAt

public T itemAt(int idx)

Description copied from class: Indexable

Returns the element of the list at the idx position.

requires: idx >= 0 && idx < size()

Specified by:

itemAt in class Indexable<T>

Parameters:

idx - the index

Returns:

the element

clear

public void clear()

Description copied from class: Set

Empties the set.

ensures: isEmpty()

Specified by:

clear in class Set<T>