JML

org.jmlspecs.models
Class JMLValueSet

java.lang.Object
  extended byorg.jmlspecs.models.JMLValueSetSpecs
      extended byorg.jmlspecs.models.JMLValueSet
All Implemented Interfaces:
Cloneable, JMLCollection, JMLType, JMLValueType, Serializable

public class JMLValueSet
extends JMLValueSetSpecs
implements JMLCollection

Sets of values. This type uses ".equals" to compare elements, and clones 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;
that you can think of as a mathematical set of values.

Version:
$Revision: 1.83 $
Author:
Gary T. Leavens, with help from Albert Baker, Clyde Ruby, and others.
See Also:
JMLCollection, JMLType, JMLEqualsSet, JMLObjectSet, JMLValueSetEnumerator, JMLValueSetSpecs, JMLObjectBag, JMLEqualsBag, JMLValueBag

Field Summary
static JMLValueSet EMPTY
          The empty JMLValueSet.
protected  int size
          The number of elements in this set.
protected  JMLListValueNode the_list
          An equational specification of the properties of sets.
 
Constructor Summary
  JMLValueSet()
          Initialize this to be an empty set.
protected JMLValueSet(JMLListValueNode ls)
          Initialize this set with the given list.
protected JMLValueSet(JMLListValueNode ls, int sz)
          Initialize this set with the given instance variables.
  JMLValueSet(JMLType e)
          Initialize this to be a singleton set containing the given element.
 
Method Summary
 JMLType 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 JMLValueSet convertFrom(Collection c)
          Return the set containing all the value in the given collection.
static JMLValueSet convertFrom(JMLCollection c)
          Return the set containing all the value in the given JMLCollection.
static JMLValueSet convertFrom(JMLType[] a)
          Return the set containing all the elements in the given array.
 JMLValueSet difference(JMLValueSet s2)
          Returns a new set that contains all the elements that are in this but not in the given argument.
 JMLValueSetEnumerator elements()
          Returns an Enumeration over this set.
 boolean equals(Object s2)
          Test whether this object's value is equal to the given argument.
protected  JMLValueSet fast_insert(JMLType 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(JMLType elem)
          Is the argument ".equals" to one of the values in theSet.
 int hashCode()
          Return a hash code for this object.
 JMLValueSet insert(JMLType 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.
 JMLValueSet intersection(JMLValueSet 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(JMLValueSet s2)
          Tells whether this set is a subset of but not equal to the argument.
 boolean isProperSuperset(JMLValueSet s2)
          Tells whether this set is a superset of but not equal to the argument.
 boolean isSubset(JMLValueSet s2)
          Tells whether this set is a subset of or equal to the argument.
 boolean isSuperset(JMLValueSet s2)
          Tells whether this set is a superset of or equal to the argument.
 JMLIterator iterator()
          Returns an Iterator over this set.
 JMLValueSet powerSet()
          Returns a new set that is the set of all subsets of this.
 JMLValueSet remove(JMLType elem)
          Returns a new set that contains all the elements of this except for the given argument.
static JMLValueSet singleton(JMLType e)
          Return the singleton set containing the given element.
 JMLType[] toArray()
          Return a new array containing all the elements of this.
 JMLValueBag toBag()
          Return a new JMLValueBag containing all the elements of this.
 JMLValueSequence toSequence()
          Return a new JMLValueSequence containing all the elements of this.
 String toString()
          Return a string representation of this object.
 JMLValueSet union(JMLValueSet s2)
          Returns a new set that contains all the elements that are in either this or the given argument.
 
Methods inherited from class org.jmlspecs.models.JMLValueSetSpecs
has
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 
Methods inherited from interface org.jmlspecs.models.JMLCollection
has
 

Field Detail

the_list

protected final JMLListValueNode 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 JMLValueSet EMPTY
The empty JMLValueSet.

See Also:
JMLValueSet()
Constructor Detail

JMLValueSet

public JMLValueSet()
Initialize this to be an empty set.

See Also:
EMPTY

JMLValueSet

public JMLValueSet(JMLType e)
Initialize this to be a singleton set containing the given element.

See Also:
singleton(org.jmlspecs.models.JMLType)

JMLValueSet

protected JMLValueSet(JMLListValueNode ls,
                      int sz)
Initialize this set with the given instance variables.


JMLValueSet

protected JMLValueSet(JMLListValueNode ls)
Initialize this set with the given list.

Method Detail

singleton

public static JMLValueSet singleton(JMLType e)
Return the singleton set containing the given element.

See Also:
JMLValueSet(JMLType)

convertFrom

public static JMLValueSet convertFrom(JMLType[] a)
Return the set containing all the elements in the given array.


convertFrom

public static JMLValueSet convertFrom(Collection c)
                               throws ClassCastException
Return the set containing all the value in the given collection.

Throws:
ClassCastException - if some element in c is not an instance of JMLType.
See Also:
containsAll(java.util.Collection)

convertFrom

public static JMLValueSet convertFrom(JMLCollection c)
                               throws ClassCastException
Return the set containing all the value in the given JMLCollection.

Throws:
ClassCastException - if some element in c is not an instance of JMLType.

has

public boolean has(JMLType elem)
Is the argument ".equals" to one of the values in theSet.


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(JMLValueSet), 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(JMLType)

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(JMLValueSet s2)
Tells whether this set is a subset of or equal to the argument.

See Also:
isProperSubset(JMLValueSet), isSuperset(JMLValueSet)

isProperSubset

public boolean isProperSubset(JMLValueSet s2)
Tells whether this set is a subset of but not equal to the argument.

See Also:
isSubset(JMLValueSet), isProperSuperset(JMLValueSet)

isSuperset

public boolean isSuperset(JMLValueSet s2)
Tells whether this set is a superset of or equal to the argument.

See Also:
isProperSuperset(JMLValueSet), isSubset(JMLValueSet), containsAll(java.util.Collection)

isProperSuperset

public boolean isProperSuperset(JMLValueSet s2)
Tells whether this set is a superset of but not equal to the argument.

See Also:
isSuperset(JMLValueSet), isProperSubset(JMLValueSet)

choose

public JMLType 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 clones the elements of the set.

Specified by:
clone in interface JMLType
Specified by:
clone in class JMLValueSetSpecs

insert

public JMLValueSet insert(JMLType elem)
                   throws IllegalStateException
Returns a new set that contains all the elements of this and also the given argument.

Throws:
IllegalStateException
See Also:
has(JMLType), remove(JMLType)

fast_insert

protected JMLValueSet fast_insert(JMLType 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(JMLType)

remove

public JMLValueSet remove(JMLType elem)
Returns a new set that contains all the elements of this except for the given argument.

See Also:
has(JMLType), insert(JMLType)

intersection

public JMLValueSet intersection(JMLValueSet s2)
Returns a new set that contains all the elements that are in both this and the given argument.

See Also:
union(JMLValueSet), difference(JMLValueSet)

union

public JMLValueSet union(JMLValueSet 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(JMLValueSet), difference(JMLValueSet)

difference

public JMLValueSet difference(JMLValueSet s2)
Returns a new set that contains all the elements that are in this but not in the given argument.

See Also:
union(JMLValueSet), difference(JMLValueSet)

powerSet

public JMLValueSet 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 JMLValueBag toBag()
Return a new JMLValueBag containing all the elements of this.

See Also:
toSequence()

toSequence

public JMLValueSequence toSequence()
Return a new JMLValueSequence containing all the elements of this.

See Also:
toBag(), toArray()

toArray

public JMLType[] toArray()
Return a new array containing all the elements of this.

See Also:
toSequence()

elements

public JMLValueSetEnumerator 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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.