JML

org.jmlspecs.models
Class JMLValueBag

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

public class JMLValueBag
extends JMLValueBagSpecs
implements JMLCollection

Bags (i.e., multisets) of values. This type uses ".equals" to compare elements, and clones elements that are passed into and returned from the bag's methods.

Version:
$Revision: 1.70 $
Author:
Gary T. Leavens, with help from Albert Baker, Clyde Ruby, and others.
See Also:
JMLCollection, JMLType, JMLObjectBag, JMLValueBagEnumerator, JMLValueBagSpecs, JMLObjectSet, JMLValueSet

Field Summary
static JMLValueBag EMPTY
          The empty JMLValueBag.
protected  int size
          The size of this bag.
protected  JMLValueBagEntryNode the_list
          The list representing the contents of this bag.
 
Constructor Summary
  JMLValueBag()
          An equational specification of the properties of bags.
  JMLValueBag(JMLType elem)
          Initialize this bag to contain the given element.
protected JMLValueBag(JMLValueBagEntryNode ls, int sz)
          Initialize this bag with the given representation.
 
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 bag.
static JMLValueBag convertFrom(Collection c)
          Return the bag containing all the value in the given collection.
static JMLValueBag convertFrom(JMLCollection c)
          Return the bag containing all the value in the given JMLCollection.
static JMLValueBag convertFrom(JMLType[] a)
          Return the bag containing all the elements in the given array.
 int count(JMLType elem)
          Tell how many times the given element occurs ".equals" to an element in this bag.
 JMLValueBag difference(JMLValueBag b2)
          Return a bag containing the items in this bag minus the items in the given bag.
 JMLValueBagEnumerator elements()
          Returns an Enumeration over this bag.
 boolean equals(Object b2)
          Test whether this object's value is equal to the given argument.
protected  JMLValueBagEntry getMatchingEntry(JMLType item)
          Find a JMLValueBagEntry that is for the same element, if possible.
 boolean has(JMLType elem)
          Tell whether the given element occurs ".equals" to an element in this bag.
 int hashCode()
          Return a hash code for this object
 JMLValueBag insert(JMLType elem)
          Return a bag containing the given item and the ones in this bag.
 JMLValueBag insert(JMLType elem, int cnt)
          Return a bag containing the given item the given number of times, in addition to the ones in this bag.
 int int_size()
          Tell the number of elements in this bag.
 JMLValueBag intersection(JMLValueBag b2)
          Return a bag containing the items in both this bag and the given bag.
 boolean isEmpty()
          Tell whether this bag has no elements.
 boolean isProperSubbag(JMLValueBag b2)
          Tells whether every item in this bag is contained in the argument, but the argument is strictly larger.
 boolean isProperSuperbag(JMLValueBag b2)
          Tells whether every item in the argument is contained in this bag argument, but this bag is strictly larger.
 boolean isSubbag(JMLValueBag b2)
          Tells whether every item in this bag is contained in the argument.
 boolean isSuperbag(JMLValueBag b2)
          Tells whether every item in the argument is contained in this bag.
 JMLIterator iterator()
          Returns an iterator over this bag.
 JMLValueBag remove(JMLType elem)
          Return a bag containing the items in this bag except for one of the given element.
 JMLValueBag remove(JMLType elem, int cnt)
          Return a bag containing the items in this bag, except for the given number of the given element.
 JMLValueBag removeAll(JMLType elem)
          Return a bag containing the items in this bag, except for all items that are ".equals" to the given item.
static JMLValueBag singleton(JMLType e)
          Return the singleton bag containing the given element.
 JMLType[] toArray()
          Return a new array containing all the elements of this.
 JMLValueSequence toSequence()
          Return a new JMLValueSequence containing all the elements of this.
 JMLValueSet toSet()
          Return a new JMLValueSet containing all the elements of this.
 String toString()
          Return a string representation of this object.
 JMLValueBag union(JMLValueBag b2)
          Return a bag containing the items in either this bag or the given bag.
 
Methods inherited from class org.jmlspecs.models.JMLValueBagSpecs
count, 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 JMLValueBagEntryNode the_list
The list representing the contents of this bag. Each element of this list is of type JMLValueBagEntry.


size

protected final int size
The size of this bag.


EMPTY

public static final JMLValueBag EMPTY
The empty JMLValueBag.

See Also:
JMLValueBag()
Constructor Detail

JMLValueBag

public JMLValueBag()
An equational specification of the properties of bags. Initialize this bag to be empty.

See Also:
EMPTY

JMLValueBag

public JMLValueBag(JMLType elem)
Initialize this bag to contain the given element.

Parameters:
elem - the element that is the sole contents of this bag.
See Also:
singleton(org.jmlspecs.models.JMLType)

JMLValueBag

protected JMLValueBag(JMLValueBagEntryNode ls,
                      int sz)
Initialize this bag with the given representation.

