org.jmlspecs.models
Class JMLObjectBagEnumerator

java.lang.Object
  org.jmlspecs.models.JMLObjectBagEnumerator

All Implemented Interfaces:

Cloneable, Enumeration, JMLEnumeration, JMLObjectType, JMLType, Serializable

public class JMLObjectBagEnumerator

extends Object

implements JMLEnumeration, JMLObjectType

Enumerators for bags (i.e., multisets) of objects.

Version:

$Revision: 1.39 $

Author:

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

See Also:

JMLEnumeration, JMLType, JMLObjectBag, JMLEnumerationToIterator

Field Summary
protected  JMLObjectBag	currentBag           The elements that have not yet been returned by nextElement.
protected  int	currentCount           The remaining count of repetitions that the current entry should be returned.
protected  Object	currEntry           The current entry.

 

Constructor Summary
(package private)	JMLObjectBagEnumerator(JMLObjectBag b)           Initialize this with the given bag.

 

Method Summary
protected  JMLObjectBag	abstractValue()           Return the abstract value of this bag enumerator.
Object	clone()           Return a clone of this enumerator.
boolean	equals(Object oth)           Return true just when this enumerator has the same state as the given argument..
int	hashCode()           Return a hash code for this enumerator.
boolean	hasMoreElements()           Tells whether this enumerator has more uniterated elements.
Object	nextElement()           Return the next element in this, if there is one.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

currentBag

protected JMLObjectBag currentBag

The elements that have not yet been returned by nextElement. The bag underlying this enumerator.

currentCount

protected int currentCount

The remaining count of repetitions that the current entry should be returned.

currEntry

protected Object currEntry

The current entry.

JMLObjectBagEnumerator

JMLObjectBagEnumerator(JMLObjectBag b)

Initialize this with the given bag.

hasMoreElements

public boolean hasMoreElements()

Tells whether this enumerator has more uniterated elements.

Specified by:

hasMoreElements in interface JMLEnumeration

nextElement

public Object nextElement()
                   throws JMLNoSuchElementException

Return the next element in this, if there is one.

Specified by:

nextElement in interface Enumeration

Throws:

JMLNoSuchElementException - when this is empty.

clone

public Object clone()

Return a clone of this enumerator.

Specified by:

clone in interface JMLEnumeration

Overrides:

clone in class Object

abstractValue

protected JMLObjectBag abstractValue()

Return the abstract value of this bag enumerator.

equals

public boolean equals(Object oth)

Return true just when this enumerator has the same state as the given argument..

Specified by:

equals in interface JMLType

Overrides:

equals in class Object

hashCode

public int hashCode()

Return a hash code for this enumerator.

Specified by:

hashCode in interface JMLType

Overrides:

hashCode in class Object