org.jmlspecs.models
Class JMLEqualsBag

java.lang.Object
  org.jmlspecs.models.JMLEqualsBag

All Implemented Interfaces:

Cloneable, JMLCollection, JMLType, Serializable

public class JMLEqualsBag

extends Object

implements JMLCollection

Bags (i.e., multisets) of objects. This type uses ".equals" to compare elements, and does not clone 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, JMLValueBag, JMLEqualsBagEnumerator, JMLObjectSet, JMLValueSet

Field Summary
static JMLEqualsBag	EMPTY           The empty JMLEqualsBag.
protected  int	size           The size of this bag.
protected  JMLEqualsBagEntryNode	the_list           The list representing the contents of this bag.

 

Constructor Summary
	JMLEqualsBag()           An equational specification of the properties of bags.
	JMLEqualsBag(Object elem)           Initialize this bag to contain the given element.
protected	JMLEqualsBag(JMLEqualsBagEntryNode ls, int sz)           Initialize this bag with the given representation.

 

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 bag.
static JMLEqualsBag	convertFrom(Object[] a)           Return the bag containing all the elements in the given array.
static JMLEqualsBag	convertFrom(Collection c)           Return the bag containing all the object in the given collection.
static JMLEqualsBag	convertFrom(JMLCollection c)           Return the bag containing all the object in the given JMLCollection.
int	count(Object elem)           Tell how many times the given element occurs ".equals" to an element in this bag.
JMLEqualsBag	difference(JMLEqualsBag b2)           Return a bag containing the items in this bag minus the items in the given bag.
JMLEqualsBagEnumerator	elements()           Returns an Enumeration over this bag.
boolean	equals(Object b2)           Test whether this object's value is equal to the given argument.
protected  JMLEqualsBagEntry	getMatchingEntry(Object item)           Find a JMLEqualsBagEntry that is for the same element, if possible.
boolean	has(Object elem)           Tell whether the given element occurs ".equals" to an element in this bag.
int	hashCode()           Return a hash code for this object
JMLEqualsBag	insert(Object elem)           Return a bag containing the given item and the ones in this bag.
JMLEqualsBag	insert(Object 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.
JMLEqualsBag	intersection(JMLEqualsBag 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(JMLEqualsBag b2)           Tells whether every item in this bag is contained in the argument, but the argument is strictly larger.
boolean	isProperSuperbag(JMLEqualsBag b2)           Tells whether every item in the argument is contained in this bag argument, but this bag is strictly larger.
boolean	isSubbag(JMLEqualsBag b2)           Tells whether every item in this bag is contained in the argument.
boolean	isSuperbag(JMLEqualsBag b2)           Tells whether every item in the argument is contained in this bag.
JMLIterator	iterator()           Returns an iterator over this bag.
JMLEqualsBag	remove(Object elem)           Return a bag containing the items in this bag except for one of the given element.
JMLEqualsBag	remove(Object elem, int cnt)           Return a bag containing the items in this bag, except for the given number of the given element.
JMLEqualsBag	removeAll(Object elem)           Return a bag containing the items in this bag, except for all items that are ".equals" to the given item.
static JMLEqualsBag	singleton(Object e)           Return the singleton bag containing the given element.
Object[]	toArray()           Return a new array containing all the elements of this.
JMLEqualsSequence	toSequence()           Return a new JMLEqualsSequence containing all the elements of this.
JMLEqualsSet	toSet()           Return a new JMLEqualsSet containing all the elements of this.
String	toString()           Return a string representation of this object.
JMLEqualsBag	union(JMLEqualsBag b2)           Return a bag containing the items in either this bag or the given bag.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

the_list

protected final JMLEqualsBagEntryNode the_list

The list representing the contents of this bag. Each element of this list is of type JMLEqualsBagEntry.

size

protected final int size

The size of this bag.

EMPTY

public static final JMLEqualsBag EMPTY

The empty JMLEqualsBag.

See Also:

JMLEqualsBag()

JMLEqualsBag

public JMLEqualsBag()

An equational specification of the properties of bags. Initialize this bag to be empty.

See Also:

EMPTY

JMLEqualsBag

public JMLEqualsBag(Object elem)

Initialize this bag to contain the given element.

Parameters:

elem - the element that is the sole contents of this bag.

See Also:

singleton(java.lang.Object)

JMLEqualsBag

protected JMLEqualsBag(JMLEqualsBagEntryNode ls,
                       int sz)

Initialize this bag with the given representation.

singleton

public static JMLEqualsBag singleton(Object e)

Return the singleton bag containing the given element.

See Also:

JMLEqualsBag(Object)

convertFrom

public static JMLEqualsBag convertFrom(Object[] a)

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

convertFrom

public static JMLEqualsBag convertFrom(Collection c)
                                throws ClassCastException

Return the bag 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 JMLEqualsBag convertFrom(JMLCollection c)
                                throws ClassCastException

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

Throws:

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

count

public int count(Object 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(Object)

has

public boolean has(Object elem)

Tell whether the given element occurs ".equals" to an element in this bag.

Specified by:

has in interface JMLCollection

Parameters:

elem - the element sought.

See Also:

count(Object)

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(JMLEqualsSet), 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(Object)

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(JMLEqualsBag b2)

Tells whether every item in this bag is contained in the argument.

See Also:

isProperSubbag(JMLEqualsBag), isSuperbag(JMLEqualsBag)

isProperSubbag

public boolean isProperSubbag(JMLEqualsBag b2)

Tells whether every item in this bag is contained in the argument, but the argument is strictly larger.

See Also:

isSubbag(JMLEqualsBag), isProperSuperbag(JMLEqualsBag)

isSuperbag

public boolean isSuperbag(JMLEqualsBag b2)

Tells whether every item in the argument is contained in this bag.

See Also:

isProperSuperbag(JMLEqualsBag), isSubbag(JMLEqualsBag), containsAll(java.util.Collection)

isProperSuperbag

public boolean isProperSuperbag(JMLEqualsBag b2)

Tells whether every item in the argument is contained in this bag argument, but this bag is strictly larger.

See Also:

isSuperbag(JMLEqualsBag), isProperSubbag(JMLEqualsBag)

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

Specified by:

clone in interface JMLType

Overrides:

clone in class Object

getMatchingEntry

protected JMLEqualsBagEntry getMatchingEntry(Object item)

Find a JMLEqualsBagEntry 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 JMLEqualsBag insert(Object elem)
                    throws IllegalStateException

Return a bag containing the given item and the ones in this bag.

Throws:

IllegalStateException

See Also:

insert(Object, int), has(Object), remove(Object)

insert

public JMLEqualsBag insert(Object 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(Object), has(Object), remove(Object, int)

remove

public JMLEqualsBag remove(Object elem)

Return a bag containing the items in this bag except for one of the given element.

See Also:

remove(Object, int), insert(Object)

remove

public JMLEqualsBag remove(Object 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(Object), insert(Object, int)

removeAll

public JMLEqualsBag removeAll(Object elem)

Return a bag containing the items in this bag, except for all items that are ".equals" to the given item.

See Also:

remove(Object), remove(Object, int)

intersection

public JMLEqualsBag intersection(JMLEqualsBag 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(JMLEqualsBag), difference(JMLEqualsBag)

union

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

difference

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

toSequence

public JMLEqualsSequence toSequence()

Return a new JMLEqualsSequence containing all the elements of this.

See Also:

toArray(), toSet()

toSet

public JMLEqualsSet toSet()

Return a new JMLEqualsSet containing all the elements of this.

See Also:

toSequence()

toArray

public Object[] toArray()

Return a new array containing all the elements of this.

See Also:

toSequence()

elements

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