org.jmlspecs.models
Class JMLEqualsSet

java.lang.Object
  org.jmlspecs.models.JMLEqualsSet

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, Serializable

public class JMLEqualsSet

extends Object

implements JMLCollection

Sets of objects. This type uses ".equals" to compare elements, and does not clone elements that are passed into and returned from the set's methods.

For the purposes of informal specification in the methods below, we assume there is a model field

public model mathematical_set theSet;

Version:

$Revision: 1.83 $

Author:

Gary T. Leavens, with help from Albert Baker, Clyde Ruby, and others.

See Also:

JMLCollection, JMLType, JMLObjectSet, JMLValueSet, JMLEqualsSetEnumerator, JMLObjectBag, JMLEqualsBag, JMLValueBag

Field Summary
static JMLEqualsSet	EMPTY           The empty JMLEqualsSet.
protected  int	size           The number of elements in this set.
protected  JMLListEqualsNode	the_list           An equational specification of the properties of sets.

 

Constructor Summary
	JMLEqualsSet()           Initialize this to be an empty set.
	JMLEqualsSet(Object e)           Initialize this to be a singleton set containing the given element.
protected	JMLEqualsSet(JMLListEqualsNode ls)           Initialize this set with the given list.
protected	JMLEqualsSet(JMLListEqualsNode ls, int sz)           Initialize this set with the given instance variables.

 

Method Summary
Object	choose()           Return an arbitrary element of this.
Object	clone()           Return a clone of this object.
boolean	containsAll(Collection c)           Tell whether, for each element in the given collection, there is a ".equals" element in this set.
static JMLEqualsSet	convertFrom(Object[] a)           Return the set containing all the elements in the given array.
static JMLEqualsSet	convertFrom(Collection c)           Return the set containing all the object in the given collection.
static JMLEqualsSet	convertFrom(JMLCollection c)           Return the set containing all the object in the given JMLCollection.
JMLEqualsSet	difference(JMLEqualsSet s2)           Returns a new set that contains all the elements that are in this but not in the given argument.
JMLEqualsSetEnumerator	elements()           Returns an Enumeration over this set.
boolean	equals(Object s2)           Test whether this object's value is equal to the given argument.
protected  JMLEqualsSet	fast_insert(Object elem)           Returns a new set that contains all the elements of this and also the given argument, assuming the argument is not in the set.
boolean	has(Object elem)           Is the argument ".equals" to one of the objects in theSet.
int	hashCode()           Return a hash code for this object.
JMLEqualsSet	insert(Object elem)           Returns a new set that contains all the elements of this and also the given argument.
int	int_size()           Tells the number of elements in the set.
JMLEqualsSet	intersection(JMLEqualsSet s2)           Returns a new set that contains all the elements that are in both this and the given argument.
boolean	isEmpty()           Is the set empty.
boolean	isProperSubset(JMLEqualsSet s2)           Tells whether this set is a subset of but not equal to the argument.
boolean	isProperSuperset(JMLEqualsSet s2)           Tells whether this set is a superset of but not equal to the argument.
boolean	isSubset(JMLEqualsSet s2)           Tells whether this set is a subset of or equal to the argument.
boolean	isSuperset(JMLEqualsSet s2)           Tells whether this set is a superset of or equal to the argument.
JMLIterator	iterator()           Returns an Iterator over this set.
JMLEqualsSet	powerSet()           Returns a new set that is the set of all subsets of this.
JMLEqualsSet	remove(Object elem)           Returns a new set that contains all the elements of this except for the given argument.
static JMLEqualsSet	singleton(Object e)           Return the singleton set containing the given element.
Object[]	toArray()           Return a new array containing all the elements of this.
JMLEqualsBag	toBag()           Return a new JMLEqualsBag containing all the elements of this.
JMLEqualsSequence	toSequence()           Return a new JMLEqualsSequence containing all the elements of this.
String	toString()           Return a string representation of this object.
JMLEqualsSet	union(JMLEqualsSet s2)           Returns a new set that contains all the elements that are in either this or the given argument.

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

the_list

protected final JMLListEqualsNode the_list

An equational specification of the properties of sets. The list representing the elements of this set.

size

protected final int size

The number of elements in this set.

EMPTY

public static final JMLEqualsSet EMPTY

The empty JMLEqualsSet.

See Also:

JMLEqualsSet()

JMLEqualsSet

public JMLEqualsSet()

Initialize this to be an empty set.

See Also:

EMPTY

JMLEqualsSet

public JMLEqualsSet(Object e)

Initialize this to be a singleton set containing the given element.

See Also:

singleton(java.lang.Object)

JMLEqualsSet

protected JMLEqualsSet(JMLListEqualsNode ls,
                       int sz)

Initialize this set with the given instance variables.

JMLEqualsSet

protected JMLEqualsSet(JMLListEqualsNode ls)

Initialize this set with the given list.

singleton

public static JMLEqualsSet singleton(Object e)

Return the singleton set containing the given element.

