|
JML | ||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object junit.framework.Assert junit.framework.TestCase org.jmlspecs.samples.list.list1.E_SLList_JML_TestData
Supply test data for the JML and JUnit based testing of E_SLList.
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_samples_list_list1_E_SLListStrategy
The strategy for generating test data of type org.jmlspecs.samples.list.list1.E_SLList. |
Fields inherited from class junit.framework.TestCase |
|
Constructor Summary | |
E_SLList_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_samples_list_list1_E_SLListIter(String methodName,
int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.samples.list.list1.E_SLList 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 |
private StrategyType vorg_jmlspecs_samples_list_list1_E_SLListStrategy
private StrategyType vjava_lang_ObjectStrategy
Constructor Detail |
public E_SLList_JML_TestData(String name)
Method Detail |
public junit.framework.TestSuite overallTestSuite()
TestSuite
public junit.framework.TestSuite emptyTestSuiteFor(String methodName)
methodName
- The method the tests in this suite are for.TestSuite
,
LimitedTestSuite
protected IndefiniteIterator vorg_jmlspecs_samples_list_list1_E_SLListIter(String methodName, int loopsThisSurrounds)
methodName
- name of the method for which this
test data will be used.loopsThisSurrounds
- number of loops that the test
contains inside this one.protected IndefiniteIterator vjava_lang_ObjectIter(String methodName, int loopsThisSurrounds)
methodName
- name of the method for which this
test data will be used.loopsThisSurrounds
- number of loops that the test
contains inside this one.
|
JML | ||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |