|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Objectorg.jmlspecs.models.JMLObjectToValueRelationEnumerator
Enumerator for pairs of keys of type Object to
values of type JMLType that form the associations in a
relation.
JMLEnumeration,
JMLValueType,
JMLObjectToValueRelationImageEnumerator,
JMLObjectToValueRelation,
JMLObjectToValueMap,
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 JMLObjectToValueRelationImageEnumerator |
imagePairEnum
An enumerator for the image pairs in this relation. |
protected Object |
key
The current key for pairs being enumerated. |
| Constructor Summary | |
(package private) |
JMLObjectToValueRelationEnumerator(JMLObjectToValueRelation rel)
Initialize this with the given relation. |
protected |
JMLObjectToValueRelationEnumerator(JMLObjectToValueRelationImageEnumerator ipEnum,
JMLValueSetEnumerator 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. |
JMLObjectValuePair |
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 JMLObjectToValueRelationImageEnumerator imagePairEnum
protected Object key
protected JMLValueSetEnumerator imageEnum
| Constructor Detail |
JMLObjectToValueRelationEnumerator(JMLObjectToValueRelation rel)
protected JMLObjectToValueRelationEnumerator(JMLObjectToValueRelationImageEnumerator ipEnum,
JMLValueSetEnumerator 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 JMLObjectValuePair 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 | ||||||||||