Class JMLCollectionUnextensibleStrategy

  extended byorg.jmlspecs.jmlunit.strategies.CachedObjectAbstractStrategy
      extended byorg.jmlspecs.jmlunit.strategies.ImmutableObjectAbstractStrategy
          extended byorg.jmlspecs.jmlunit.strategies.JMLCollectionUnextensibleStrategy
All Implemented Interfaces:

class JMLCollectionUnextensibleStrategy
extends ImmutableObjectAbstractStrategy

A strategy for providing test data of type JMLCollection. This subclasses ImmutableObjectAbstractStrategy because the test data provided are all immutable.

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.CachedObjectAbstractStrategy
Constructor Summary
(package private) JMLCollectionUnextensibleStrategy()
Model Method Summary
Model methods inherited from class java.lang.Object
Method Summary
protected  Object[] addData()
          Test data of type JMLCollection.
Methods inherited from class org.jmlspecs.jmlunit.strategies.ImmutableObjectAbstractStrategy
Methods inherited from class org.jmlspecs.jmlunit.strategies.CachedObjectAbstractStrategy
defaultData, getData, iterator
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail


Method Detail


protected Object[] addData()
Test data of type JMLCollection. These should all be immutable, or the superclass of this class should be changed.

addData in class CachedObjectAbstractStrategy
Specifications inherited from overridden method in class CachedObjectAbstractStrategy:
protected normal_behavior
assignable objectState;
ensures \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.