org.jmlspecs.jmlunit.strategies
Class IntAbstractIterator
java.lang.Object
org.jmlspecs.jmlunit.strategies.IntAbstractIterator
- All Implemented Interfaces:
- Cloneable, IndefiniteIterator, IntIterator
- Direct Known Subclasses:
- IntAbstractFilteringIteratorDecorator, IntArrayIterator, IntCompositeIterator
- public abstract class IntAbstractIterator
- extends Object
- implements IntIterator
Common code for iterators over values of type int that
implement the IntIterator interface.
- Author:
- Gary T. Leavens
Specifications inherited from class Object |
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this); |
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. |
IntAbstractIterator
public IntAbstractIterator()
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 IntIterator
- Specifications: nullable (inherited)pure
- Specifications inherited from overridden method in interface IntIterator:
pure nullable- also
-
public normal_behavior
requires !this.atEnd();
ensures \result instanceof java.lang.Integer;
- 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:
IntIterator
- Return a copy of this iterator in the same state as this object.
- Specified by:
clone
in interface IntIterator
- 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 IntIterator:
pure- also
-
public normal_behavior
assignable \nothing;
ensures \fresh(\result )&&\result instanceof org.jmlspecs.jmlunit.strategies.IntIterator;
ensures \result != this;
ensures_redundantly \result != null;
ensures ((org.jmlspecs.jmlunit.strategies.IntIterator)\result ).atEnd() == this.atEnd();
ensures !this.atEnd() ==> new java.lang.Integer(((org.jmlspecs.jmlunit.strategies.IntIterator)\result ).getInt()).equals(new java.lang.Integer(this.getInt()));
- 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 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.