|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Objectorg.jmlspecs.models.JMLValueToValueRelationEnumerator
Enumerator for pairs of keys of type JMLType to
values of type JMLType that form the associations in a
relation.
JMLEnumeration,
JMLValueType,
JMLValueToValueRelationImageEnumerator,
JMLValueToValueRelation,
JMLValueToValueMap,
JMLEnumerationToIterator,
JMLValueSet| Field Summary | |
protected JMLValueSetEnumerator |
imageEnum
An enumerator for the range elements that are related to the key that have not yet been returned. |
protected JMLValueToValueRelationImageEnumerator |
imagePairEnum
An enumerator for the image pairs in this relation. |
protected JMLType |
key
The current key for pairs being enumerated. |
| Constructor Summary | |
(package private) |
JMLValueToValueRelationEnumerator(JMLValueToValueRelation rel)
Initialize this with the given relation. |
protected |
JMLValueToValueRelationEnumerator(JMLValueToValueRelationImageEnumerator ipEnum,
JMLValueSetEnumerator iEnum,
JMLType 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. |
JMLValueValuePair |
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 JMLValueToValueRelationImageEnumerator imagePairEnum
protected JMLType key
protected JMLValueSetEnumerator imageEnum
| Constructor Detail |
JMLValueToValueRelationEnumerator(JMLValueToValueRelation rel)
protected JMLValueToValueRelationEnumerator(JMLValueToValueRelationImageEnumerator ipEnum,
JMLValueSetEnumerator iEnum,
JMLType 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 JMLValueValuePair 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 | ||||||||||