org.jmlspecs.jmlunit.strategies
Class NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter

java.lang.Object
  org.jmlspecs.jmlunit.strategies.NewObjectAbstractIterator
      org.jmlspecs.jmlunit.strategies.NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter

All Implemented Interfaces:

Cloneable, IndefiniteIterator

Enclosing class:

NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1

class NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter

extends NewObjectAbstractIterator

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

 

Field Summary

 

Fields inherited from class org.jmlspecs.jmlunit.strategies.NewObjectAbstractIterator

 

Constructor Summary

NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter()           Initialize the superclass.

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
Object	make(int n)           Return null for index 0, and for n > 0, return the object returned NewObjectAbstractStrategy.this.make(n-1);

 

Methods inherited from class org.jmlspecs.jmlunit.strategies.NewObjectAbstractIterator

advance, atEnd, clone, get, initialize

 

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Constructor Detail

NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter

public NewObjectAbstractExtensibleStrategyDecorator.NewObjectAbstractExtensibleStrategyDecorator$1.NewIter()

Initialize the superclass. This needs to be done so that the initialize method is called after this object is constructed, otherwise a downcall to make here gives a null pointer exception.

See Also:

NewObjectAbstractIterator.initialize()

Specifications:

assignable objectState;

make

public Object make(int n)

Return null for index 0, and for n > 0, return the object returned NewObjectAbstractStrategy.this.make(n-1);

Specifications: pure

Specifications inherited from overridden method make(int n) in class NewObjectAbstractIterator:
       pure nullable

public behavior
requires 0 <= n;
assignable \nothing;
signals_only java.util.NoSuchElementException;