|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Objectorg.jmlspecs.models.JMLObjectBag
Bags (i.e., multisets) of objects. This type uses "==" to compare elements, and does not clone elements that are passed into and returned from the bag's methods.
JMLCollection,
JMLType,
JMLValueSet,
JMLObjectSetEnumerator,
JMLObjectSet,
JMLValueSet| Field Summary | |
static JMLObjectBag |
EMPTY
The empty JMLObjectBag. |
protected int |
size
The size of this bag. |
protected JMLObjectBagEntryNode |
the_list
The list representing the contents of this bag. |
| Constructor Summary | |
|
JMLObjectBag()
An equational specification of the properties of bags. |
|
JMLObjectBag(Object elem)
Initialize this bag to contain the given element. |
protected |
JMLObjectBag(JMLObjectBagEntryNode 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 "==" element in this bag. |
static JMLObjectBag |
convertFrom(Object[] a)
Return the bag containing all the elements in the given array. |
static JMLObjectBag |
convertFrom(Collection c)
Return the bag containing all the object in the given collection. |
static JMLObjectBag |
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 "==" to an element in this bag. |
JMLObjectBag |
difference(JMLObjectBag b2)
Return a bag containing the items in this bag minus the items in the given bag. |
JMLObjectBagEnumerator |
elements()
Returns an Enumeration over this bag. |
boolean |
equals(Object b2)
Test whether this object's value is equal to the given argument. |
protected JMLObjectBagEntry |
getMatchingEntry(Object item)
Find a JMLObjectBagEntry that is for the same element, if possible. |
boolean |
has(Object elem)
Tell whether the given element occurs "==" to an element in this bag. |
int |
hashCode()
Return a hash code for this object |
JMLObjectBag |
insert(Object elem)
Return a bag containing the given item and the ones in this bag. |
JMLObjectBag |
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. |
JMLObjectBag |
intersection(JMLObjectBag 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(JMLObjectBag b2)
Tells whether every item in this bag is contained in the argument, but the argument is strictly larger. |
boolean |
isProperSuperbag(JMLObjectBag b2)
Tells whether every item in the argument is contained in this bag argument, but this bag is strictly larger. |
boolean |
isSubbag(JMLObjectBag b2)
Tells whether every item in this bag is contained in the argument. |
boolean |
isSuperbag(JMLObjectBag b2)
Tells whether every item in the argument is contained in this bag. |
JMLIterator |
iterator()
Returns an iterator over this bag. |
JMLObjectBag |
remove(Object elem)
Return a bag containing the items in this bag except for one of the given element. |
JMLObjectBag |
remove(Object elem,
int cnt)
Return a bag containing the items in this bag, except for the given number of the given element. |
JMLObjectBag |
removeAll(Object elem)
Return a bag containing the items in this bag, except for all items that are "==" to the given item. |
static JMLObjectBag |
singleton(Object e)
Return the singleton bag containing the given element. |
Object[] |
toArray()
Return a new array containing all the elements of this. |
JMLObjectSequence |
toSequence()
Return a new JMLObjectSequence containing all the elements of this. |
JMLObjectSet |
toSet()
Return a new JMLObjectSet containing all the elements of this. |
String |
toString()
Return a string representation of this object. |
JMLObjectBag |
union(JMLObjectBag 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 |
protected final JMLObjectBagEntryNode the_list
protected final int size
public static final JMLObjectBag EMPTY
JMLObjectBag()| Constructor Detail |
public JMLObjectBag()
EMPTYpublic JMLObjectBag(Object elem)
elem - the element that is the sole contents of this bag.singleton(java.lang.Object)
protected JMLObjectBag(JMLObjectBagEntryNode ls,
int sz)
| Method Detail |
public static JMLObjectBag singleton(Object e)
JMLObjectBag(Object)public static JMLObjectBag convertFrom(Object[] a)
public static JMLObjectBag convertFrom(Collection c)
throws ClassCastException
ClassCastException - if some element in c is not an instance of
Object.containsAll(java.util.Collection)
public static JMLObjectBag convertFrom(JMLCollection c)
throws ClassCastException
ClassCastException - if some element in c is not an instance of
Object.public int count(Object elem)
elem - the element sought.
has(Object)public boolean has(Object elem)
has in interface JMLCollectionelem - the element sought.count(Object)public boolean containsAll(Collection c)
c - the collection whose elements are sought.#isSuperbag(JMLObjectSet),
convertFrom(java.util.Collection)public boolean equals(Object b2)
Note that the elementTypes may be different for otherwise equal bags.
equals in interface JMLTypeequals in class Objectpublic int hashCode()
hashCode in interface JMLTypehashCode in class Objectpublic boolean isEmpty()
int_size(),
has(Object)public int int_size()
int_size in interface JMLCollectionpublic boolean isSubbag(JMLObjectBag b2)
isProperSubbag(JMLObjectBag),
isSuperbag(JMLObjectBag)public boolean isProperSubbag(JMLObjectBag b2)
isSubbag(JMLObjectBag),
isProperSuperbag(JMLObjectBag)public boolean isSuperbag(JMLObjectBag b2)
isProperSuperbag(JMLObjectBag),
isSubbag(JMLObjectBag),
containsAll(java.util.Collection)public boolean isProperSuperbag(JMLObjectBag b2)
isSuperbag(JMLObjectBag),
isProperSubbag(JMLObjectBag)
public Object choose()
throws JMLNoSuchElementException
JMLNoSuchElementException - if this is empty.isEmpty(),
elements()public Object clone()
clone in interface JMLTypeclone in class Objectprotected JMLObjectBagEntry getMatchingEntry(Object item)
item - the item sought.
public JMLObjectBag insert(Object elem)
throws IllegalStateException
IllegalStateExceptioninsert(Object, int),
has(Object),
remove(Object)
public JMLObjectBag insert(Object elem,
int cnt)
throws IllegalArgumentException,
IllegalStateException
IllegalArgumentException
IllegalStateExceptioninsert(Object),
has(Object),
remove(Object, int)public JMLObjectBag remove(Object elem)
remove(Object, int),
insert(Object)
public JMLObjectBag remove(Object elem,
int cnt)
throws IllegalArgumentException
IllegalArgumentExceptionremove(Object),
insert(Object, int)public JMLObjectBag removeAll(Object elem)
remove(Object),
remove(Object, int)public JMLObjectBag intersection(JMLObjectBag b2)
union(JMLObjectBag),
difference(JMLObjectBag)public JMLObjectBag union(JMLObjectBag b2)
intersection(JMLObjectBag),
difference(JMLObjectBag)public JMLObjectBag difference(JMLObjectBag b2)
union(JMLObjectBag),
difference(JMLObjectBag)public JMLObjectSequence toSequence()
toArray(),
toSet()public JMLObjectSet toSet()
toSequence()public Object[] toArray()
toSequence()public JMLObjectBagEnumerator elements()
iterator()public JMLIterator iterator()
iterator in interface JMLCollectionelements()public String toString()
toString in class Object
|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||