Method Detail

singleton

public static JMLValueBag singleton(JMLType e)
Return the singleton bag containing the given element.

See Also:
JMLValueBag(JMLType)

convertFrom

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


convertFrom

public static JMLValueBag convertFrom(Collection c)
                               throws ClassCastException
Return the bag 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 JMLValueBag convertFrom(JMLCollection c)
                               throws ClassCastException
Return the bag containing all the value in the given JMLCollection.

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

count

public int count(JMLType elem)
Tell how many times the given element occurs ".equals" to an element in this bag.

Parameters:
elem - the element sought.
Returns:
the number of times elem occurs in this bag.
See Also:
has(JMLType)

has

public boolean has(JMLType elem)
Tell whether the given element occurs ".equals" to an element in this bag.

Parameters:
elem - the element sought.
See Also:
count(JMLType)

containsAll

public boolean containsAll(Collection c)
Tell whether, for each element in the given collection, there is a ".equals" element in this bag.

Parameters:
c - the collection whose elements are sought.
See Also:
#isSuperbag(JMLValueSet), convertFrom(java.util.Collection)

equals

public boolean equals(Object b2)
Test whether this object's value is equal to the given argument. This comparison uses ".equals" to compare elements.

Note that the elementTypes may be different for otherwise equal bags.

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()
Tell whether this bag has no elements.

See Also:
int_size(), has(JMLType)

int_size

public int int_size()
Tell the number of elements in this bag.

Specified by:
int_size in interface JMLCollection

isSubbag

public boolean isSubbag(JMLValueBag b2)
Tells whether every item in this bag is contained in the argument.

See Also:
isProperSubbag(JMLValueBag), isSuperbag(JMLValueBag)

isProperSubbag

public boolean isProperSubbag(JMLValueBag b2)
Tells whether every item in this bag is contained in the argument, but the argument is strictly larger.

See Also:
isSubbag(JMLValueBag), isProperSuperbag(JMLValueBag)

isSuperbag

public boolean isSuperbag(JMLValueBag b2)
Tells whether every item in the argument is contained in this bag.

See Also:
isProperSuperbag(JMLValueBag), isSubbag(JMLValueBag), containsAll(java.util.Collection)

isProperSuperbag

public boolean isProperSuperbag(JMLValueBag b2)
Tells whether every item in the argument is contained in this bag argument, but this bag is strictly larger.

See Also:
isSuperbag(JMLValueBag), isProperSubbag(JMLValueBag)

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 bag.

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

getMatchingEntry

protected JMLValueBagEntry getMatchingEntry(JMLType item)
Find a JMLValueBagEntry that is for the same element, if possible.

Parameters:
item - the item sought.
Returns:
null if the item is not in the bag.

insert

public JMLValueBag insert(JMLType elem)
                   throws IllegalStateException
Return a bag containing the given item and the ones in this bag.

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

insert

public JMLValueBag insert(JMLType elem,
                          int cnt)
                   throws IllegalArgumentException,
                          IllegalStateException
Return a bag containing the given item the given number of times, in addition to the ones in this bag.

Throws:
IllegalArgumentException
IllegalStateException
See Also:
insert(JMLType), has(JMLType), remove(JMLType, int)

remove

public JMLValueBag remove(JMLType elem)
Return a bag containing the items in this bag except for one of the given element.

See Also:
remove(JMLType, int), insert(JMLType)

remove

public JMLValueBag remove(JMLType elem,
                          int cnt)
                   throws IllegalArgumentException
Return a bag containing the items in this bag, except for the given number of the given element.

Throws:
IllegalArgumentException
See Also:
remove(JMLType), insert(JMLType, int)

removeAll

public JMLValueBag removeAll(JMLType elem)
Return a bag containing the items in this bag, except for all items that are ".equals" to the given item.

See Also:
remove(JMLType), remove(JMLType, int)

intersection

public JMLValueBag intersection(JMLValueBag b2)
Return a bag containing the items in both this bag and the given bag. Note that items occur the minimum number of times they occur in both bags.

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

union

public JMLValueBag union(JMLValueBag b2)
Return a bag containing the items in either this bag or the given bag. Note that items occur the sum of times they occur in both bags.

See Also:
intersection(JMLValueBag), difference(JMLValueBag)

difference

public JMLValueBag difference(JMLValueBag b2)
Return a bag containing the items in this bag minus the items in the given bag. If an item occurs in this bag N times, and M times in the given bag, then it occurs N-M times in the result.

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

toSequence

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

See Also:
toArray(), toSet()

toSet

public JMLValueSet toSet()
Return a new JMLValueSet containing all the elements of this.

See Also:
toSequence()

toArray

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

See Also:
toSequence()

elements

public JMLValueBagEnumerator elements()
Returns an Enumeration over this bag.

See Also:
iterator()

iterator

public JMLIterator iterator()
Returns an iterator over this bag.

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.