|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Objectorg.jmlspecs.models.JMLEqualsToObjectRelationEnumerator
Enumerator for pairs of keys of type Object to
values of type Object that form the associations in a
relation.
JMLEnumeration,
JMLValueType,
JMLEqualsToObjectRelationImageEnumerator,
JMLEqualsToObjectRelation,
JMLEqualsToObjectMap,
JMLEnumerationToIterator,
JMLValueSet| Field Summary | |
protected JMLObjectSetEnumerator |
imageEnum
An enumerator for the range elements that are related to the key that have not yet been returned. |
protected JMLEqualsToObjectRelationImageEnumerator |
imagePairEnum
An enumerator for the image pairs in this relation. |
protected Object |
key
The current key for pairs being enumerated. |
| Constructor Summary | |
(package private) |
JMLEqualsToObjectRelationEnumerator(JMLEqualsToObjectRelation rel)
Initialize this with the given relation. |
protected |
JMLEqualsToObjectRelationEnumerator(JMLEqualsToObjectRelationImageEnumerator ipEnum,
JMLObjectSetEnumerator iEnum,
Object k)
|
| Method Summary | |
protected JMLValueSet |
abstractValue()
Return the set of uniterated pairs from this 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 image pair in this, if there is one. |
JMLEqualsObjectPair |
nextPair()
Return the next pair in this, if there is one. |
| Methods inherited from class java.lang.Object |
finalize, getClass, notify, notifyAll, toString, wait, wait, wait |
| Field Detail |
protected JMLEqualsToObjectRelationImageEnumerator imagePairEnum
protected Object key
protected JMLObjectSetEnumerator imageEnum
| Constructor Detail |
JMLEqualsToObjectRelationEnumerator(JMLEqualsToObjectRelation rel)
protected JMLEqualsToObjectRelationEnumerator(JMLEqualsToObjectRelationImageEnumerator ipEnum,
JMLObjectSetEnumerator iEnum,
Object k)
| Method Detail |
public boolean hasMoreElements()
hasMoreElements in interface JMLEnumerationnextElement(),
nextPair()
public Object nextElement()
throws JMLNoSuchElementException
nextElement in interface EnumerationJMLNoSuchElementException - when this is empty.hasMoreElements(),
nextPair()
public JMLEqualsObjectPair nextPair()
throws JMLNoSuchElementException
JMLNoSuchElementException - when this is empty.hasMoreElements(),
nextElement()public Object clone()
clone in interface JMLEnumerationclone in class Objectpublic boolean equals(Object oth)
equals in interface JMLTypeequals in class Objectpublic int hashCode()
hashCode in interface JMLTypehashCode in class Objectprotected JMLValueSet abstractValue()
|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||