pt.ua.base
Class Set<T>

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

Direct Known Subclasses:

ArrayedSet, LinkedSet

public abstract class Set<T>
extends Indexable<T>

Generic set module.

invariant: Indexable

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

Set()

Method Summary

abstract void	add(T e) Adds an element to the set.
abstract void	clear() Empties the set.
void	copy(Set<T> other) Copies a set to this set (deep copy).
abstract Set<T>	deepClone() Clones current list.
boolean	exists(T e) Queries element e existence.
abstract void	remove(T e) Removes element from the set.

Methods inherited from class pt.ua.base.Indexable

headList, itemAt, subList, tailList, toArray, toList, toString

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

Set

public Set()

Method Detail

copy

public void copy(Set<T> other)

Copies a set to this set (deep copy).

requires: other != null
requires: !isLimited() || maxSize() >= other.size()

Parameters:

other - the set to copy from

deepClone

public abstract Set<T> deepClone()

Description copied from class: Listable

Clones current list.

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

Specified by:

deepClone in class Indexable<T>

Returns:

a deep clone of current list

add

public abstract void add(T e)

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

Parameters:

e - the element to insert in set

remove

public abstract void remove(T e)

Removes element from the set.

requires: exists(e)

ensures: !isFull()

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

exists

public boolean exists(T e)

Queries element e existence.

Returns:

true if element exists, false otherwise

clear

public abstract void clear()

Empties the set.

ensures: isEmpty()