JML

org.jmlspecs.jmlunit.strategies
Class FloatAbstractIterator

java.lang.Object
  extended byorg.jmlspecs.jmlunit.strategies.FloatAbstractIterator
All Implemented Interfaces:
Cloneable, FloatIterator, IndefiniteIterator
Direct Known Subclasses:
FloatAbstractFilteringIteratorDecorator, FloatArrayIterator, FloatCompositeIterator

public abstract class FloatAbstractIterator
extends Object
implements FloatIterator

Common code for iterators over values of type float that implement the FloatIterator interface.

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
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Constructor Summary
FloatAbstractIterator()
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 Object clone()
          Return a copy of this iterator in the same state as this object.
 Object get()
          Return the current element in this iteration.
 
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 
Methods inherited from interface org.jmlspecs.jmlunit.strategies.FloatIterator
getFloat
 
Methods inherited from interface org.jmlspecs.jmlunit.strategies.IndefiniteIterator
advance, atEnd
 

Constructor Detail

FloatAbstractIterator

public FloatAbstractIterator()
Method Detail

get

public Object get()
Description copied from interface: IndefiniteIterator
Return the current element in this iteration. This method may be called multiple times, and does not advance the state of the iterator when it is called. The idea is to permit several similar copies to be returned (e.g., clones) each time it is called.

Specified by:
get in interface FloatIterator
Specifications: nullable (inherited)pure
Specifications inherited from overridden method in interface FloatIterator:
       pure nullable
     also
public normal_behavior
requires !this.atEnd();
ensures \result instanceof java.lang.Float;
Specifications inherited from overridden method in interface IndefiniteIterator:
       pure nullable
public behavior
assignable \nothing;
ensures_redundantly this.atEnd() == \old(this.atEnd());
signals (java.lang.Exception e) e instanceof java.util.NoSuchElementException&&this.atEnd();

clone

public Object clone()
Description copied from interface: FloatIterator
Return a copy of this iterator in the same state as this object.

Specified by:
clone in interface FloatIterator
Overrides:
clone in class Object
Specifications: pure
Specifications inherited from overridden method in class Object:
       non_null
protected normal_behavior
requires this instanceof java.lang.Cloneable;
assignable \nothing;
ensures \result != null;
ensures \typeof(\result ) == \typeof(this);
ensures (* \result is a clone of this *);
     also
protected normal_behavior
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
requires this.getClass().isArray();
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures java.lang.reflect.Array.getLength(\result ) == java.lang.reflect.Array.getLength(this);
ensures ( \forall int i; 0 <= i&&i < java.lang.reflect.Array.getLength(this); ( \exists java.lang.Object result_i; result_i == java.lang.reflect.Array.get(\result ,i); (result_i == null&&java.lang.reflect.Array.get(this,i) == null)||(result_i != null&&result_i.equals(java.lang.reflect.Array.get(this,i)))));
     also
protected exceptional_behavior
requires !(this instanceof java.lang.Cloneable);
assignable \nothing;
signals_only java.lang.CloneNotSupportedException;
     also
protected normal_behavior
requires \elemtype(\typeof(this)) <: \type(java.lang.Object);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((java.lang.Object[])\result ).length == ((java.lang.Object[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((java.lang.Object[])this).length; ((java.lang.Object[])\result )[i] == ((java.lang.Object[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(int);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((int[])\result ).length == ((int[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((int[])this).length; ((int[])\result )[i] == ((int[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(byte);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((byte[])\result ).length == ((byte[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((byte[])this).length; ((byte[])\result )[i] == ((byte[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(char);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((char[])\result ).length == ((char[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((char[])this).length; ((char[])\result )[i] == ((char[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(long);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((long[])\result ).length == ((long[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((long[])this).length; ((long[])\result )[i] == ((long[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(short);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((short[])\result ).length == ((short[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((short[])this).length; ((short[])\result )[i] == ((short[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(boolean);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((boolean[])\result ).length == ((boolean[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((boolean[])this).length; ((boolean[])\result )[i] == ((boolean[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(float);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((float[])\result ).length == ((float[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((float[])this).length; (java.lang.Float.isNaN(((float[])\result )[i])&&java.lang.Float.isNaN(((float[])this)[i]))||((float[])\result )[i] == ((float[])this)[i]);
     also
protected normal_behavior
requires \elemtype(\typeof(this)) == \type(double);
assignable \nothing;
ensures \elemtype(\typeof(\result )) == \elemtype(\typeof(this));
ensures ((double[])\result ).length == ((double[])this).length;
ensures ( \forall int i; 0 <= i&&i < ((double[])this).length; (java.lang.Double.isNaN(((double[])\result )[i])&&java.lang.Double.isNaN(((double[])this)[i]))||((double[])\result )[i] == ((double[])this)[i]);
Specifications inherited from overridden method in interface FloatIterator:
       pure
     also
public normal_behavior
assignable \nothing;
ensures \fresh(\result )&&\result instanceof org.jmlspecs.jmlunit.strategies.FloatIterator;
ensures \result != this;
ensures_redundantly \result != null;
ensures ((org.jmlspecs.jmlunit.strategies.FloatIterator)\result ).atEnd() == this.atEnd();
ensures !this.atEnd() ==> new java.lang.Float(((org.jmlspecs.jmlunit.strategies.FloatIterator)\result ).getFloat()).equals(new java.lang.Float(this.getFloat()));
Specifications inherited from overridden method in interface IndefiniteIterator:
       pure
     also
public normal_behavior
assignable \nothing;
ensures \fresh(\result )&&\result instanceof org.jmlspecs.jmlunit.strategies.IndefiniteIterator;
ensures \result != this;
ensures_redundantly \result != null;
ensures ((org.jmlspecs.jmlunit.strategies.IndefiniteIterator)\result ).atEnd() == this.atEnd();

JML

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.