JML

org.jmlspecs.models
Class JMLObjectToObjectRelation_JML_TestData

java.lang.Object
  extended byjunit.framework.Assert
      extended byjunit.framework.TestCase
          extended byorg.jmlspecs.models.JMLObjectToObjectRelation_JML_TestData
All Implemented Interfaces:
junit.framework.Test

public abstract class JMLObjectToObjectRelation_JML_TestData
extends junit.framework.TestCase

Supply test data for the JML and JUnit based testing of Person.

Test data is supplied by overriding methods in this class. See the JML documentation and the comments below about how to do this.

This class is also the place to override the setUp() and tearDown() methods if your testing needs some actions to be taken before and after each test is executed.

This class is never rewritten by jmlunit.


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
private  Integer i0
           
private  Integer i1
           
private  Integer i2
           
private  Integer i3
           
private  Integer i4
           
private  JMLObjectToObjectRelation intsToArrays
           
private  JMLObjectToObjectRelation lessThan2
           
private  JMLObjectToObjectRelation lessThan3
           
private  JMLObjectToObjectRelation lessThan4
           
private  StrategyType vjava_lang_ObjectStrategy
          The strategy for generating test data of type java.lang.Object.
private  StrategyType vorg_jmlspecs_models_JMLObjectObjectPairStrategy
          The strategy for generating test data of type org.jmlspecs.models.JMLObjectObjectPair.
private  StrategyType vorg_jmlspecs_models_JMLObjectSetStrategy
          The strategy for generating test data of type org.jmlspecs.models.JMLObjectSet.
private  StrategyType vorg_jmlspecs_models_JMLObjectToObjectRelationStrategy
          The strategy for generating test data of type org.jmlspecs.models.JMLObjectToObjectRelation.
private  StrategyType vorg_jmlspecs_models_JMLValueToObjectRelationStrategy
          The strategy for generating test data of type org.jmlspecs.models.JMLValueToObjectRelation.
 
Fields inherited from class junit.framework.TestCase
 
Constructor Summary
JMLObjectToObjectRelation_JML_TestData(String name)
          Initialize this class.
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 junit.framework.TestSuite emptyTestSuiteFor(String methodName)
          Return an empty test suite for accumulating tests for the named method.
 junit.framework.TestSuite overallTestSuite()
          Return the overall test suite for accumulating tests; the result will hold every test that will be run.
protected  IndefiniteIterator vjava_lang_ObjectIter(String methodName, int loopsThisSurrounds)
          Return a new, freshly allocated indefinite iterator that produces test data of type java.lang.Object for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPairIter(String methodName, int loopsThisSurrounds)
          Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectObjectPair for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator vorg_jmlspecs_models_JMLObjectSetIter(String methodName, int loopsThisSurrounds)
          Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectSet for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelationIter(String methodName, int loopsThisSurrounds)
          Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToObjectRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator vorg_jmlspecs_models_JMLValueToObjectRelationIter(String methodName, int loopsThisSurrounds)
          Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToObjectRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
 
Methods inherited from class junit.framework.TestCase
countTestCases, createResult, getName, run, run, runBare, runTest, setName, setUp, tearDown, toString
 
Methods inherited from class junit.framework.Assert
assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertEquals, assertFalse, assertFalse, assertNotNull, assertNotNull, assertNotSame, assertNotSame, assertNull, assertNull, assertSame, assertSame, assertTrue, assertTrue, fail, fail
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

i4

private final Integer i4

i3

private final Integer i3

i2

private final Integer i2

i1

private final Integer i1

i0

private final Integer i0

intsToArrays

private final JMLObjectToObjectRelation intsToArrays

lessThan4

private final JMLObjectToObjectRelation lessThan4

lessThan3

private final JMLObjectToObjectRelation lessThan3

lessThan2

private final JMLObjectToObjectRelation lessThan2

vorg_jmlspecs_models_JMLValueToObjectRelationStrategy

private StrategyType vorg_jmlspecs_models_JMLValueToObjectRelationStrategy
The strategy for generating test data of type org.jmlspecs.models.JMLValueToObjectRelation.


vorg_jmlspecs_models_JMLObjectObjectPairStrategy

