Package components.set

Interface SetKernel<T>

Type Parameters:

T - type of SetKernel elements

All Superinterfaces:

Iterable<T>, Standard<Set<T>>

All Known Subinterfaces:

Set<T>

All Known Implementing Classes:

Set1L, Set2, Set3, Set4, SetSecondary

public interface SetKernel<T>
extends Standard<Set<T>>, Iterable<T>

Set kernel component with primary methods. (Note: by package-wide convention, all references are non-null.)

Mathematical Model (abstract value and abstract invariant of this):

type SetKernel is modeled by finite set of T

Constructor(s) (initial abstract value(s) of this):

():
 ensures
  this = {}

Iterator String (abstract value of ~this):

entries(~this.seen * ~this.unseen) = this  and
|~this.seen * ~this.unseen| = |this|

Method Summary

Modifier and Type	Method	Description
void	add(T x)	Adds x to this.
boolean	contains(T x)	Reports whether x is in this.
T	remove(T x)	Removes x from this, and returns it.
T	removeAny()	Removes and returns an arbitrary element from this.
int	size()	Reports size (cardinality) of this.

Methods inherited from interface java.lang.Iterable

forEach, iterator, spliterator

Methods inherited from interface components.standard.Standard

clear, newInstance, transferFrom

Method Details

add

void add(T x)

Adds x to this.

Parameters:

x - the element to be added

Aliases:

reference x

Updates:

this

Requires:

x is not in this

Ensures:

this = #this union {x}

remove

T remove(T x)

Removes x from this, and returns it.

Parameters:

x - the element to be removed

Returns:

the element removed

Updates:

this

Requires:

x is in this

Ensures:

this = #this \ {x}  and
remove = x

removeAny

T removeAny()

Removes and returns an arbitrary element from this.

Returns:

the element removed from this

Updates:

this

Requires:

|this| > 0

Ensures:

removeAny is in #this and
this = #this \ {removeAny}

contains

boolean contains(T x)

Reports whether x is in this.

Parameters:

x - the element to be checked

Returns:

true iff element is in this

Ensures:

contains = (x is in this)

size

int size()

Reports size (cardinality) of this.

Returns:

the number of elements in this

Ensures:

size = |this|