java.util
Interface Enumeration

All Known Subinterfaces:

JMLEnumeration

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.

Version:

$Revision: 1.15 $

Author:

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

moreElements

public boolean moreElements

Do we have more elements?

Specifications: instance
is in groups: objectState

elementType

public Class elementType

The type of the elements we return.

Specifications: instance nullable

returnsNull

public boolean returnsNull

Do we ever return null as an element?

Specifications: instance

hasMoreElements

public boolean hasMoreElements()

Specifications:

public normal_behavior
assignable objectState;
ensures \result <==> this.moreElements;

nextElement

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);

     also

public exceptional_behavior
requires !this.moreElements;
assignable \nothing;
signals_only java.util.NoSuchElementException;