Interface Enumeration

All Known Subinterfaces:
All Known Implementing Classes:
JMLEqualsBagEnumerator, JMLEqualsSequenceEnumerator, JMLEqualsSetEnumerator, JMLEqualsToEqualsRelationEnumerator, JMLEqualsToEqualsRelationImageEnumerator, JMLEqualsToObjectRelationEnumerator, JMLEqualsToObjectRelationImageEnumerator, JMLEqualsToValueRelationEnumerator, JMLEqualsToValueRelationImageEnumerator, JMLObjectBagEnumerator, JMLObjectSequenceEnumerator, JMLObjectSetEnumerator, JMLObjectToEqualsRelationEnumerator, JMLObjectToEqualsRelationImageEnumerator, JMLObjectToObjectRelationEnumerator, JMLObjectToObjectRelationImageEnumerator, JMLObjectToValueRelationEnumerator, JMLObjectToValueRelationImageEnumerator, JMLValueBagEnumerator, JMLValueSequenceEnumerator, JMLValueSetEnumerator, JMLValueToEqualsRelationEnumerator, JMLValueToEqualsRelationImageEnumerator, JMLValueToObjectRelationEnumerator, JMLValueToObjectRelationImageEnumerator, JMLValueToValueRelationEnumerator, JMLValueToValueRelationImageEnumerator

public interface Enumeration

JML's specification of java.util.Enumeration. Some of this specification is taken from ESC/Java.

$Revision: 1.15 $
Gary T. Leavens

Class Specifications

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Model Field Summary
[instance]  boolean moreElements
          Do we have more elements?
Ghost Field Summary
[instance]  Class elementType
          The type of the elements we return.
[instance]  boolean returnsNull
          Do we ever return null as an element?
Method Summary
 boolean hasMoreElements()
 Object nextElement()

Model Field Detail


public boolean moreElements
Do we have more elements?

Specifications: instance
is in groups: objectState
Ghost Field Detail


public Class elementType
The type of the elements we return.

Specifications: instance nullable


public boolean returnsNull
Do we ever return null as an element?

Specifications: instance
Method Detail


public boolean hasMoreElements()
public normal_behavior
assignable objectState;
ensures \result <==> this.moreElements;


public Object nextElement()
Specifications: nullable
public normal_behavior
requires this.moreElements;
assignable objectState;
assignable moreElements;
ensures (\result == null)||\typeof(\result ) <: this.elementType;
ensures !this.returnsNull ==> (\result != null);
public exceptional_behavior
requires !this.moreElements;
assignable \nothing;
signals_only java.util.NoSuchElementException;


JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.