| java.lang.Object org.jmlspecs.models.JML_Elem_SetEnumerator
JML_Elem_SetEnumerator | public class JML_Elem_SetEnumerator implements JMLEnumeration,_SuperType_(Code) | | An enumerator for sets of _ElemType_English_s.
version: $Revision: 1.1 $ author: Gary T. Leavens, with help from Albert Baker, Clyde Ruby, author: and others. See Also: JMLEnumeration See Also: _SuperType_ See Also: JML_Elem_Set See Also: JMLEnumerationToIterator |
Field Summary | |
protected JMLList_Elem_Node | currentNode The list representing the elements that have not yet been
returned by this enumerator. |
Method Summary | |
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 element in this, if there is one. |
currentNode | protected JMLList_Elem_Node currentNode(Code) | | The list representing the elements that have not yet been
returned by this enumerator.
|
JML_Elem_SetEnumerator | JML_Elem_SetEnumerator(JML_Elem_Set s)(Code) | | Initialize this with the given set.
|
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.
|
hashCode | public int hashCode()(Code) | | Return a hash code for this enumerator.
|
|
|