|
JML | ||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||||
java.lang.Objectorg.jmlspecs.models.JMLObjectToValueRelationImageEnumerator
Enumerator for pairs of keys and their relational images. This
enumerator returns pairs of type JMLObjectValuePair,
each of which has a "key" field of type Object and a
"value" field of type JMLValueSets containing JMLType.
JMLEnumeration,
JMLValueType,
JMLObjectToValueRelationEnumerator,
JMLObjectToValueRelation,
JMLObjectToValueMap,
JMLEnumerationToIterator,
JMLValueSet| Field Summary | |
protected JMLValueSetEnumerator |
pairEnum
An enumerator for the image pairs in this relation. |
| Constructor Summary | |
(package private) |
JMLObjectToValueRelationImageEnumerator(JMLObjectToValueRelation rel)
Initialize this with the given relation. |
protected |
JMLObjectToValueRelationImageEnumerator(JMLValueSetEnumerator pEnum)
|
| 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 |
nextImagePair()
Return the next image 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 JMLValueSetEnumerator pairEnum
| Constructor Detail |
JMLObjectToValueRelationImageEnumerator(JMLObjectToValueRelation rel)
protected JMLObjectToValueRelationImageEnumerator(JMLValueSetEnumerator pEnum)
| Method Detail |
public boolean hasMoreElements()
hasMoreElements in interface JMLEnumerationnextElement(),
nextImagePair()
public Object nextElement()
throws JMLNoSuchElementException
nextElement in interface EnumerationJMLNoSuchElementException - when this is empty.hasMoreElements(),
nextImagePair()
public JMLObjectValuePair nextImagePair()
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 | ||||||||||