org.jmlspecs.models
Class JMLValueToValueMap_JML_TestData

java.lang.Object
  junit.framework.Assert
      junit.framework.TestCase
          org.jmlspecs.models.JMLValueToValueMap_JML_TestData

All Implemented Interfaces:

junit.framework.Test

public abstract class JMLValueToValueMap_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  StrategyType	vjava_lang_ObjectStrategy           The strategy for generating test data of type java.lang.Object.
private  StrategyType	vorg_jmlspecs_models_JMLObjectToValueMapStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLObjectToValueMap.
private  StrategyType	vorg_jmlspecs_models_JMLObjectToValueRelationStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLObjectToValueRelation.
private  StrategyType	vorg_jmlspecs_models_JMLValueSetStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLValueSet.
private  StrategyType	vorg_jmlspecs_models_JMLValueToValueMapStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLValueToValueMap.
private  StrategyType	vorg_jmlspecs_models_JMLValueToValueRelationStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLValueToValueRelation.
private  StrategyType	vorg_jmlspecs_models_JMLValueValuePairStrategy           The strategy for generating test data of type org.jmlspecs.models.JMLValueValuePair.

 

Fields inherited from class junit.framework.TestCase

 

Constructor Summary

JMLValueToValueMap_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_JMLObjectToValueMapIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToValueMap for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLObjectToValueRelationIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToValueRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLTypeIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLType for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLValueSetIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueSet for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLValueToValueMapIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToValueMap for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLValueToValueRelationIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToValueRelation for testing the method named by the String methodName in a loop that encloses loopsThisSurrounds many other loops.
protected  IndefiniteIterator	vorg_jmlspecs_models_JMLValueValuePairIter(String methodName, int loopsThisSurrounds)           Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueValuePair 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

vorg_jmlspecs_models_JMLObjectToValueMapStrategy

private StrategyType vorg_jmlspecs_models_JMLObjectToValueMapStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLObjectToValueMap.

vorg_jmlspecs_models_JMLValueSetStrategy

private StrategyType vorg_jmlspecs_models_JMLValueSetStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLValueSet.

vorg_jmlspecs_models_JMLValueToValueMapStrategy

private StrategyType vorg_jmlspecs_models_JMLValueToValueMapStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLValueToValueMap.

vorg_jmlspecs_models_JMLValueValuePairStrategy

private StrategyType vorg_jmlspecs_models_JMLValueValuePairStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLValueValuePair.

vorg_jmlspecs_models_JMLValueToValueRelationStrategy

private StrategyType vorg_jmlspecs_models_JMLValueToValueRelationStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLValueToValueRelation.

vorg_jmlspecs_models_JMLObjectToValueRelationStrategy

private StrategyType vorg_jmlspecs_models_JMLObjectToValueRelationStrategy

The strategy for generating test data of type org.jmlspecs.models.JMLObjectToValueRelation.

vjava_lang_ObjectStrategy

private StrategyType vjava_lang_ObjectStrategy

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

JMLValueToValueMap_JML_TestData

public JMLValueToValueMap_JML_TestData(String name)

Initialize this class.

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_JMLObjectToValueMapIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLObjectToValueMapIter(String methodName,
                                                                          int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToValueMap 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_JMLValueSetIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLValueSetIter(String methodName,
                                                                  int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueSet 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_JMLValueToValueMapIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueMapIter(String methodName,
                                                                         int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToValueMap 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_JMLTypeIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLTypeIter(String methodName,
                                                              int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLType 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_JMLValueValuePairIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePairIter(String methodName,
                                                                        int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueValuePair 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_JMLValueToValueRelationIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueRelationIter(String methodName,
                                                                              int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLValueToValueRelation 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_JMLObjectToValueRelationIter

protected IndefiniteIterator vorg_jmlspecs_models_JMLObjectToValueRelationIter(String methodName,
                                                                               int loopsThisSurrounds)

Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.models.JMLObjectToValueRelation 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 );