| java.lang.Object org.jmlspecs.models.JML_Domain_To_Range_RelationImageEnumerator
JML_Domain_To_Range_RelationImageEnumerator | public class JML_Domain_To_Range_RelationImageEnumerator implements JMLEnumeration,JMLValueType(Code) | | Enumerator for pairs of keys and their relational images. This
enumerator returns pairs of type
JML_Domain_ValuePair ,
each of which has a "key" field of type
_DomainType_ and a
"value" field of type
JML_Range_Set s containing
_RangeType_ .
version: $Revision: 1.2 $ author: Gary T. Leavens See Also: JMLEnumeration See Also: JMLValueType See Also: JML_Domain_To_Range_RelationEnumerator See Also: JML_Domain_To_Range_Relation See Also: JML_Domain_To_Range_Map See Also: JMLEnumerationToIterator See Also: JMLValueSet |
Method Summary | |
protected JMLValueSet | abstractValue() Return the set of uniterated pairs from this enumerator. | public Object | clone() Return a clone of this enumerator. | public boolean | equals(Object oth) Return true just when this enumerator has the same state as
the given argument. | public boolean | hasMoreElements() Tells whether this enumerator has more uniterated elements. | public int | hashCode() Return a hash code for this enumerator. | public Object | nextElement() Return the next image pair in this, if there is one. | public JML_Domain_ValuePair | nextImagePair() Return the next image pair in this, if there is one. |
JML_Domain_To_Range_RelationImageEnumerator | JML_Domain_To_Range_RelationImageEnumerator(JML_Domain_To_Range_Relation rel)(Code) | | Initialize this with the given relation.
|
abstractValue | protected JMLValueSet abstractValue()(Code) | | Return the set of uniterated pairs from this enumerator.
|
clone | public Object clone()(Code) | | Return a clone of this enumerator.
|
equals | public boolean equals(Object oth)(Code) | | Return true just when this enumerator has the same state as
the given argument.
|
hasMoreElements | public boolean hasMoreElements()(Code) | | Tells whether this enumerator has more uniterated elements.
See Also: JML_Domain_To_Range_RelationImageEnumerator.nextElement See Also: JML_Domain_To_Range_RelationImageEnumerator.nextImagePair |
hashCode | public int hashCode()(Code) | | Return a hash code for this enumerator.
|
nextElement | public Object nextElement() throws JMLNoSuchElementException(Code) | | Return the next image pair in this, if there is one.
exception: JMLNoSuchElementException - when this is empty. See Also: JML_Domain_To_Range_RelationImageEnumerator.hasMoreElements See Also: JML_Domain_To_Range_RelationImageEnumerator.nextImagePair |
nextImagePair | public JML_Domain_ValuePair nextImagePair() throws JMLNoSuchElementException(Code) | | Return the next image pair in this, if there is one.
exception: JMLNoSuchElementException - when this is empty. See Also: JML_Domain_To_Range_RelationImageEnumerator.hasMoreElements See Also: JML_Domain_To_Range_RelationImageEnumerator.nextElement |
|
|