Class ImmutableObjectArrayIterator

  extended byorg.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator
      extended byorg.jmlspecs.jmlunit.strategies.ImmutableObjectArrayIterator
All Implemented Interfaces:
Cloneable, IndefiniteIterator

public class ImmutableObjectArrayIterator
extends ObjectArrayAbstractIterator

An iterator that provides test data by returning the current object from an array of immutable objects passed to its constructor.

This can only handle iterations up to Integer.MAX_VALUE elements.

Gary T. Leavens

Class Specifications

Specifications inherited from class ObjectArrayAbstractIterator
public invariant 0 <= <= this.elems.length;

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
Field Summary
Fields inherited from class org.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator
elems, next
Constructor Summary
ImmutableObjectArrayIterator(Object[] elems)
          Initialize this iterator to iterate over a clone of the array
Model Method Summary
Model methods inherited from class java.lang.Object
Method Summary
protected  Object duplicateIfNeeded(nullable Object elem)
          Return the argument (which is presumed to be immutable, and therefore not cloned).
Methods inherited from class org.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator
advance, atEnd, clone, elementsString, get, toString
Methods inherited from class java.lang.Object
equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail


public ImmutableObjectArrayIterator(Object[] elems)
Initialize this iterator to iterate over a clone of the array

public normal_behavior
assignable this.elems, next;
ensures == 0;
ensures (* this.elems is a clone of elems *);
ensures \fresh(this.elems);
ensures_redundantly this.elems != null&&this.elems != elems;
ensures this.elems.length == elems.length;
Method Detail


protected Object duplicateIfNeeded(nullable Object elem)
Return the argument (which is presumed to be immutable, and therefore not cloned).

Specifications: pure nullable
protected normal_behavior
assignable \nothing;
ensures \result == this.elems[];
Specifications inherited from overridden method duplicateIfNeeded(Object elem) in class ObjectArrayAbstractIterator:
       pure spec_public nullable
public normal_behavior
assignable \nothing;


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.