See Also:

JMLEqualsSet(Object)

convertFrom

public static JMLEqualsSet convertFrom(Object[] a)

Return the set containing all the elements in the given array.

convertFrom

public static JMLEqualsSet convertFrom(Collection c)
                                throws ClassCastException

Return the set containing all the object in the given collection.

Throws:

ClassCastException - if some element in c is not an instance of Object.

See Also:

containsAll(java.util.Collection)

convertFrom

public static JMLEqualsSet convertFrom(JMLCollection c)
                                throws ClassCastException

Return the set containing all the object in the given JMLCollection.

Throws:

ClassCastException - if some element in c is not an instance of Object.

has

public boolean has(Object elem)

Is the argument ".equals" to one of the objects in theSet.

Specified by:

has in interface JMLCollection

containsAll

public boolean containsAll(Collection c)

Tell whether, for each element in the given collection, there is a ".equals" element in this set.

Parameters:

c - the collection whose elements are sought.

See Also:

isSuperset(JMLEqualsSet), convertFrom(java.util.Collection)

equals

public boolean equals(Object s2)

Description copied from interface: JMLType

Test whether this object's value is equal to the given argument.

Specified by:

equals in interface JMLType

Overrides:

equals in class Object

hashCode

public int hashCode()

Return a hash code for this object.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object

isEmpty

public boolean isEmpty()

Is the set empty.

See Also:

int_size(), has(Object)

int_size

public int int_size()

Tells the number of elements in the set.

Specified by:

int_size in interface JMLCollection

isSubset

public boolean isSubset(JMLEqualsSet s2)

Tells whether this set is a subset of or equal to the argument.

See Also:

isProperSubset(JMLEqualsSet), isSuperset(JMLEqualsSet)

isProperSubset

public boolean isProperSubset(JMLEqualsSet s2)

Tells whether this set is a subset of but not equal to the argument.

See Also:

isSubset(JMLEqualsSet), isProperSuperset(JMLEqualsSet)

isSuperset

public boolean isSuperset(JMLEqualsSet s2)

Tells whether this set is a superset of or equal to the argument.

See Also:

isProperSuperset(JMLEqualsSet), isSubset(JMLEqualsSet), containsAll(java.util.Collection)

isProperSuperset

public boolean isProperSuperset(JMLEqualsSet s2)

Tells whether this set is a superset of but not equal to the argument.

See Also:

isSuperset(JMLEqualsSet), isProperSubset(JMLEqualsSet)

choose

public Object choose()
              throws JMLNoSuchElementException

Return an arbitrary element of this.

Throws:

JMLNoSuchElementException - if this is empty.

See Also:

isEmpty(), elements()

clone

public Object clone()

Return a clone of this object. This method does not clone the elements of the set.

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

insert

public JMLEqualsSet insert(Object elem)
                    throws IllegalStateException

Returns a new set that contains all the elements of this and also the given argument.

Throws:

IllegalStateException

See Also:

has(Object), remove(Object)

fast_insert

protected JMLEqualsSet fast_insert(Object elem)

Returns a new set that contains all the elements of this and also the given argument, assuming the argument is not in the set.

See Also:

insert(Object)

remove

public JMLEqualsSet remove(Object elem)

Returns a new set that contains all the elements of this except for the given argument.

See Also:

has(Object), insert(Object)

intersection

public JMLEqualsSet intersection(JMLEqualsSet s2)

Returns a new set that contains all the elements that are in both this and the given argument.

See Also:

union(JMLEqualsSet), difference(JMLEqualsSet)

union

public JMLEqualsSet union(JMLEqualsSet s2)
                   throws IllegalStateException

Returns a new set that contains all the elements that are in either this or the given argument.

Throws:

IllegalStateException

See Also:

intersection(JMLEqualsSet), difference(JMLEqualsSet)

difference

public JMLEqualsSet difference(JMLEqualsSet s2)

Returns a new set that contains all the elements that are in this but not in the given argument.

See Also:

union(JMLEqualsSet), difference(JMLEqualsSet)

powerSet

public JMLEqualsSet powerSet()
                      throws IllegalStateException

Returns a new set that is the set of all subsets of this. The implementation is by Tim Wahls.

Throws:

IllegalStateException

toBag

public JMLEqualsBag toBag()

Return a new JMLEqualsBag containing all the elements of this.

See Also:

toSequence()

toSequence

public JMLEqualsSequence toSequence()

Return a new JMLEqualsSequence containing all the elements of this.

See Also:

toBag(), toArray()

toArray

public Object[] toArray()

Return a new array containing all the elements of this.

See Also:

toSequence()

elements

public JMLEqualsSetEnumerator elements()

Returns an Enumeration over this set.

See Also:

iterator()

iterator

public JMLIterator iterator()

Returns an Iterator over this set.

Specified by:

iterator in interface JMLCollection

See Also:

elements()

toString

public String toString()

Return a string representation of this object.

Overrides:

toString in class Object