|
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.list2.E_OneWayList_JML_TestData
Supply test data for the JML and JUnit based testing of E_OneWayList.
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 | |
(package private) String |
first
|
(package private) String |
fourth
|
(package private) String |
second
|
(package private) String |
third
|
private StrategyType |
vjava_lang_ObjectStrategy
The strategy for generating test data of type java.lang.Object. |
private StrategyType |
vorg_jmlspecs_samples_list_list2_E_OneWayListStrategy
The strategy for generating test data of type org.jmlspecs.samples.list.list2.E_OneWayList. |
Fields inherited from class junit.framework.TestCase |
|
Constructor Summary | |
E_OneWayList_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_list2_E_OneWayListIter(String methodName,
int loopsThisSurrounds)
Return a new, freshly allocated indefinite iterator that produces test data of type org.jmlspecs.samples.list.list2.E_OneWayList 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 |
String first
String second
String third
String fourth
private StrategyType vjava_lang_ObjectStrategy
private StrategyType vorg_jmlspecs_samples_list_list2_E_OneWayListStrategy
Constructor Detail |
public E_OneWayList_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 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.protected IndefiniteIterator vorg_jmlspecs_samples_list_list2_E_OneWayListIter(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 |