org.jmlspecs.jmlunit.strategies
Class ImmutableObjectArrayIterator

java.lang.Object
  org.jmlspecs.jmlunit.strategies.ObjectArrayAbstractIterator
      org.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.

Author:

Gary T. Leavens

Class Specifications

Specifications inherited from class ObjectArrayAbstractIterator

public invariant 0 <= this.next&&this.next <= 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

hashValue

 

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

ImmutableObjectArrayIterator

public ImmutableObjectArrayIterator(Object[] elems)

Initialize this iterator to iterate over a clone of the array

Specifications:

public normal_behavior
assignable this.elems, next;
ensures this.next == 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;

duplicateIfNeeded

protected Object duplicateIfNeeded(nullable Object elem)

Return the argument (which is presumed to be immutable, and therefore not cloned).

Specifications: pure nullable

     also

protected normal_behavior
assignable \nothing;
ensures \result == this.elems[this.next];

Specifications inherited from overridden method duplicateIfNeeded(Object elem) in class ObjectArrayAbstractIterator:
       pure spec_public nullable

public normal_behavior
assignable \nothing;