private StrategyType vorg_jmlspecs_models_JMLObjectObjectPairStrategy
The strategy for generating test data of type org.jmlspecs.models.JMLObjectObjectPair.


vorg_jmlspecs_models_JMLObjectSetStrategy

private StrategyType vorg_jmlspecs_models_JMLObjectSetStrategy
The strategy for generating test data of type org.jmlspecs.models.JMLObjectSet.


vorg_jmlspecs_models_JMLObjectToObjectRelationStrategy

private StrategyType vorg_jmlspecs_models_JMLObjectToObjectRelationStrategy
The strategy for generating test data of type org.jmlspecs.models.JMLObjectToObjectRelation.


vjava_lang_ObjectStrategy

private StrategyType vjava_lang_ObjectStrategy
The strategy for generating test data of type java.lang.Object.

Constructor Detail

JMLObjectToObjectRelation_JML_TestData

public JMLObjectToObjectRelation_JML_TestData(String name)
Initialize this class.

Method Detail

overallTestSuite

public junit.framework.TestSuite overallTestSuite()
Return the overall test suite for accumulating tests; the result will hold every test that will be run. This factory method can be altered to provide filtering of test suites, as they are added to this overall test suite, based on various criteria. The test driver will first call the method addTestSuite to add a test suite formed from custom programmed test methods (named testX for some X), which you can add to this class; this initial test suite will also include a method to check that the code being tested was compiled with jmlc. After that, for each method to be tested, a test suite containing tests for that method will be added to this overall test suite, using the addTest method. Test suites added for a method will have some subtype of TestSuite and that method's name as their name. So, if you want to control the overall suite of tests for testing some method, e.g., to limit the number of tests for each method, return a special-purpose subclass of junit.framework.TestSuite in which you override the addTest method.

See Also:
TestSuite
Specifications:
assignable objectState;
ensures \result != null;

emptyTestSuiteFor

public junit.framework.TestSuite emptyTestSuiteFor(String methodName)
Return an empty test suite for accumulating tests for the named method. This factory method can be altered to provide filtering or limiting of the tests for the named method, as they are added to the test suite for this method. The driver will add individual tests using the addTest method. So, if you want to filter individual tests, return a subclass of TestSuite in which you override the addTest method.

Parameters:
methodName - The method the tests in this suite are for.
See Also:
TestSuite, LimitedTestSuite
Specifications:
assignable objectState;
ensures \result != null;

vorg_jmlspecs_models_JMLValueToObjectRelationIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLValueToObjectRelationIter(String methodName,
                                                                               int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToObjectRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.

Parameters:
methodName - name of the method for which this test data will be used.
loopsThisSurrounds - number of loops that the test contains inside this one.
Specifications:
requires methodName != null&&loopsThisSurrounds >= 0;
ensures \fresh(\result );

vorg_jmlspecs_models_JMLObjectObjectPairIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPairIter(String methodName,
                                                                          int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectObjectPair for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.

Parameters:
methodName - name of the method for which this test data will be used.
loopsThisSurrounds - number of loops that the test contains inside this one.
Specifications:
requires methodName != null&&loopsThisSurrounds >= 0;
ensures \fresh(\result );

vorg_jmlspecs_models_JMLObjectSetIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLObjectSetIter(String methodName,
                                                                   int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectSet for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.

Parameters:
methodName - name of the method for which this test data will be used.
loopsThisSurrounds - number of loops that the test contains inside this one.
Specifications:
requires methodName != null&&loopsThisSurrounds >= 0;
ensures \fresh(\result );

vorg_jmlspecs_models_JMLObjectToObjectRelationIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelationIter(String methodName,
                                                                                int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToObjectRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.

Parameters:
methodName - name of the method for which this test data will be used.
loopsThisSurrounds - number of loops that the test contains inside this one.
Specifications:
requires methodName != null&&loopsThisSurrounds >= 0;
ensures \fresh(\result );

vjava_lang_ObjectIter

protected IndefiniteIterator vjava_lang_ObjectIter(String methodName,
                                                   int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type java.lang.Object for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.

Parameters:
methodName - name of the method for which this test data will be used.
loopsThisSurrounds - number of loops that the test contains inside this one.
Specifications:
requires methodName != null&&loopsThisSurrounds >= 0;
ensures \fresh(\result );

JML

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.