Class CloneableObjectArrayAbstractIterator

  extended byorg.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator
      extended byorg.jmlspecs.jmlunit.strategies.CloneableObjectArrayAbstractIterator
All Implemented Interfaces:
Cloneable, IndefiniteIterator
Direct Known Subclasses:
CloneableObjectAbstractStrategy.CloneableObjectAbstractStrategy$1, CloneableObjectArrayAbstractIterator_JML_TestData.IntArrayArrayIterator

public abstract class CloneableObjectArrayAbstractIterator
extends ObjectArrayAbstractIterator

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

Gary T. Leavens
See Also:

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
CloneableObjectArrayAbstractIterator(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 abstract  Object cloneElement(Object elem)
          Return a clone of the argument, which is assumed not to be null.
protected  Object duplicateIfNeeded(nullable Object elem)
          Return a clone of the argument, or null if it is null.
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 CloneableObjectArrayAbstractIterator(Object[] elems)
Initialize this iterator to iterate over a clone of the array

public normal_behavior
requires elems != null;
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 a clone of the argument, or null if it is null.

Specifications: pure nullable
Specifications inherited from overridden method duplicateIfNeeded(Object elem) in class ObjectArrayAbstractIterator:
       pure spec_public nullable
public normal_behavior
assignable \nothing;


protected abstract Object cloneElement(Object elem)
Return a clone of the argument, which is assumed not to be null.

Specifications: pure
protected normal_behavior
requires elem != null;
assignable \nothing;
ensures \result != null;
ensures (* \result is a clone of elem *);
ensures_redundantly \result != null;


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.