How to use tests method of junit.framework.TestSuite class

Best junit code snippet using junit.framework.TestSuite.tests

Source:JMLValueSet_JML_Test.java Github

copy

Full Screen

...16 /** Initialize this class. */17 public JMLValueSet_JML_Test(java.lang.String name) {18 super(name);19 }20 /** Run the tests. */21 public static void main(java.lang.String[] args) {22 org.jmlspecs.jmlunit.JMLTestRunner.run(suite());23 // You can also use a JUnit test runner such as:24 // junit.textui.TestRunner.run(suite());25 }26 /** Test to see if the code for class JMLValueSet27 * has been compiled with runtime assertion checking (i.e., by jmlc).28 * Code that is not compiled with jmlc would not make an effective test,29 * since no assertion checking would be done. */30 public void test$IsRACCompiled() {31 junit.framework.Assert.assertTrue("code for class JMLValueSet"32 + " was not compiled with jmlc"33 + " so no assertions will be checked!",34 org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLValueSet.class)35 );36 }37 /** Return the test suite for this test class. This will have38 * added to it at least test$IsRACCompiled(), and any test methods39 * written explicitly by the user in the superclass. It will also40 * have added test suites for each testing each method and41 * constructor.42 */43 //@ ensures \result != null;44 public static junit.framework.Test suite() {45 JMLValueSet_JML_Test testobj46 = new JMLValueSet_JML_Test("JMLValueSet_JML_Test");47 junit.framework.TestSuite testsuite = testobj.overallTestSuite();48 // Add instances of Test found by the reflection mechanism.49 testsuite.addTestSuite(JMLValueSet_JML_Test.class);50 testobj.addTestSuiteForEachMethod(testsuite);51 return testsuite;52 }53 /** A JUnit test object that can run a single test method. This54 * is defined as a nested class solely for convenience; it can't55 * be defined once and for all because it must subclass its56 * enclosing class.57 */58 protected static abstract class OneTest extends JMLValueSet_JML_Test {59 /** Initialize this test object. */60 public OneTest(String name) {61 super(name);62 }63 /** The result object that holds information about testing. */64 protected junit.framework.TestResult result;65 //@ also66 //@ requires result != null;67 public void run(junit.framework.TestResult result) {68 this.result = result;69 super.run(result);70 }71 /* Run a single test and decide whether the test was72 * successful, meaningless, or a failure. This is the73 * Template Method pattern abstraction of the inner loop in a74 * JML/JUnit test. */75 public void runTest() throws java.lang.Throwable {76 try {77 // The call being tested!78 doCall();79 }80 catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) {81 // meaningless test input82 addMeaningless();83 } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) {84 // test failure85 int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel();86 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel87 (org.jmlspecs.jmlrac.runtime.JMLOption.NONE);88 try {89 java.lang.String failmsg = this.failMessage(e);90 junit.framework.AssertionFailedError err91 = new junit.framework.AssertionFailedError(failmsg);92 err.setStackTrace(new java.lang.StackTraceElement[]{});93 err.initCause(e);94 result.addFailure(this, err);95 } finally {96 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l);97 }98 } catch (java.lang.Throwable e) {99 // test success100 }101 }102 /** Call the method to be tested with the appropriate arguments. */103 protected abstract void doCall() throws java.lang.Throwable;104 /** Format the error message for a test failure, based on the105 * method's arguments. */106 protected abstract java.lang.String failMessage107 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e);108 /** Inform listeners that a meaningless test was run. */109 private void addMeaningless() {110 if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) {111 ((org.jmlspecs.jmlunit.JMLTestResult)result)112 .addMeaningless(this);113 }114 }115 }116 /** Create the tests that are to be run for testing the class117 * JMLValueSet. The framework will then run them.118 * @param overallTestSuite$ The suite accumulating all of the tests119 * for this driver class.120 */121 //@ requires overallTestSuite$ != null;122 public void addTestSuiteForEachMethod123 (junit.framework.TestSuite overallTestSuite$)124 {125 try {126 this.addTestSuiteFor$TestJMLValueSet(overallTestSuite$);127 } catch (java.lang.Throwable ex) {128 overallTestSuite$.addTest129 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));130 }131 try {132 this.addTestSuiteFor$TestJMLValueSet$1(overallTestSuite$);133 } catch (java.lang.Throwable ex) {134 overallTestSuite$.addTest135 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));136 }137 try {138 this.addTestSuiteFor$TestSingleton(overallTestSuite$);139 } catch (java.lang.Throwable ex) {140 overallTestSuite$.addTest141 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));142 }143 try {144 this.addTestSuiteFor$TestConvertFrom(overallTestSuite$);145 } catch (java.lang.Throwable ex) {146 overallTestSuite$.addTest147 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));148 }149 try {150 this.addTestSuiteFor$TestConvertFrom$1(overallTestSuite$);151 } catch (java.lang.Throwable ex) {152 overallTestSuite$.addTest153 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));154 }155 try {156 this.addTestSuiteFor$TestConvertFrom$2(overallTestSuite$);157 } catch (java.lang.Throwable ex) {158 overallTestSuite$.addTest159 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));160 }161 try {162 this.addTestSuiteFor$TestHas(overallTestSuite$);163 } catch (java.lang.Throwable ex) {164 overallTestSuite$.addTest165 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));166 }167 try {168 this.addTestSuiteFor$TestContainsAll(overallTestSuite$);169 } catch (java.lang.Throwable ex) {170 overallTestSuite$.addTest171 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));172 }173 try {174 this.addTestSuiteFor$TestEquals(overallTestSuite$);175 } catch (java.lang.Throwable ex) {176 overallTestSuite$.addTest177 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));178 }179 try {180 this.addTestSuiteFor$TestHashCode(overallTestSuite$);181 } catch (java.lang.Throwable ex) {182 overallTestSuite$.addTest183 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));184 }185 try {186 this.addTestSuiteFor$TestIsEmpty(overallTestSuite$);187 } catch (java.lang.Throwable ex) {188 overallTestSuite$.addTest189 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));190 }191 try {192 this.addTestSuiteFor$TestInt_size(overallTestSuite$);193 } catch (java.lang.Throwable ex) {194 overallTestSuite$.addTest195 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));196 }197 try {198 this.addTestSuiteFor$TestIsSubset(overallTestSuite$);199 } catch (java.lang.Throwable ex) {200 overallTestSuite$.addTest201 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));202 }203 try {204 this.addTestSuiteFor$TestIsProperSubset(overallTestSuite$);205 } catch (java.lang.Throwable ex) {206 overallTestSuite$.addTest207 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));208 }209 try {210 this.addTestSuiteFor$TestIsSuperset(overallTestSuite$);211 } catch (java.lang.Throwable ex) {212 overallTestSuite$.addTest213 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));214 }215 try {216 this.addTestSuiteFor$TestIsProperSuperset(overallTestSuite$);217 } catch (java.lang.Throwable ex) {218 overallTestSuite$.addTest219 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));220 }221 try {222 this.addTestSuiteFor$TestChoose(overallTestSuite$);223 } catch (java.lang.Throwable ex) {224 overallTestSuite$.addTest225 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));226 }227 try {228 this.addTestSuiteFor$TestClone(overallTestSuite$);229 } catch (java.lang.Throwable ex) {230 overallTestSuite$.addTest231 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));232 }233 try {234 this.addTestSuiteFor$TestInsert(overallTestSuite$);235 } catch (java.lang.Throwable ex) {236 overallTestSuite$.addTest237 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));238 }239 try {240 this.addTestSuiteFor$TestRemove(overallTestSuite$);241 } catch (java.lang.Throwable ex) {242 overallTestSuite$.addTest243 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));244 }245 try {246 this.addTestSuiteFor$TestIntersection(overallTestSuite$);247 } catch (java.lang.Throwable ex) {248 overallTestSuite$.addTest249 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));250 }251 try {252 this.addTestSuiteFor$TestUnion(overallTestSuite$);253 } catch (java.lang.Throwable ex) {254 overallTestSuite$.addTest255 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));256 }257 try {258 this.addTestSuiteFor$TestDifference(overallTestSuite$);259 } catch (java.lang.Throwable ex) {260 overallTestSuite$.addTest261 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));262 }263 try {264 this.addTestSuiteFor$TestPowerSet(overallTestSuite$);265 } catch (java.lang.Throwable ex) {266 overallTestSuite$.addTest267 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));268 }269 try {270 this.addTestSuiteFor$TestToBag(overallTestSuite$);271 } catch (java.lang.Throwable ex) {272 overallTestSuite$.addTest273 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));274 }275 try {276 this.addTestSuiteFor$TestToSequence(overallTestSuite$);277 } catch (java.lang.Throwable ex) {278 overallTestSuite$.addTest279 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));280 }281 try {282 this.addTestSuiteFor$TestToArray(overallTestSuite$);283 } catch (java.lang.Throwable ex) {284 overallTestSuite$.addTest285 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));286 }287 try {288 this.addTestSuiteFor$TestElements(overallTestSuite$);289 } catch (java.lang.Throwable ex) {290 overallTestSuite$.addTest291 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));292 }293 try {294 this.addTestSuiteFor$TestIterator(overallTestSuite$);295 } catch (java.lang.Throwable ex) {296 overallTestSuite$.addTest297 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));298 }299 try {300 this.addTestSuiteFor$TestToString(overallTestSuite$);301 } catch (java.lang.Throwable ex) {302 overallTestSuite$.addTest303 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));304 }305 try {306 this.addTestSuiteFor$TestHas$1(overallTestSuite$);307 } catch (java.lang.Throwable ex) {308 overallTestSuite$.addTest309 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));310 }311 }312 /** Add tests for the JMLValueSet contructor313 * to the overall test suite. */314 private void addTestSuiteFor$TestJMLValueSet315 (junit.framework.TestSuite overallTestSuite$)316 {317 junit.framework.TestSuite methodTests$318 = this.emptyTestSuiteFor("JMLValueSet");319 try {320 methodTests$.addTest321 (new TestJMLValueSet());322 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {323 // methodTests$ doesn't want more tests324 }325 overallTestSuite$.addTest(methodTests$);326 }327 /** Test for the JMLValueSet contructor. */328 protected static class TestJMLValueSet extends OneTest {329 /** Initialize this instance. */330 public TestJMLValueSet() {331 super("JMLValueSet");332 }333 protected void doCall() throws java.lang.Throwable {334 new JMLValueSet();335 }336 protected java.lang.String failMessage337 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)338 {339 java.lang.String msg = "\n\tContructor 'JMLValueSet'";340 return msg;341 }342 }343 /** Add tests for the JMLValueSet contructor344 * to the overall test suite. */345 private void addTestSuiteFor$TestJMLValueSet$1346 (junit.framework.TestSuite overallTestSuite$)347 {348 junit.framework.TestSuite methodTests$349 = this.emptyTestSuiteFor("JMLValueSet");350 try {351 org.jmlspecs.jmlunit.strategies.IndefiniteIterator352 vorg_jmlspecs_models_JMLType$1$iter353 = this.vorg_jmlspecs_models_JMLTypeIter("JMLValueSet", 0);354 this.check_has_data355 (vorg_jmlspecs_models_JMLType$1$iter,356 "this.vorg_jmlspecs_models_JMLTypeIter(\"JMLValueSet\", 0)");357 while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) {358 final org.jmlspecs.models.JMLType e359 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get();360 methodTests$.addTest361 (new TestJMLValueSet$1(e));362 vorg_jmlspecs_models_JMLType$1$iter.advance();363 }364 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {365 // methodTests$ doesn't want more tests366 }367 overallTestSuite$.addTest(methodTests$);368 }369 /** Test for the JMLValueSet contructor. */370 protected static class TestJMLValueSet$1 extends OneTest {371 /** Argument e */372 private org.jmlspecs.models.JMLType e;373 /** Initialize this instance. */374 public TestJMLValueSet$1(org.jmlspecs.models.JMLType e) {375 super("JMLValueSet"+ ":" + (e==null? "null" :"{org.jmlspecs.models.JMLType}"));376 this.e = e;377 }378 protected void doCall() throws java.lang.Throwable {379 new JMLValueSet(e);380 }381 protected java.lang.String failMessage382 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)383 {384 java.lang.String msg = "\n\tContructor 'JMLValueSet' applied to";385 msg += "\n\tArgument e: " + this.e;386 return msg;387 }388 }389 /** Add tests for the singleton method390 * to the overall test suite. */391 private void addTestSuiteFor$TestSingleton392 (junit.framework.TestSuite overallTestSuite$)393 {394 junit.framework.TestSuite methodTests$395 = this.emptyTestSuiteFor("singleton");396 try {397 org.jmlspecs.jmlunit.strategies.IndefiniteIterator398 vorg_jmlspecs_models_JMLType$1$iter399 = this.vorg_jmlspecs_models_JMLTypeIter("singleton", 0);400 this.check_has_data401 (vorg_jmlspecs_models_JMLType$1$iter,402 "this.vorg_jmlspecs_models_JMLTypeIter(\"singleton\", 0)");403 while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) {404 final org.jmlspecs.models.JMLType e405 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get();406 methodTests$.addTest407 (new TestSingleton(e));408 vorg_jmlspecs_models_JMLType$1$iter.advance();409 }410 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {411 // methodTests$ doesn't want more tests412 }413 overallTestSuite$.addTest(methodTests$);414 }415 /** Test for the singleton method. */416 protected static class TestSingleton extends OneTest {417 /** Argument e */418 private org.jmlspecs.models.JMLType e;419 /** Initialize this instance. */420 public TestSingleton(org.jmlspecs.models.JMLType e) {421 super("singleton"+ ":" + (e==null? "null" :"{org.jmlspecs.models.JMLType}"));422 this.e = e;423 }424 protected void doCall() throws java.lang.Throwable {425 JMLValueSet.singleton(e);426 }427 protected java.lang.String failMessage428 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)429 {430 java.lang.String msg = "\n\tMethod 'singleton' applied to";431 msg += "\n\tReceiver class JMLValueSet";432 msg += "\n\tArgument e: " + this.e;433 return msg;434 }435 }436 /** Add tests for the convertFrom method437 * to the overall test suite. */438 private void addTestSuiteFor$TestConvertFrom439 (junit.framework.TestSuite overallTestSuite$)440 {441 junit.framework.TestSuite methodTests$442 = this.emptyTestSuiteFor("convertFrom");443 try {444 org.jmlspecs.jmlunit.strategies.IndefiniteIterator445 vorg_jmlspecs_models_JMLType$_$1$iter446 = this.vorg_jmlspecs_models_JMLType$_Iter("convertFrom", 0);447 this.check_has_data448 (vorg_jmlspecs_models_JMLType$_$1$iter,449 "this.vorg_jmlspecs_models_JMLType$_Iter(\"convertFrom\", 0)");450 while (!vorg_jmlspecs_models_JMLType$_$1$iter.atEnd()) {451 final org.jmlspecs.models.JMLType[] a452 = (org.jmlspecs.models.JMLType[]) vorg_jmlspecs_models_JMLType$_$1$iter.get();453 methodTests$.addTest454 (new TestConvertFrom(a));455 vorg_jmlspecs_models_JMLType$_$1$iter.advance();456 }457 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {458 // methodTests$ doesn't want more tests459 }460 overallTestSuite$.addTest(methodTests$);461 }462 /** Test for the convertFrom method. */463 protected static class TestConvertFrom extends OneTest {464 /** Argument a */465 private org.jmlspecs.models.JMLType[] a;466 /** Initialize this instance. */467 public TestConvertFrom(org.jmlspecs.models.JMLType[] a) {468 super("convertFrom"+ ":" + (a==null?"null":("{org.jmlspecs.models.JMLType["+a.length + "]"+"}")));469 this.a = a;470 }471 protected void doCall() throws java.lang.Throwable {472 JMLValueSet.convertFrom(a);473 }474 protected java.lang.String failMessage475 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)476 {477 java.lang.String msg = "\n\tMethod 'convertFrom' applied to";478 msg += "\n\tReceiver class JMLValueSet";479 msg += "\n\tArgument a: " + this.a;480 return msg;481 }482 }483 /** Add tests for the convertFrom method484 * to the overall test suite. */485 private void addTestSuiteFor$TestConvertFrom$1486 (junit.framework.TestSuite overallTestSuite$)487 {488 junit.framework.TestSuite methodTests$489 = this.emptyTestSuiteFor("convertFrom");490 try {491 org.jmlspecs.jmlunit.strategies.IndefiniteIterator492 vjava_util_Collection$1$iter493 = this.vjava_util_CollectionIter("convertFrom", 0);494 this.check_has_data495 (vjava_util_Collection$1$iter,496 "this.vjava_util_CollectionIter(\"convertFrom\", 0)");497 while (!vjava_util_Collection$1$iter.atEnd()) {498 final java.util.Collection c499 = (java.util.Collection) vjava_util_Collection$1$iter.get();500 methodTests$.addTest501 (new TestConvertFrom$1(c));502 vjava_util_Collection$1$iter.advance();503 }504 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {505 // methodTests$ doesn't want more tests506 }507 overallTestSuite$.addTest(methodTests$);508 }509 /** Test for the convertFrom method. */510 protected static class TestConvertFrom$1 extends OneTest {511 /** Argument c */512 private java.util.Collection c;513 /** Initialize this instance. */514 public TestConvertFrom$1(java.util.Collection c) {515 super("convertFrom"+ ":" + (c==null? "null" :"{java.util.Collection}"));516 this.c = c;517 }518 protected void doCall() throws java.lang.Throwable {519 JMLValueSet.convertFrom(c);520 }521 protected java.lang.String failMessage522 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)523 {524 java.lang.String msg = "\n\tMethod 'convertFrom' applied to";525 msg += "\n\tReceiver class JMLValueSet";526 msg += "\n\tArgument c: " + this.c;527 return msg;528 }529 }530 /** Add tests for the convertFrom method531 * to the overall test suite. */532 private void addTestSuiteFor$TestConvertFrom$2533 (junit.framework.TestSuite overallTestSuite$)534 {535 junit.framework.TestSuite methodTests$536 = this.emptyTestSuiteFor("convertFrom");537 try {538 org.jmlspecs.jmlunit.strategies.IndefiniteIterator539 vorg_jmlspecs_models_JMLCollection$1$iter540 = this.vorg_jmlspecs_models_JMLCollectionIter("convertFrom", 0);541 this.check_has_data542 (vorg_jmlspecs_models_JMLCollection$1$iter,543 "this.vorg_jmlspecs_models_JMLCollectionIter(\"convertFrom\", 0)");544 while (!vorg_jmlspecs_models_JMLCollection$1$iter.atEnd()) {545 final org.jmlspecs.models.JMLCollection c546 = (org.jmlspecs.models.JMLCollection) vorg_jmlspecs_models_JMLCollection$1$iter.get();547 methodTests$.addTest548 (new TestConvertFrom$2(c));549 vorg_jmlspecs_models_JMLCollection$1$iter.advance();550 }551 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {552 // methodTests$ doesn't want more tests553 }554 overallTestSuite$.addTest(methodTests$);555 }556 /** Test for the convertFrom method. */557 protected static class TestConvertFrom$2 extends OneTest {558 /** Argument c */559 private org.jmlspecs.models.JMLCollection c;560 /** Initialize this instance. */561 public TestConvertFrom$2(org.jmlspecs.models.JMLCollection c) {562 super("convertFrom"+ ":" + (c==null? "null" :"{org.jmlspecs.models.JMLCollection}"));563 this.c = c;564 }565 protected void doCall() throws java.lang.Throwable {566 JMLValueSet.convertFrom(c);567 }568 protected java.lang.String failMessage569 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)570 {571 java.lang.String msg = "\n\tMethod 'convertFrom' applied to";572 msg += "\n\tReceiver class JMLValueSet";573 msg += "\n\tArgument c: " + this.c;574 return msg;575 }576 }577 /** Add tests for the has method578 * to the overall test suite. */579 private void addTestSuiteFor$TestHas580 (junit.framework.TestSuite overallTestSuite$)581 {582 junit.framework.TestSuite methodTests$583 = this.emptyTestSuiteFor("has");584 try {585 org.jmlspecs.jmlunit.strategies.IndefiniteIterator586 receivers$iter587 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator588 (this.vorg_jmlspecs_models_JMLValueSetIter("has", 1));589 this.check_has_data590 (receivers$iter,591 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"has\", 1))");592 while (!receivers$iter.atEnd()) {593 org.jmlspecs.jmlunit.strategies.IndefiniteIterator594 vorg_jmlspecs_models_JMLType$1$iter595 = this.vorg_jmlspecs_models_JMLTypeIter("has", 0);596 this.check_has_data597 (vorg_jmlspecs_models_JMLType$1$iter,598 "this.vorg_jmlspecs_models_JMLTypeIter(\"has\", 0)");599 while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) {600 final org.jmlspecs.models.JMLValueSet receiver$601 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();602 final org.jmlspecs.models.JMLType elem603 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get();604 methodTests$.addTest605 (new TestHas(receiver$, elem));606 vorg_jmlspecs_models_JMLType$1$iter.advance();607 }608 receivers$iter.advance();609 }610 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {611 // methodTests$ doesn't want more tests612 }613 overallTestSuite$.addTest(methodTests$);614 }615 /** Test for the has method. */616 protected static class TestHas extends OneTest {617 /** The receiver */618 private org.jmlspecs.models.JMLValueSet receiver$;619 /** Argument elem */620 private org.jmlspecs.models.JMLType elem;621 /** Initialize this instance. */622 public TestHas(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLType elem) {623 super("has"+ ":" + (elem==null? "null" :"{org.jmlspecs.models.JMLType}"));624 this.receiver$ = receiver$;625 this.elem = elem;626 }627 protected void doCall() throws java.lang.Throwable {628 receiver$.has(elem);629 }630 protected java.lang.String failMessage631 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)632 {633 java.lang.String msg = "\n\tMethod 'has' applied to";634 msg += "\n\tReceiver: " + this.receiver$;635 msg += "\n\tArgument elem: " + this.elem;636 return msg;637 }638 }639 /** Add tests for the containsAll method640 * to the overall test suite. */641 private void addTestSuiteFor$TestContainsAll642 (junit.framework.TestSuite overallTestSuite$)643 {644 junit.framework.TestSuite methodTests$645 = this.emptyTestSuiteFor("containsAll");646 try {647 org.jmlspecs.jmlunit.strategies.IndefiniteIterator648 receivers$iter649 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator650 (this.vorg_jmlspecs_models_JMLValueSetIter("containsAll", 1));651 this.check_has_data652 (receivers$iter,653 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"containsAll\", 1))");654 while (!receivers$iter.atEnd()) {655 org.jmlspecs.jmlunit.strategies.IndefiniteIterator656 vjava_util_Collection$1$iter657 = this.vjava_util_CollectionIter("containsAll", 0);658 this.check_has_data659 (vjava_util_Collection$1$iter,660 "this.vjava_util_CollectionIter(\"containsAll\", 0)");661 while (!vjava_util_Collection$1$iter.atEnd()) {662 final org.jmlspecs.models.JMLValueSet receiver$663 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();664 final java.util.Collection c665 = (java.util.Collection) vjava_util_Collection$1$iter.get();666 methodTests$.addTest667 (new TestContainsAll(receiver$, c));668 vjava_util_Collection$1$iter.advance();669 }670 receivers$iter.advance();671 }672 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {673 // methodTests$ doesn't want more tests674 }675 overallTestSuite$.addTest(methodTests$);676 }677 /** Test for the containsAll method. */678 protected static class TestContainsAll extends OneTest {679 /** The receiver */680 private org.jmlspecs.models.JMLValueSet receiver$;681 /** Argument c */682 private java.util.Collection c;683 /** Initialize this instance. */684 public TestContainsAll(org.jmlspecs.models.JMLValueSet receiver$, java.util.Collection c) {685 super("containsAll"+ ":" + (c==null? "null" :"{java.util.Collection}"));686 this.receiver$ = receiver$;687 this.c = c;688 }689 protected void doCall() throws java.lang.Throwable {690 receiver$.containsAll(c);691 }692 protected java.lang.String failMessage693 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)694 {695 java.lang.String msg = "\n\tMethod 'containsAll' applied to";696 msg += "\n\tReceiver: " + this.receiver$;697 msg += "\n\tArgument c: " + this.c;698 return msg;699 }700 }701 /** Add tests for the equals method702 * to the overall test suite. */703 private void addTestSuiteFor$TestEquals704 (junit.framework.TestSuite overallTestSuite$)705 {706 junit.framework.TestSuite methodTests$707 = this.emptyTestSuiteFor("equals");708 try {709 org.jmlspecs.jmlunit.strategies.IndefiniteIterator710 receivers$iter711 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator712 (this.vorg_jmlspecs_models_JMLValueSetIter("equals", 1));713 this.check_has_data714 (receivers$iter,715 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"equals\", 1))");716 while (!receivers$iter.atEnd()) {717 org.jmlspecs.jmlunit.strategies.IndefiniteIterator718 vjava_lang_Object$1$iter719 = this.vjava_lang_ObjectIter("equals", 0);720 this.check_has_data721 (vjava_lang_Object$1$iter,722 "this.vjava_lang_ObjectIter(\"equals\", 0)");723 while (!vjava_lang_Object$1$iter.atEnd()) {724 final org.jmlspecs.models.JMLValueSet receiver$725 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();726 final java.lang.Object s2727 = (java.lang.Object) vjava_lang_Object$1$iter.get();728 methodTests$.addTest729 (new TestEquals(receiver$, s2));730 vjava_lang_Object$1$iter.advance();731 }732 receivers$iter.advance();733 }734 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {735 // methodTests$ doesn't want more tests736 }737 overallTestSuite$.addTest(methodTests$);738 }739 /** Test for the equals method. */740 protected static class TestEquals extends OneTest {741 /** The receiver */742 private org.jmlspecs.models.JMLValueSet receiver$;743 /** Argument s2 */744 private java.lang.Object s2;745 /** Initialize this instance. */746 public TestEquals(org.jmlspecs.models.JMLValueSet receiver$, java.lang.Object s2) {747 super("equals"+ ":" + (s2==null? "null" :"{java.lang.Object}"));748 this.receiver$ = receiver$;749 this.s2 = s2;750 }751 protected void doCall() throws java.lang.Throwable {752 receiver$.equals(s2);753 }754 protected java.lang.String failMessage755 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)756 {757 java.lang.String msg = "\n\tMethod 'equals' applied to";758 msg += "\n\tReceiver: " + this.receiver$;759 msg += "\n\tArgument s2: " + this.s2;760 return msg;761 }762 }763 /** Add tests for the hashCode method764 * to the overall test suite. */765 private void addTestSuiteFor$TestHashCode766 (junit.framework.TestSuite overallTestSuite$)767 {768 junit.framework.TestSuite methodTests$769 = this.emptyTestSuiteFor("hashCode");770 try {771 org.jmlspecs.jmlunit.strategies.IndefiniteIterator772 receivers$iter773 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator774 (this.vorg_jmlspecs_models_JMLValueSetIter("hashCode", 0));775 this.check_has_data776 (receivers$iter,777 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"hashCode\", 0))");778 while (!receivers$iter.atEnd()) {779 final org.jmlspecs.models.JMLValueSet receiver$780 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();781 methodTests$.addTest782 (new TestHashCode(receiver$));783 receivers$iter.advance();784 }785 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {786 // methodTests$ doesn't want more tests787 }788 overallTestSuite$.addTest(methodTests$);789 }790 /** Test for the hashCode method. */791 protected static class TestHashCode extends OneTest {792 /** The receiver */793 private org.jmlspecs.models.JMLValueSet receiver$;794 /** Initialize this instance. */795 public TestHashCode(org.jmlspecs.models.JMLValueSet receiver$) {796 super("hashCode");797 this.receiver$ = receiver$;798 }799 protected void doCall() throws java.lang.Throwable {800 receiver$.hashCode();801 }802 protected java.lang.String failMessage803 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)804 {805 java.lang.String msg = "\n\tMethod 'hashCode' applied to";806 msg += "\n\tReceiver: " + this.receiver$;807 return msg;808 }809 }810 /** Add tests for the isEmpty method811 * to the overall test suite. */812 private void addTestSuiteFor$TestIsEmpty813 (junit.framework.TestSuite overallTestSuite$)814 {815 junit.framework.TestSuite methodTests$816 = this.emptyTestSuiteFor("isEmpty");817 try {818 org.jmlspecs.jmlunit.strategies.IndefiniteIterator819 receivers$iter820 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator821 (this.vorg_jmlspecs_models_JMLValueSetIter("isEmpty", 0));822 this.check_has_data823 (receivers$iter,824 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"isEmpty\", 0))");825 while (!receivers$iter.atEnd()) {826 final org.jmlspecs.models.JMLValueSet receiver$827 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();828 methodTests$.addTest829 (new TestIsEmpty(receiver$));830 receivers$iter.advance();831 }832 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {833 // methodTests$ doesn't want more tests834 }835 overallTestSuite$.addTest(methodTests$);836 }837 /** Test for the isEmpty method. */838 protected static class TestIsEmpty extends OneTest {839 /** The receiver */840 private org.jmlspecs.models.JMLValueSet receiver$;841 /** Initialize this instance. */842 public TestIsEmpty(org.jmlspecs.models.JMLValueSet receiver$) {843 super("isEmpty");844 this.receiver$ = receiver$;845 }846 protected void doCall() throws java.lang.Throwable {847 receiver$.isEmpty();848 }849 protected java.lang.String failMessage850 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)851 {852 java.lang.String msg = "\n\tMethod 'isEmpty' applied to";853 msg += "\n\tReceiver: " + this.receiver$;854 return msg;855 }856 }857 /** Add tests for the int_size method858 * to the overall test suite. */859 private void addTestSuiteFor$TestInt_size860 (junit.framework.TestSuite overallTestSuite$)861 {862 junit.framework.TestSuite methodTests$863 = this.emptyTestSuiteFor("int_size");864 try {865 org.jmlspecs.jmlunit.strategies.IndefiniteIterator866 receivers$iter867 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator868 (this.vorg_jmlspecs_models_JMLValueSetIter("int_size", 0));869 this.check_has_data870 (receivers$iter,871 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"int_size\", 0))");872 while (!receivers$iter.atEnd()) {873 final org.jmlspecs.models.JMLValueSet receiver$874 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();875 methodTests$.addTest876 (new TestInt_size(receiver$));877 receivers$iter.advance();878 }879 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {880 // methodTests$ doesn't want more tests881 }882 overallTestSuite$.addTest(methodTests$);883 }884 /** Test for the int_size method. */885 protected static class TestInt_size extends OneTest {886 /** The receiver */887 private org.jmlspecs.models.JMLValueSet receiver$;888 /** Initialize this instance. */889 public TestInt_size(org.jmlspecs.models.JMLValueSet receiver$) {890 super("int_size");891 this.receiver$ = receiver$;892 }893 protected void doCall() throws java.lang.Throwable {894 receiver$.int_size();895 }896 protected java.lang.String failMessage897 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)898 {899 java.lang.String msg = "\n\tMethod 'int_size' applied to";900 msg += "\n\tReceiver: " + this.receiver$;901 return msg;902 }903 }904 /** Add tests for the isSubset method905 * to the overall test suite. */906 private void addTestSuiteFor$TestIsSubset907 (junit.framework.TestSuite overallTestSuite$)908 {909 junit.framework.TestSuite methodTests$910 = this.emptyTestSuiteFor("isSubset");911 try {912 org.jmlspecs.jmlunit.strategies.IndefiniteIterator913 receivers$iter914 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator915 (this.vorg_jmlspecs_models_JMLValueSetIter("isSubset", 1));916 this.check_has_data917 (receivers$iter,918 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"isSubset\", 1))");919 while (!receivers$iter.atEnd()) {920 org.jmlspecs.jmlunit.strategies.IndefiniteIterator921 vorg_jmlspecs_models_JMLValueSet$1$iter922 = this.vorg_jmlspecs_models_JMLValueSetIter("isSubset", 0);923 this.check_has_data924 (vorg_jmlspecs_models_JMLValueSet$1$iter,925 "this.vorg_jmlspecs_models_JMLValueSetIter(\"isSubset\", 0)");926 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {927 final org.jmlspecs.models.JMLValueSet receiver$928 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();929 final org.jmlspecs.models.JMLValueSet s2930 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();931 methodTests$.addTest932 (new TestIsSubset(receiver$, s2));933 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();934 }935 receivers$iter.advance();936 }937 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {938 // methodTests$ doesn't want more tests939 }940 overallTestSuite$.addTest(methodTests$);941 }942 /** Test for the isSubset method. */943 protected static class TestIsSubset extends OneTest {944 /** The receiver */945 private org.jmlspecs.models.JMLValueSet receiver$;946 /** Argument s2 */947 private org.jmlspecs.models.JMLValueSet s2;948 /** Initialize this instance. */949 public TestIsSubset(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {950 super("isSubset"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));951 this.receiver$ = receiver$;952 this.s2 = s2;953 }954 protected void doCall() throws java.lang.Throwable {955 receiver$.isSubset(s2);956 }957 protected java.lang.String failMessage958 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)959 {960 java.lang.String msg = "\n\tMethod 'isSubset' applied to";961 msg += "\n\tReceiver: " + this.receiver$;962 msg += "\n\tArgument s2: " + this.s2;963 return msg;964 }965 }966 /** Add tests for the isProperSubset method967 * to the overall test suite. */968 private void addTestSuiteFor$TestIsProperSubset969 (junit.framework.TestSuite overallTestSuite$)970 {971 junit.framework.TestSuite methodTests$972 = this.emptyTestSuiteFor("isProperSubset");973 try {974 org.jmlspecs.jmlunit.strategies.IndefiniteIterator975 receivers$iter976 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator977 (this.vorg_jmlspecs_models_JMLValueSetIter("isProperSubset", 1));978 this.check_has_data979 (receivers$iter,980 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"isProperSubset\", 1))");981 while (!receivers$iter.atEnd()) {982 org.jmlspecs.jmlunit.strategies.IndefiniteIterator983 vorg_jmlspecs_models_JMLValueSet$1$iter984 = this.vorg_jmlspecs_models_JMLValueSetIter("isProperSubset", 0);985 this.check_has_data986 (vorg_jmlspecs_models_JMLValueSet$1$iter,987 "this.vorg_jmlspecs_models_JMLValueSetIter(\"isProperSubset\", 0)");988 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {989 final org.jmlspecs.models.JMLValueSet receiver$990 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();991 final org.jmlspecs.models.JMLValueSet s2992 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();993 methodTests$.addTest994 (new TestIsProperSubset(receiver$, s2));995 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();996 }997 receivers$iter.advance();998 }999 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1000 // methodTests$ doesn't want more tests1001 }1002 overallTestSuite$.addTest(methodTests$);1003 }1004 /** Test for the isProperSubset method. */1005 protected static class TestIsProperSubset extends OneTest {1006 /** The receiver */1007 private org.jmlspecs.models.JMLValueSet receiver$;1008 /** Argument s2 */1009 private org.jmlspecs.models.JMLValueSet s2;1010 /** Initialize this instance. */1011 public TestIsProperSubset(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1012 super("isProperSubset"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1013 this.receiver$ = receiver$;1014 this.s2 = s2;1015 }1016 protected void doCall() throws java.lang.Throwable {1017 receiver$.isProperSubset(s2);1018 }1019 protected java.lang.String failMessage1020 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1021 {1022 java.lang.String msg = "\n\tMethod 'isProperSubset' applied to";1023 msg += "\n\tReceiver: " + this.receiver$;1024 msg += "\n\tArgument s2: " + this.s2;1025 return msg;1026 }1027 }1028 /** Add tests for the isSuperset method1029 * to the overall test suite. */1030 private void addTestSuiteFor$TestIsSuperset1031 (junit.framework.TestSuite overallTestSuite$)1032 {1033 junit.framework.TestSuite methodTests$1034 = this.emptyTestSuiteFor("isSuperset");1035 try {1036 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1037 receivers$iter1038 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1039 (this.vorg_jmlspecs_models_JMLValueSetIter("isSuperset", 1));1040 this.check_has_data1041 (receivers$iter,1042 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"isSuperset\", 1))");1043 while (!receivers$iter.atEnd()) {1044 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1045 vorg_jmlspecs_models_JMLValueSet$1$iter1046 = this.vorg_jmlspecs_models_JMLValueSetIter("isSuperset", 0);1047 this.check_has_data1048 (vorg_jmlspecs_models_JMLValueSet$1$iter,1049 "this.vorg_jmlspecs_models_JMLValueSetIter(\"isSuperset\", 0)");1050 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {1051 final org.jmlspecs.models.JMLValueSet receiver$1052 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1053 final org.jmlspecs.models.JMLValueSet s21054 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();1055 methodTests$.addTest1056 (new TestIsSuperset(receiver$, s2));1057 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();1058 }1059 receivers$iter.advance();1060 }1061 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1062 // methodTests$ doesn't want more tests1063 }1064 overallTestSuite$.addTest(methodTests$);1065 }1066 /** Test for the isSuperset method. */1067 protected static class TestIsSuperset extends OneTest {1068 /** The receiver */1069 private org.jmlspecs.models.JMLValueSet receiver$;1070 /** Argument s2 */1071 private org.jmlspecs.models.JMLValueSet s2;1072 /** Initialize this instance. */1073 public TestIsSuperset(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1074 super("isSuperset"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1075 this.receiver$ = receiver$;1076 this.s2 = s2;1077 }1078 protected void doCall() throws java.lang.Throwable {1079 receiver$.isSuperset(s2);1080 }1081 protected java.lang.String failMessage1082 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1083 {1084 java.lang.String msg = "\n\tMethod 'isSuperset' applied to";1085 msg += "\n\tReceiver: " + this.receiver$;1086 msg += "\n\tArgument s2: " + this.s2;1087 return msg;1088 }1089 }1090 /** Add tests for the isProperSuperset method1091 * to the overall test suite. */1092 private void addTestSuiteFor$TestIsProperSuperset1093 (junit.framework.TestSuite overallTestSuite$)1094 {1095 junit.framework.TestSuite methodTests$1096 = this.emptyTestSuiteFor("isProperSuperset");1097 try {1098 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1099 receivers$iter1100 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1101 (this.vorg_jmlspecs_models_JMLValueSetIter("isProperSuperset", 1));1102 this.check_has_data1103 (receivers$iter,1104 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"isProperSuperset\", 1))");1105 while (!receivers$iter.atEnd()) {1106 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1107 vorg_jmlspecs_models_JMLValueSet$1$iter1108 = this.vorg_jmlspecs_models_JMLValueSetIter("isProperSuperset", 0);1109 this.check_has_data1110 (vorg_jmlspecs_models_JMLValueSet$1$iter,1111 "this.vorg_jmlspecs_models_JMLValueSetIter(\"isProperSuperset\", 0)");1112 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {1113 final org.jmlspecs.models.JMLValueSet receiver$1114 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1115 final org.jmlspecs.models.JMLValueSet s21116 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();1117 methodTests$.addTest1118 (new TestIsProperSuperset(receiver$, s2));1119 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();1120 }1121 receivers$iter.advance();1122 }1123 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1124 // methodTests$ doesn't want more tests1125 }1126 overallTestSuite$.addTest(methodTests$);1127 }1128 /** Test for the isProperSuperset method. */1129 protected static class TestIsProperSuperset extends OneTest {1130 /** The receiver */1131 private org.jmlspecs.models.JMLValueSet receiver$;1132 /** Argument s2 */1133 private org.jmlspecs.models.JMLValueSet s2;1134 /** Initialize this instance. */1135 public TestIsProperSuperset(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1136 super("isProperSuperset"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1137 this.receiver$ = receiver$;1138 this.s2 = s2;1139 }1140 protected void doCall() throws java.lang.Throwable {1141 receiver$.isProperSuperset(s2);1142 }1143 protected java.lang.String failMessage1144 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1145 {1146 java.lang.String msg = "\n\tMethod 'isProperSuperset' applied to";1147 msg += "\n\tReceiver: " + this.receiver$;1148 msg += "\n\tArgument s2: " + this.s2;1149 return msg;1150 }1151 }1152 /** Add tests for the choose method1153 * to the overall test suite. */1154 private void addTestSuiteFor$TestChoose1155 (junit.framework.TestSuite overallTestSuite$)1156 {1157 junit.framework.TestSuite methodTests$1158 = this.emptyTestSuiteFor("choose");1159 try {1160 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1161 receivers$iter1162 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1163 (this.vorg_jmlspecs_models_JMLValueSetIter("choose", 0));1164 this.check_has_data1165 (receivers$iter,1166 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"choose\", 0))");1167 while (!receivers$iter.atEnd()) {1168 final org.jmlspecs.models.JMLValueSet receiver$1169 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1170 methodTests$.addTest1171 (new TestChoose(receiver$));1172 receivers$iter.advance();1173 }1174 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1175 // methodTests$ doesn't want more tests1176 }1177 overallTestSuite$.addTest(methodTests$);1178 }1179 /** Test for the choose method. */1180 protected static class TestChoose extends OneTest {1181 /** The receiver */1182 private org.jmlspecs.models.JMLValueSet receiver$;1183 /** Initialize this instance. */1184 public TestChoose(org.jmlspecs.models.JMLValueSet receiver$) {1185 super("choose");1186 this.receiver$ = receiver$;1187 }1188 protected void doCall() throws java.lang.Throwable {1189 receiver$.choose();1190 }1191 protected java.lang.String failMessage1192 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1193 {1194 java.lang.String msg = "\n\tMethod 'choose' applied to";1195 msg += "\n\tReceiver: " + this.receiver$;1196 return msg;1197 }1198 }1199 /** Add tests for the clone method1200 * to the overall test suite. */1201 private void addTestSuiteFor$TestClone1202 (junit.framework.TestSuite overallTestSuite$)1203 {1204 junit.framework.TestSuite methodTests$1205 = this.emptyTestSuiteFor("clone");1206 try {1207 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1208 receivers$iter1209 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1210 (this.vorg_jmlspecs_models_JMLValueSetIter("clone", 0));1211 this.check_has_data1212 (receivers$iter,1213 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"clone\", 0))");1214 while (!receivers$iter.atEnd()) {1215 final org.jmlspecs.models.JMLValueSet receiver$1216 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1217 methodTests$.addTest1218 (new TestClone(receiver$));1219 receivers$iter.advance();1220 }1221 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1222 // methodTests$ doesn't want more tests1223 }1224 overallTestSuite$.addTest(methodTests$);1225 }1226 /** Test for the clone method. */1227 protected static class TestClone extends OneTest {1228 /** The receiver */1229 private org.jmlspecs.models.JMLValueSet receiver$;1230 /** Initialize this instance. */1231 public TestClone(org.jmlspecs.models.JMLValueSet receiver$) {1232 super("clone");1233 this.receiver$ = receiver$;1234 }1235 protected void doCall() throws java.lang.Throwable {1236 receiver$.clone();1237 }1238 protected java.lang.String failMessage1239 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1240 {1241 java.lang.String msg = "\n\tMethod 'clone' applied to";1242 msg += "\n\tReceiver: " + this.receiver$;1243 return msg;1244 }1245 }1246 /** Add tests for the insert method1247 * to the overall test suite. */1248 private void addTestSuiteFor$TestInsert1249 (junit.framework.TestSuite overallTestSuite$)1250 {1251 junit.framework.TestSuite methodTests$1252 = this.emptyTestSuiteFor("insert");1253 try {1254 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1255 receivers$iter1256 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1257 (this.vorg_jmlspecs_models_JMLValueSetIter("insert", 1));1258 this.check_has_data1259 (receivers$iter,1260 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"insert\", 1))");1261 while (!receivers$iter.atEnd()) {1262 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1263 vorg_jmlspecs_models_JMLType$1$iter1264 = this.vorg_jmlspecs_models_JMLTypeIter("insert", 0);1265 this.check_has_data1266 (vorg_jmlspecs_models_JMLType$1$iter,1267 "this.vorg_jmlspecs_models_JMLTypeIter(\"insert\", 0)");1268 while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) {1269 final org.jmlspecs.models.JMLValueSet receiver$1270 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1271 final org.jmlspecs.models.JMLType elem1272 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get();1273 methodTests$.addTest1274 (new TestInsert(receiver$, elem));1275 vorg_jmlspecs_models_JMLType$1$iter.advance();1276 }1277 receivers$iter.advance();1278 }1279 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1280 // methodTests$ doesn't want more tests1281 }1282 overallTestSuite$.addTest(methodTests$);1283 }1284 /** Test for the insert method. */1285 protected static class TestInsert extends OneTest {1286 /** The receiver */1287 private org.jmlspecs.models.JMLValueSet receiver$;1288 /** Argument elem */1289 private org.jmlspecs.models.JMLType elem;1290 /** Initialize this instance. */1291 public TestInsert(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLType elem) {1292 super("insert"+ ":" + (elem==null? "null" :"{org.jmlspecs.models.JMLType}"));1293 this.receiver$ = receiver$;1294 this.elem = elem;1295 }1296 protected void doCall() throws java.lang.Throwable {1297 receiver$.insert(elem);1298 }1299 protected java.lang.String failMessage1300 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1301 {1302 java.lang.String msg = "\n\tMethod 'insert' applied to";1303 msg += "\n\tReceiver: " + this.receiver$;1304 msg += "\n\tArgument elem: " + this.elem;1305 return msg;1306 }1307 }1308 /** Add tests for the remove method1309 * to the overall test suite. */1310 private void addTestSuiteFor$TestRemove1311 (junit.framework.TestSuite overallTestSuite$)1312 {1313 junit.framework.TestSuite methodTests$1314 = this.emptyTestSuiteFor("remove");1315 try {1316 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1317 receivers$iter1318 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1319 (this.vorg_jmlspecs_models_JMLValueSetIter("remove", 1));1320 this.check_has_data1321 (receivers$iter,1322 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"remove\", 1))");1323 while (!receivers$iter.atEnd()) {1324 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1325 vorg_jmlspecs_models_JMLType$1$iter1326 = this.vorg_jmlspecs_models_JMLTypeIter("remove", 0);1327 this.check_has_data1328 (vorg_jmlspecs_models_JMLType$1$iter,1329 "this.vorg_jmlspecs_models_JMLTypeIter(\"remove\", 0)");1330 while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) {1331 final org.jmlspecs.models.JMLValueSet receiver$1332 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1333 final org.jmlspecs.models.JMLType elem1334 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get();1335 methodTests$.addTest1336 (new TestRemove(receiver$, elem));1337 vorg_jmlspecs_models_JMLType$1$iter.advance();1338 }1339 receivers$iter.advance();1340 }1341 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1342 // methodTests$ doesn't want more tests1343 }1344 overallTestSuite$.addTest(methodTests$);1345 }1346 /** Test for the remove method. */1347 protected static class TestRemove extends OneTest {1348 /** The receiver */1349 private org.jmlspecs.models.JMLValueSet receiver$;1350 /** Argument elem */1351 private org.jmlspecs.models.JMLType elem;1352 /** Initialize this instance. */1353 public TestRemove(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLType elem) {1354 super("remove"+ ":" + (elem==null? "null" :"{org.jmlspecs.models.JMLType}"));1355 this.receiver$ = receiver$;1356 this.elem = elem;1357 }1358 protected void doCall() throws java.lang.Throwable {1359 receiver$.remove(elem);1360 }1361 protected java.lang.String failMessage1362 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1363 {1364 java.lang.String msg = "\n\tMethod 'remove' applied to";1365 msg += "\n\tReceiver: " + this.receiver$;1366 msg += "\n\tArgument elem: " + this.elem;1367 return msg;1368 }1369 }1370 /** Add tests for the intersection method1371 * to the overall test suite. */1372 private void addTestSuiteFor$TestIntersection1373 (junit.framework.TestSuite overallTestSuite$)1374 {1375 junit.framework.TestSuite methodTests$1376 = this.emptyTestSuiteFor("intersection");1377 try {1378 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1379 receivers$iter1380 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1381 (this.vorg_jmlspecs_models_JMLValueSetIter("intersection", 1));1382 this.check_has_data1383 (receivers$iter,1384 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"intersection\", 1))");1385 while (!receivers$iter.atEnd()) {1386 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1387 vorg_jmlspecs_models_JMLValueSet$1$iter1388 = this.vorg_jmlspecs_models_JMLValueSetIter("intersection", 0);1389 this.check_has_data1390 (vorg_jmlspecs_models_JMLValueSet$1$iter,1391 "this.vorg_jmlspecs_models_JMLValueSetIter(\"intersection\", 0)");1392 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {1393 final org.jmlspecs.models.JMLValueSet receiver$1394 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1395 final org.jmlspecs.models.JMLValueSet s21396 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();1397 methodTests$.addTest1398 (new TestIntersection(receiver$, s2));1399 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();1400 }1401 receivers$iter.advance();1402 }1403 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1404 // methodTests$ doesn't want more tests1405 }1406 overallTestSuite$.addTest(methodTests$);1407 }1408 /** Test for the intersection method. */1409 protected static class TestIntersection extends OneTest {1410 /** The receiver */1411 private org.jmlspecs.models.JMLValueSet receiver$;1412 /** Argument s2 */1413 private org.jmlspecs.models.JMLValueSet s2;1414 /** Initialize this instance. */1415 public TestIntersection(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1416 super("intersection"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1417 this.receiver$ = receiver$;1418 this.s2 = s2;1419 }1420 protected void doCall() throws java.lang.Throwable {1421 receiver$.intersection(s2);1422 }1423 protected java.lang.String failMessage1424 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1425 {1426 java.lang.String msg = "\n\tMethod 'intersection' applied to";1427 msg += "\n\tReceiver: " + this.receiver$;1428 msg += "\n\tArgument s2: " + this.s2;1429 return msg;1430 }1431 }1432 /** Add tests for the union method1433 * to the overall test suite. */1434 private void addTestSuiteFor$TestUnion1435 (junit.framework.TestSuite overallTestSuite$)1436 {1437 junit.framework.TestSuite methodTests$1438 = this.emptyTestSuiteFor("union");1439 try {1440 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1441 receivers$iter1442 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1443 (this.vorg_jmlspecs_models_JMLValueSetIter("union", 1));1444 this.check_has_data1445 (receivers$iter,1446 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"union\", 1))");1447 while (!receivers$iter.atEnd()) {1448 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1449 vorg_jmlspecs_models_JMLValueSet$1$iter1450 = this.vorg_jmlspecs_models_JMLValueSetIter("union", 0);1451 this.check_has_data1452 (vorg_jmlspecs_models_JMLValueSet$1$iter,1453 "this.vorg_jmlspecs_models_JMLValueSetIter(\"union\", 0)");1454 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {1455 final org.jmlspecs.models.JMLValueSet receiver$1456 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1457 final org.jmlspecs.models.JMLValueSet s21458 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();1459 methodTests$.addTest1460 (new TestUnion(receiver$, s2));1461 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();1462 }1463 receivers$iter.advance();1464 }1465 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1466 // methodTests$ doesn't want more tests1467 }1468 overallTestSuite$.addTest(methodTests$);1469 }1470 /** Test for the union method. */1471 protected static class TestUnion extends OneTest {1472 /** The receiver */1473 private org.jmlspecs.models.JMLValueSet receiver$;1474 /** Argument s2 */1475 private org.jmlspecs.models.JMLValueSet s2;1476 /** Initialize this instance. */1477 public TestUnion(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1478 super("union"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1479 this.receiver$ = receiver$;1480 this.s2 = s2;1481 }1482 protected void doCall() throws java.lang.Throwable {1483 receiver$.union(s2);1484 }1485 protected java.lang.String failMessage1486 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1487 {1488 java.lang.String msg = "\n\tMethod 'union' applied to";1489 msg += "\n\tReceiver: " + this.receiver$;1490 msg += "\n\tArgument s2: " + this.s2;1491 return msg;1492 }1493 }1494 /** Add tests for the difference method1495 * to the overall test suite. */1496 private void addTestSuiteFor$TestDifference1497 (junit.framework.TestSuite overallTestSuite$)1498 {1499 junit.framework.TestSuite methodTests$1500 = this.emptyTestSuiteFor("difference");1501 try {1502 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1503 receivers$iter1504 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1505 (this.vorg_jmlspecs_models_JMLValueSetIter("difference", 1));1506 this.check_has_data1507 (receivers$iter,1508 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"difference\", 1))");1509 while (!receivers$iter.atEnd()) {1510 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1511 vorg_jmlspecs_models_JMLValueSet$1$iter1512 = this.vorg_jmlspecs_models_JMLValueSetIter("difference", 0);1513 this.check_has_data1514 (vorg_jmlspecs_models_JMLValueSet$1$iter,1515 "this.vorg_jmlspecs_models_JMLValueSetIter(\"difference\", 0)");1516 while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) {1517 final org.jmlspecs.models.JMLValueSet receiver$1518 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1519 final org.jmlspecs.models.JMLValueSet s21520 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get();1521 methodTests$.addTest1522 (new TestDifference(receiver$, s2));1523 vorg_jmlspecs_models_JMLValueSet$1$iter.advance();1524 }1525 receivers$iter.advance();1526 }1527 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1528 // methodTests$ doesn't want more tests1529 }1530 overallTestSuite$.addTest(methodTests$);1531 }1532 /** Test for the difference method. */1533 protected static class TestDifference extends OneTest {1534 /** The receiver */1535 private org.jmlspecs.models.JMLValueSet receiver$;1536 /** Argument s2 */1537 private org.jmlspecs.models.JMLValueSet s2;1538 /** Initialize this instance. */1539 public TestDifference(org.jmlspecs.models.JMLValueSet receiver$, org.jmlspecs.models.JMLValueSet s2) {1540 super("difference"+ ":" + (s2==null? "null" :"{org.jmlspecs.models.JMLValueSet}"));1541 this.receiver$ = receiver$;1542 this.s2 = s2;1543 }1544 protected void doCall() throws java.lang.Throwable {1545 receiver$.difference(s2);1546 }1547 protected java.lang.String failMessage1548 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1549 {1550 java.lang.String msg = "\n\tMethod 'difference' applied to";1551 msg += "\n\tReceiver: " + this.receiver$;1552 msg += "\n\tArgument s2: " + this.s2;1553 return msg;1554 }1555 }1556 /** Add tests for the powerSet method1557 * to the overall test suite. */1558 private void addTestSuiteFor$TestPowerSet1559 (junit.framework.TestSuite overallTestSuite$)1560 {1561 junit.framework.TestSuite methodTests$1562 = this.emptyTestSuiteFor("powerSet");1563 try {1564 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1565 receivers$iter1566 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1567 (this.vorg_jmlspecs_models_JMLValueSetIter("powerSet", 0));1568 this.check_has_data1569 (receivers$iter,1570 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"powerSet\", 0))");1571 while (!receivers$iter.atEnd()) {1572 final org.jmlspecs.models.JMLValueSet receiver$1573 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1574 methodTests$.addTest1575 (new TestPowerSet(receiver$));1576 receivers$iter.advance();1577 }1578 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1579 // methodTests$ doesn't want more tests1580 }1581 overallTestSuite$.addTest(methodTests$);1582 }1583 /** Test for the powerSet method. */1584 protected static class TestPowerSet extends OneTest {1585 /** The receiver */1586 private org.jmlspecs.models.JMLValueSet receiver$;1587 /** Initialize this instance. */1588 public TestPowerSet(org.jmlspecs.models.JMLValueSet receiver$) {1589 super("powerSet");1590 this.receiver$ = receiver$;1591 }1592 protected void doCall() throws java.lang.Throwable {1593 receiver$.powerSet();1594 }1595 protected java.lang.String failMessage1596 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1597 {1598 java.lang.String msg = "\n\tMethod 'powerSet' applied to";1599 msg += "\n\tReceiver: " + this.receiver$;1600 return msg;1601 }1602 }1603 /** Add tests for the toBag method1604 * to the overall test suite. */1605 private void addTestSuiteFor$TestToBag1606 (junit.framework.TestSuite overallTestSuite$)1607 {1608 junit.framework.TestSuite methodTests$1609 = this.emptyTestSuiteFor("toBag");1610 try {1611 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1612 receivers$iter1613 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1614 (this.vorg_jmlspecs_models_JMLValueSetIter("toBag", 0));1615 this.check_has_data1616 (receivers$iter,1617 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"toBag\", 0))");1618 while (!receivers$iter.atEnd()) {1619 final org.jmlspecs.models.JMLValueSet receiver$1620 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1621 methodTests$.addTest1622 (new TestToBag(receiver$));1623 receivers$iter.advance();1624 }1625 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1626 // methodTests$ doesn't want more tests1627 }1628 overallTestSuite$.addTest(methodTests$);1629 }1630 /** Test for the toBag method. */1631 protected static class TestToBag extends OneTest {1632 /** The receiver */1633 private org.jmlspecs.models.JMLValueSet receiver$;1634 /** Initialize this instance. */1635 public TestToBag(org.jmlspecs.models.JMLValueSet receiver$) {1636 super("toBag");1637 this.receiver$ = receiver$;1638 }1639 protected void doCall() throws java.lang.Throwable {1640 receiver$.toBag();1641 }1642 protected java.lang.String failMessage1643 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1644 {1645 java.lang.String msg = "\n\tMethod 'toBag' applied to";1646 msg += "\n\tReceiver: " + this.receiver$;1647 return msg;1648 }1649 }1650 /** Add tests for the toSequence method1651 * to the overall test suite. */1652 private void addTestSuiteFor$TestToSequence1653 (junit.framework.TestSuite overallTestSuite$)1654 {1655 junit.framework.TestSuite methodTests$1656 = this.emptyTestSuiteFor("toSequence");1657 try {1658 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1659 receivers$iter1660 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1661 (this.vorg_jmlspecs_models_JMLValueSetIter("toSequence", 0));1662 this.check_has_data1663 (receivers$iter,1664 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"toSequence\", 0))");1665 while (!receivers$iter.atEnd()) {1666 final org.jmlspecs.models.JMLValueSet receiver$1667 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1668 methodTests$.addTest1669 (new TestToSequence(receiver$));1670 receivers$iter.advance();1671 }1672 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1673 // methodTests$ doesn't want more tests1674 }1675 overallTestSuite$.addTest(methodTests$);1676 }1677 /** Test for the toSequence method. */1678 protected static class TestToSequence extends OneTest {1679 /** The receiver */1680 private org.jmlspecs.models.JMLValueSet receiver$;1681 /** Initialize this instance. */1682 public TestToSequence(org.jmlspecs.models.JMLValueSet receiver$) {1683 super("toSequence");1684 this.receiver$ = receiver$;1685 }1686 protected void doCall() throws java.lang.Throwable {1687 receiver$.toSequence();1688 }1689 protected java.lang.String failMessage1690 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1691 {1692 java.lang.String msg = "\n\tMethod 'toSequence' applied to";1693 msg += "\n\tReceiver: " + this.receiver$;1694 return msg;1695 }1696 }1697 /** Add tests for the toArray method1698 * to the overall test suite. */1699 private void addTestSuiteFor$TestToArray1700 (junit.framework.TestSuite overallTestSuite$)1701 {1702 junit.framework.TestSuite methodTests$1703 = this.emptyTestSuiteFor("toArray");1704 try {1705 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1706 receivers$iter1707 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1708 (this.vorg_jmlspecs_models_JMLValueSetIter("toArray", 0));1709 this.check_has_data1710 (receivers$iter,1711 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"toArray\", 0))");1712 while (!receivers$iter.atEnd()) {1713 final org.jmlspecs.models.JMLValueSet receiver$1714 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1715 methodTests$.addTest1716 (new TestToArray(receiver$));1717 receivers$iter.advance();1718 }1719 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1720 // methodTests$ doesn't want more tests1721 }1722 overallTestSuite$.addTest(methodTests$);1723 }1724 /** Test for the toArray method. */1725 protected static class TestToArray extends OneTest {1726 /** The receiver */1727 private org.jmlspecs.models.JMLValueSet receiver$;1728 /** Initialize this instance. */1729 public TestToArray(org.jmlspecs.models.JMLValueSet receiver$) {1730 super("toArray");1731 this.receiver$ = receiver$;1732 }1733 protected void doCall() throws java.lang.Throwable {1734 receiver$.toArray();1735 }1736 protected java.lang.String failMessage1737 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1738 {1739 java.lang.String msg = "\n\tMethod 'toArray' applied to";1740 msg += "\n\tReceiver: " + this.receiver$;1741 return msg;1742 }1743 }1744 /** Add tests for the elements method1745 * to the overall test suite. */1746 private void addTestSuiteFor$TestElements1747 (junit.framework.TestSuite overallTestSuite$)1748 {1749 junit.framework.TestSuite methodTests$1750 = this.emptyTestSuiteFor("elements");1751 try {1752 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1753 receivers$iter1754 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1755 (this.vorg_jmlspecs_models_JMLValueSetIter("elements", 0));1756 this.check_has_data1757 (receivers$iter,1758 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"elements\", 0))");1759 while (!receivers$iter.atEnd()) {1760 final org.jmlspecs.models.JMLValueSet receiver$1761 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1762 methodTests$.addTest1763 (new TestElements(receiver$));1764 receivers$iter.advance();1765 }1766 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1767 // methodTests$ doesn't want more tests1768 }1769 overallTestSuite$.addTest(methodTests$);1770 }1771 /** Test for the elements method. */1772 protected static class TestElements extends OneTest {1773 /** The receiver */1774 private org.jmlspecs.models.JMLValueSet receiver$;1775 /** Initialize this instance. */1776 public TestElements(org.jmlspecs.models.JMLValueSet receiver$) {1777 super("elements");1778 this.receiver$ = receiver$;1779 }1780 protected void doCall() throws java.lang.Throwable {1781 receiver$.elements();1782 }1783 protected java.lang.String failMessage1784 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1785 {1786 java.lang.String msg = "\n\tMethod 'elements' applied to";1787 msg += "\n\tReceiver: " + this.receiver$;1788 return msg;1789 }1790 }1791 /** Add tests for the iterator method1792 * to the overall test suite. */1793 private void addTestSuiteFor$TestIterator1794 (junit.framework.TestSuite overallTestSuite$)1795 {1796 junit.framework.TestSuite methodTests$1797 = this.emptyTestSuiteFor("iterator");1798 try {1799 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1800 receivers$iter1801 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1802 (this.vorg_jmlspecs_models_JMLValueSetIter("iterator", 0));1803 this.check_has_data1804 (receivers$iter,1805 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"iterator\", 0))");1806 while (!receivers$iter.atEnd()) {1807 final org.jmlspecs.models.JMLValueSet receiver$1808 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1809 methodTests$.addTest1810 (new TestIterator(receiver$));1811 receivers$iter.advance();1812 }1813 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1814 // methodTests$ doesn't want more tests1815 }1816 overallTestSuite$.addTest(methodTests$);1817 }1818 /** Test for the iterator method. */1819 protected static class TestIterator extends OneTest {1820 /** The receiver */1821 private org.jmlspecs.models.JMLValueSet receiver$;1822 /** Initialize this instance. */1823 public TestIterator(org.jmlspecs.models.JMLValueSet receiver$) {1824 super("iterator");1825 this.receiver$ = receiver$;1826 }1827 protected void doCall() throws java.lang.Throwable {1828 receiver$.iterator();1829 }1830 protected java.lang.String failMessage1831 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1832 {1833 java.lang.String msg = "\n\tMethod 'iterator' applied to";1834 msg += "\n\tReceiver: " + this.receiver$;1835 return msg;1836 }1837 }1838 /** Add tests for the toString method1839 * to the overall test suite. */1840 private void addTestSuiteFor$TestToString1841 (junit.framework.TestSuite overallTestSuite$)1842 {1843 junit.framework.TestSuite methodTests$1844 = this.emptyTestSuiteFor("toString");1845 try {1846 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1847 receivers$iter1848 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1849 (this.vorg_jmlspecs_models_JMLValueSetIter("toString", 0));1850 this.check_has_data1851 (receivers$iter,1852 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"toString\", 0))");1853 while (!receivers$iter.atEnd()) {1854 final org.jmlspecs.models.JMLValueSet receiver$1855 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1856 methodTests$.addTest1857 (new TestToString(receiver$));1858 receivers$iter.advance();1859 }1860 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1861 // methodTests$ doesn't want more tests1862 }1863 overallTestSuite$.addTest(methodTests$);1864 }1865 /** Test for the toString method. */1866 protected static class TestToString extends OneTest {1867 /** The receiver */1868 private org.jmlspecs.models.JMLValueSet receiver$;1869 /** Initialize this instance. */1870 public TestToString(org.jmlspecs.models.JMLValueSet receiver$) {1871 super("toString");1872 this.receiver$ = receiver$;1873 }1874 protected void doCall() throws java.lang.Throwable {1875 receiver$.toString();1876 }1877 protected java.lang.String failMessage1878 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1879 {1880 java.lang.String msg = "\n\tMethod 'toString' applied to";1881 msg += "\n\tReceiver: " + this.receiver$;1882 return msg;1883 }1884 }1885 /** Add tests for the has method1886 * to the overall test suite. */1887 private void addTestSuiteFor$TestHas$11888 (junit.framework.TestSuite overallTestSuite$)1889 {1890 junit.framework.TestSuite methodTests$1891 = this.emptyTestSuiteFor("has");1892 try {1893 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1894 receivers$iter1895 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1896 (this.vorg_jmlspecs_models_JMLValueSetIter("has", 1));1897 this.check_has_data1898 (receivers$iter,1899 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueSetIter(\"has\", 1))");1900 while (!receivers$iter.atEnd()) {1901 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1902 vjava_lang_Object$1$iter1903 = this.vjava_lang_ObjectIter("has", 0);1904 this.check_has_data1905 (vjava_lang_Object$1$iter,1906 "this.vjava_lang_ObjectIter(\"has\", 0)");1907 while (!vjava_lang_Object$1$iter.atEnd()) {1908 final org.jmlspecs.models.JMLValueSet receiver$1909 = (org.jmlspecs.models.JMLValueSet) receivers$iter.get();1910 final java.lang.Object arg11911 = (java.lang.Object) vjava_lang_Object$1$iter.get();1912 methodTests$.addTest1913 (new TestHas$1(receiver$, arg1));1914 vjava_lang_Object$1$iter.advance();1915 }1916 receivers$iter.advance();1917 }1918 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1919 // methodTests$ doesn't want more tests1920 }1921 overallTestSuite$.addTest(methodTests$);1922 }1923 /** Test for the has method. */1924 protected static class TestHas$1 extends OneTest {1925 /** The receiver */1926 private org.jmlspecs.models.JMLValueSet receiver$;1927 /** Argument arg1 */1928 private java.lang.Object arg1;1929 /** Initialize this instance. */1930 public TestHas$1(org.jmlspecs.models.JMLValueSet receiver$, java.lang.Object arg1) {1931 super("has"+ ":" + (arg1==null? "null" :"{java.lang.Object}"));1932 this.receiver$ = receiver$;1933 this.arg1 = arg1;...

Full Screen

Full Screen

Source:JMLInteger_JML_Test.java Github

copy

Full Screen

...15 /** Initialize this class. */16 public JMLInteger_JML_Test(java.lang.String name) {17 super(name);18 }19 /** Run the tests. */20 public static void main(java.lang.String[] args) {21 org.jmlspecs.jmlunit.JMLTestRunner.run(suite());22 // You can also use a JUnit test runner such as:23 // junit.textui.TestRunner.run(suite());24 }25 /** Test to see if the code for class JMLInteger26 * has been compiled with runtime assertion checking (i.e., by jmlc).27 * Code that is not compiled with jmlc would not make an effective test,28 * since no assertion checking would be done. */29 public void test$IsRACCompiled() {30 junit.framework.Assert.assertTrue("code for class JMLInteger"31 + " was not compiled with jmlc"32 + " so no assertions will be checked!",33 org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLInteger.class)34 );35 }36 /** Return the test suite for this test class. This will have37 * added to it at least test$IsRACCompiled(), and any test methods38 * written explicitly by the user in the superclass. It will also39 * have added test suites for each testing each method and40 * constructor.41 */42 //@ ensures \result != null;43 public static junit.framework.Test suite() {44 JMLInteger_JML_Test testobj45 = new JMLInteger_JML_Test("JMLInteger_JML_Test");46 junit.framework.TestSuite testsuite = testobj.overallTestSuite();47 // Add instances of Test found by the reflection mechanism.48 testsuite.addTestSuite(JMLInteger_JML_Test.class);49 testobj.addTestSuiteForEachMethod(testsuite);50 return testsuite;51 }52 /** A JUnit test object that can run a single test method. This53 * is defined as a nested class solely for convenience; it can't54 * be defined once and for all because it must subclass its55 * enclosing class.56 */57 protected static abstract class OneTest extends JMLInteger_JML_Test {58 /** Initialize this test object. */59 public OneTest(String name) {60 super(name);61 }62 /** The result object that holds information about testing. */63 protected junit.framework.TestResult result;64 //@ also65 //@ requires result != null;66 public void run(junit.framework.TestResult result) {67 this.result = result;68 super.run(result);69 }70 /* Run a single test and decide whether the test was71 * successful, meaningless, or a failure. This is the72 * Template Method pattern abstraction of the inner loop in a73 * JML/JUnit test. */74 public void runTest() throws java.lang.Throwable {75 try {76 // The call being tested!77 doCall();78 }79 catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) {80 // meaningless test input81 addMeaningless();82 } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) {83 // test failure84 int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel();85 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel86 (org.jmlspecs.jmlrac.runtime.JMLOption.NONE);87 try {88 java.lang.String failmsg = this.failMessage(e);89 junit.framework.AssertionFailedError err90 = new junit.framework.AssertionFailedError(failmsg);91 err.setStackTrace(new java.lang.StackTraceElement[]{});92 err.initCause(e);93 result.addFailure(this, err);94 } finally {95 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l);96 }97 } catch (java.lang.Throwable e) {98 // test success99 }100 }101 /** Call the method to be tested with the appropriate arguments. */102 protected abstract void doCall() throws java.lang.Throwable;103 /** Format the error message for a test failure, based on the104 * method's arguments. */105 protected abstract java.lang.String failMessage106 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e);107 /** Inform listeners that a meaningless test was run. */108 private void addMeaningless() {109 if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) {110 ((org.jmlspecs.jmlunit.JMLTestResult)result)111 .addMeaningless(this);112 }113 }114 }115 /** Create the tests that are to be run for testing the class116 * JMLInteger. The framework will then run them.117 * @param overallTestSuite$ The suite accumulating all of the tests118 * for this driver class.119 */120 //@ requires overallTestSuite$ != null;121 public void addTestSuiteForEachMethod122 (junit.framework.TestSuite overallTestSuite$)123 {124 try {125 this.addTestSuiteFor$TestJMLInteger(overallTestSuite$);126 } catch (java.lang.Throwable ex) {127 overallTestSuite$.addTest128 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));129 }130 try {131 this.addTestSuiteFor$TestJMLInteger$1(overallTestSuite$);132 } catch (java.lang.Throwable ex) {133 overallTestSuite$.addTest134 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));135 }136 try {137 this.addTestSuiteFor$TestJMLInteger$2(overallTestSuite$);138 } catch (java.lang.Throwable ex) {139 overallTestSuite$.addTest140 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));141 }142 try {143 this.addTestSuiteFor$TestJMLInteger$3(overallTestSuite$);144 } catch (java.lang.Throwable ex) {145 overallTestSuite$.addTest146 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));147 }148 try {149 this.addTestSuiteFor$TestClone(overallTestSuite$);150 } catch (java.lang.Throwable ex) {151 overallTestSuite$.addTest152 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));153 }154 try {155 this.addTestSuiteFor$TestCompareTo(overallTestSuite$);156 } catch (java.lang.Throwable ex) {157 overallTestSuite$.addTest158 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));159 }160 try {161 this.addTestSuiteFor$TestEquals(overallTestSuite$);162 } catch (java.lang.Throwable ex) {163 overallTestSuite$.addTest164 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));165 }166 try {167 this.addTestSuiteFor$TestHashCode(overallTestSuite$);168 } catch (java.lang.Throwable ex) {169 overallTestSuite$.addTest170 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));171 }172 try {173 this.addTestSuiteFor$TestIntValue(overallTestSuite$);174 } catch (java.lang.Throwable ex) {175 overallTestSuite$.addTest176 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));177 }178 try {179 this.addTestSuiteFor$TestGetInteger(overallTestSuite$);180 } catch (java.lang.Throwable ex) {181 overallTestSuite$.addTest182 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));183 }184 try {185 this.addTestSuiteFor$TestNegated(overallTestSuite$);186 } catch (java.lang.Throwable ex) {187 overallTestSuite$.addTest188 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));189 }190 try {191 this.addTestSuiteFor$TestPlus(overallTestSuite$);192 } catch (java.lang.Throwable ex) {193 overallTestSuite$.addTest194 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));195 }196 try {197 this.addTestSuiteFor$TestMinus(overallTestSuite$);198 } catch (java.lang.Throwable ex) {199 overallTestSuite$.addTest200 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));201 }202 try {203 this.addTestSuiteFor$TestTimes(overallTestSuite$);204 } catch (java.lang.Throwable ex) {205 overallTestSuite$.addTest206 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));207 }208 try {209 this.addTestSuiteFor$TestDividedBy(overallTestSuite$);210 } catch (java.lang.Throwable ex) {211 overallTestSuite$.addTest212 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));213 }214 try {215 this.addTestSuiteFor$TestRemainderBy(overallTestSuite$);216 } catch (java.lang.Throwable ex) {217 overallTestSuite$.addTest218 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));219 }220 try {221 this.addTestSuiteFor$TestGreaterThan(overallTestSuite$);222 } catch (java.lang.Throwable ex) {223 overallTestSuite$.addTest224 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));225 }226 try {227 this.addTestSuiteFor$TestLessThan(overallTestSuite$);228 } catch (java.lang.Throwable ex) {229 overallTestSuite$.addTest230 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));231 }232 try {233 this.addTestSuiteFor$TestGreaterThanOrEqualTo(overallTestSuite$);234 } catch (java.lang.Throwable ex) {235 overallTestSuite$.addTest236 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));237 }238 try {239 this.addTestSuiteFor$TestLessThanOrEqualTo(overallTestSuite$);240 } catch (java.lang.Throwable ex) {241 overallTestSuite$.addTest242 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));243 }244 try {245 this.addTestSuiteFor$TestToString(overallTestSuite$);246 } catch (java.lang.Throwable ex) {247 overallTestSuite$.addTest248 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));249 }250 }251 /** Add tests for the JMLInteger contructor252 * to the overall test suite. */253 private void addTestSuiteFor$TestJMLInteger254 (junit.framework.TestSuite overallTestSuite$)255 {256 junit.framework.TestSuite methodTests$257 = this.emptyTestSuiteFor("JMLInteger");258 try {259 methodTests$.addTest260 (new TestJMLInteger());261 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {262 // methodTests$ doesn't want more tests263 }264 overallTestSuite$.addTest(methodTests$);265 }266 /** Test for the JMLInteger contructor. */267 protected static class TestJMLInteger extends OneTest {268 /** Initialize this instance. */269 public TestJMLInteger() {270 super("JMLInteger");271 }272 protected void doCall() throws java.lang.Throwable {273 new JMLInteger();274 }275 protected java.lang.String failMessage276 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)277 {278 java.lang.String msg = "\n\tContructor 'JMLInteger'";279 return msg;280 }281 }282 /** Add tests for the JMLInteger contructor283 * to the overall test suite. */284 private void addTestSuiteFor$TestJMLInteger$1285 (junit.framework.TestSuite overallTestSuite$)286 {287 junit.framework.TestSuite methodTests$288 = this.emptyTestSuiteFor("JMLInteger");289 try {290 org.jmlspecs.jmlunit.strategies.IntIterator291 vint$1$iter292 = this.vintIter("JMLInteger", 0);293 this.check_has_data294 (vint$1$iter,295 "this.vintIter(\"JMLInteger\", 0)");296 while (!vint$1$iter.atEnd()) {297 final int inInt298 = vint$1$iter.getInt();299 methodTests$.addTest300 (new TestJMLInteger$1(inInt));301 vint$1$iter.advance();302 }303 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {304 // methodTests$ doesn't want more tests305 }306 overallTestSuite$.addTest(methodTests$);307 }308 /** Test for the JMLInteger contructor. */309 protected static class TestJMLInteger$1 extends OneTest {310 /** Argument inInt */311 private int inInt;312 /** Initialize this instance. */313 public TestJMLInteger$1(int inInt) {314 super("JMLInteger"+ ":" + inInt);315 this.inInt = inInt;316 }317 protected void doCall() throws java.lang.Throwable {318 new JMLInteger(inInt);319 }320 protected java.lang.String failMessage321 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)322 {323 java.lang.String msg = "\n\tContructor 'JMLInteger' applied to";324 msg += "\n\tArgument inInt: " + this.inInt;325 return msg;326 }327 }328 /** Add tests for the JMLInteger contructor329 * to the overall test suite. */330 private void addTestSuiteFor$TestJMLInteger$2331 (junit.framework.TestSuite overallTestSuite$)332 {333 junit.framework.TestSuite methodTests$334 = this.emptyTestSuiteFor("JMLInteger");335 try {336 org.jmlspecs.jmlunit.strategies.IndefiniteIterator337 vjava_lang_Integer$1$iter338 = this.vjava_lang_IntegerIter("JMLInteger", 0);339 this.check_has_data340 (vjava_lang_Integer$1$iter,341 "this.vjava_lang_IntegerIter(\"JMLInteger\", 0)");342 while (!vjava_lang_Integer$1$iter.atEnd()) {343 final java.lang.Integer inInteger344 = (java.lang.Integer) vjava_lang_Integer$1$iter.get();345 methodTests$.addTest346 (new TestJMLInteger$2(inInteger));347 vjava_lang_Integer$1$iter.advance();348 }349 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {350 // methodTests$ doesn't want more tests351 }352 overallTestSuite$.addTest(methodTests$);353 }354 /** Test for the JMLInteger contructor. */355 protected static class TestJMLInteger$2 extends OneTest {356 /** Argument inInteger */357 private java.lang.Integer inInteger;358 /** Initialize this instance. */359 public TestJMLInteger$2(java.lang.Integer inInteger) {360 super("JMLInteger"+ ":" + (inInteger==null? "null" :"{java.lang.Integer}"));361 this.inInteger = inInteger;362 }363 protected void doCall() throws java.lang.Throwable {364 new JMLInteger(inInteger);365 }366 protected java.lang.String failMessage367 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)368 {369 java.lang.String msg = "\n\tContructor 'JMLInteger' applied to";370 msg += "\n\tArgument inInteger: " + this.inInteger;371 return msg;372 }373 }374 /** Add tests for the JMLInteger contructor375 * to the overall test suite. */376 private void addTestSuiteFor$TestJMLInteger$3377 (junit.framework.TestSuite overallTestSuite$)378 {379 junit.framework.TestSuite methodTests$380 = this.emptyTestSuiteFor("JMLInteger");381 try {382 org.jmlspecs.jmlunit.strategies.IndefiniteIterator383 vjava_lang_String$1$iter384 = this.vjava_lang_StringIter("JMLInteger", 0);385 this.check_has_data386 (vjava_lang_String$1$iter,387 "this.vjava_lang_StringIter(\"JMLInteger\", 0)");388 while (!vjava_lang_String$1$iter.atEnd()) {389 final java.lang.String s390 = (java.lang.String) vjava_lang_String$1$iter.get();391 methodTests$.addTest392 (new TestJMLInteger$3(s));393 vjava_lang_String$1$iter.advance();394 }395 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {396 // methodTests$ doesn't want more tests397 }398 overallTestSuite$.addTest(methodTests$);399 }400 /** Test for the JMLInteger contructor. */401 protected static class TestJMLInteger$3 extends OneTest {402 /** Argument s */403 private java.lang.String s;404 /** Initialize this instance. */405 public TestJMLInteger$3(java.lang.String s) {406 super("JMLInteger"+ ":" + (s==null? "null" :("\""+s+"\"")));407 this.s = s;408 }409 protected void doCall() throws java.lang.Throwable {410 new JMLInteger(s);411 }412 protected java.lang.String failMessage413 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)414 {415 java.lang.String msg = "\n\tContructor 'JMLInteger' applied to";416 msg += "\n\tArgument s: " + this.s;417 return msg;418 }419 }420 /** Add tests for the clone method421 * to the overall test suite. */422 private void addTestSuiteFor$TestClone423 (junit.framework.TestSuite overallTestSuite$)424 {425 junit.framework.TestSuite methodTests$426 = this.emptyTestSuiteFor("clone");427 try {428 org.jmlspecs.jmlunit.strategies.IndefiniteIterator429 receivers$iter430 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator431 (this.vorg_jmlspecs_models_JMLIntegerIter("clone", 0));432 this.check_has_data433 (receivers$iter,434 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"clone\", 0))");435 while (!receivers$iter.atEnd()) {436 final org.jmlspecs.models.JMLInteger receiver$437 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();438 methodTests$.addTest439 (new TestClone(receiver$));440 receivers$iter.advance();441 }442 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {443 // methodTests$ doesn't want more tests444 }445 overallTestSuite$.addTest(methodTests$);446 }447 /** Test for the clone method. */448 protected static class TestClone extends OneTest {449 /** The receiver */450 private org.jmlspecs.models.JMLInteger receiver$;451 /** Initialize this instance. */452 public TestClone(org.jmlspecs.models.JMLInteger receiver$) {453 super("clone");454 this.receiver$ = receiver$;455 }456 protected void doCall() throws java.lang.Throwable {457 receiver$.clone();458 }459 protected java.lang.String failMessage460 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)461 {462 java.lang.String msg = "\n\tMethod 'clone' applied to";463 msg += "\n\tReceiver: " + this.receiver$;464 return msg;465 }466 }467 /** Add tests for the compareTo method468 * to the overall test suite. */469 private void addTestSuiteFor$TestCompareTo470 (junit.framework.TestSuite overallTestSuite$)471 {472 junit.framework.TestSuite methodTests$473 = this.emptyTestSuiteFor("compareTo");474 try {475 org.jmlspecs.jmlunit.strategies.IndefiniteIterator476 receivers$iter477 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator478 (this.vorg_jmlspecs_models_JMLIntegerIter("compareTo", 1));479 this.check_has_data480 (receivers$iter,481 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"compareTo\", 1))");482 while (!receivers$iter.atEnd()) {483 org.jmlspecs.jmlunit.strategies.IndefiniteIterator484 vjava_lang_Object$1$iter485 = this.vjava_lang_ObjectIter("compareTo", 0);486 this.check_has_data487 (vjava_lang_Object$1$iter,488 "this.vjava_lang_ObjectIter(\"compareTo\", 0)");489 while (!vjava_lang_Object$1$iter.atEnd()) {490 final org.jmlspecs.models.JMLInteger receiver$491 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();492 final java.lang.Object op2493 = (java.lang.Object) vjava_lang_Object$1$iter.get();494 methodTests$.addTest495 (new TestCompareTo(receiver$, op2));496 vjava_lang_Object$1$iter.advance();497 }498 receivers$iter.advance();499 }500 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {501 // methodTests$ doesn't want more tests502 }503 overallTestSuite$.addTest(methodTests$);504 }505 /** Test for the compareTo method. */506 protected static class TestCompareTo extends OneTest {507 /** The receiver */508 private org.jmlspecs.models.JMLInteger receiver$;509 /** Argument op2 */510 private java.lang.Object op2;511 /** Initialize this instance. */512 public TestCompareTo(org.jmlspecs.models.JMLInteger receiver$, java.lang.Object op2) {513 super("compareTo"+ ":" + (op2==null? "null" :"{java.lang.Object}"));514 this.receiver$ = receiver$;515 this.op2 = op2;516 }517 protected void doCall() throws java.lang.Throwable {518 receiver$.compareTo(op2);519 }520 protected java.lang.String failMessage521 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)522 {523 java.lang.String msg = "\n\tMethod 'compareTo' applied to";524 msg += "\n\tReceiver: " + this.receiver$;525 msg += "\n\tArgument op2: " + this.op2;526 return msg;527 }528 }529 /** Add tests for the equals method530 * to the overall test suite. */531 private void addTestSuiteFor$TestEquals532 (junit.framework.TestSuite overallTestSuite$)533 {534 junit.framework.TestSuite methodTests$535 = this.emptyTestSuiteFor("equals");536 try {537 org.jmlspecs.jmlunit.strategies.IndefiniteIterator538 receivers$iter539 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator540 (this.vorg_jmlspecs_models_JMLIntegerIter("equals", 1));541 this.check_has_data542 (receivers$iter,543 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"equals\", 1))");544 while (!receivers$iter.atEnd()) {545 org.jmlspecs.jmlunit.strategies.IndefiniteIterator546 vjava_lang_Object$1$iter547 = this.vjava_lang_ObjectIter("equals", 0);548 this.check_has_data549 (vjava_lang_Object$1$iter,550 "this.vjava_lang_ObjectIter(\"equals\", 0)");551 while (!vjava_lang_Object$1$iter.atEnd()) {552 final org.jmlspecs.models.JMLInteger receiver$553 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();554 final java.lang.Object op2555 = (java.lang.Object) vjava_lang_Object$1$iter.get();556 methodTests$.addTest557 (new TestEquals(receiver$, op2));558 vjava_lang_Object$1$iter.advance();559 }560 receivers$iter.advance();561 }562 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {563 // methodTests$ doesn't want more tests564 }565 overallTestSuite$.addTest(methodTests$);566 }567 /** Test for the equals method. */568 protected static class TestEquals extends OneTest {569 /** The receiver */570 private org.jmlspecs.models.JMLInteger receiver$;571 /** Argument op2 */572 private java.lang.Object op2;573 /** Initialize this instance. */574 public TestEquals(org.jmlspecs.models.JMLInteger receiver$, java.lang.Object op2) {575 super("equals"+ ":" + (op2==null? "null" :"{java.lang.Object}"));576 this.receiver$ = receiver$;577 this.op2 = op2;578 }579 protected void doCall() throws java.lang.Throwable {580 receiver$.equals(op2);581 }582 protected java.lang.String failMessage583 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)584 {585 java.lang.String msg = "\n\tMethod 'equals' applied to";586 msg += "\n\tReceiver: " + this.receiver$;587 msg += "\n\tArgument op2: " + this.op2;588 return msg;589 }590 }591 /** Add tests for the hashCode method592 * to the overall test suite. */593 private void addTestSuiteFor$TestHashCode594 (junit.framework.TestSuite overallTestSuite$)595 {596 junit.framework.TestSuite methodTests$597 = this.emptyTestSuiteFor("hashCode");598 try {599 org.jmlspecs.jmlunit.strategies.IndefiniteIterator600 receivers$iter601 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator602 (this.vorg_jmlspecs_models_JMLIntegerIter("hashCode", 0));603 this.check_has_data604 (receivers$iter,605 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"hashCode\", 0))");606 while (!receivers$iter.atEnd()) {607 final org.jmlspecs.models.JMLInteger receiver$608 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();609 methodTests$.addTest610 (new TestHashCode(receiver$));611 receivers$iter.advance();612 }613 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {614 // methodTests$ doesn't want more tests615 }616 overallTestSuite$.addTest(methodTests$);617 }618 /** Test for the hashCode method. */619 protected static class TestHashCode extends OneTest {620 /** The receiver */621 private org.jmlspecs.models.JMLInteger receiver$;622 /** Initialize this instance. */623 public TestHashCode(org.jmlspecs.models.JMLInteger receiver$) {624 super("hashCode");625 this.receiver$ = receiver$;626 }627 protected void doCall() throws java.lang.Throwable {628 receiver$.hashCode();629 }630 protected java.lang.String failMessage631 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)632 {633 java.lang.String msg = "\n\tMethod 'hashCode' applied to";634 msg += "\n\tReceiver: " + this.receiver$;635 return msg;636 }637 }638 /** Add tests for the intValue method639 * to the overall test suite. */640 private void addTestSuiteFor$TestIntValue641 (junit.framework.TestSuite overallTestSuite$)642 {643 junit.framework.TestSuite methodTests$644 = this.emptyTestSuiteFor("intValue");645 try {646 org.jmlspecs.jmlunit.strategies.IndefiniteIterator647 receivers$iter648 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator649 (this.vorg_jmlspecs_models_JMLIntegerIter("intValue", 0));650 this.check_has_data651 (receivers$iter,652 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"intValue\", 0))");653 while (!receivers$iter.atEnd()) {654 final org.jmlspecs.models.JMLInteger receiver$655 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();656 methodTests$.addTest657 (new TestIntValue(receiver$));658 receivers$iter.advance();659 }660 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {661 // methodTests$ doesn't want more tests662 }663 overallTestSuite$.addTest(methodTests$);664 }665 /** Test for the intValue method. */666 protected static class TestIntValue extends OneTest {667 /** The receiver */668 private org.jmlspecs.models.JMLInteger receiver$;669 /** Initialize this instance. */670 public TestIntValue(org.jmlspecs.models.JMLInteger receiver$) {671 super("intValue");672 this.receiver$ = receiver$;673 }674 protected void doCall() throws java.lang.Throwable {675 receiver$.intValue();676 }677 protected java.lang.String failMessage678 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)679 {680 java.lang.String msg = "\n\tMethod 'intValue' applied to";681 msg += "\n\tReceiver: " + this.receiver$;682 return msg;683 }684 }685 /** Add tests for the getInteger method686 * to the overall test suite. */687 private void addTestSuiteFor$TestGetInteger688 (junit.framework.TestSuite overallTestSuite$)689 {690 junit.framework.TestSuite methodTests$691 = this.emptyTestSuiteFor("getInteger");692 try {693 org.jmlspecs.jmlunit.strategies.IndefiniteIterator694 receivers$iter695 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator696 (this.vorg_jmlspecs_models_JMLIntegerIter("getInteger", 0));697 this.check_has_data698 (receivers$iter,699 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"getInteger\", 0))");700 while (!receivers$iter.atEnd()) {701 final org.jmlspecs.models.JMLInteger receiver$702 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();703 methodTests$.addTest704 (new TestGetInteger(receiver$));705 receivers$iter.advance();706 }707 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {708 // methodTests$ doesn't want more tests709 }710 overallTestSuite$.addTest(methodTests$);711 }712 /** Test for the getInteger method. */713 protected static class TestGetInteger extends OneTest {714 /** The receiver */715 private org.jmlspecs.models.JMLInteger receiver$;716 /** Initialize this instance. */717 public TestGetInteger(org.jmlspecs.models.JMLInteger receiver$) {718 super("getInteger");719 this.receiver$ = receiver$;720 }721 protected void doCall() throws java.lang.Throwable {722 receiver$.getInteger();723 }724 protected java.lang.String failMessage725 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)726 {727 java.lang.String msg = "\n\tMethod 'getInteger' applied to";728 msg += "\n\tReceiver: " + this.receiver$;729 return msg;730 }731 }732 /** Add tests for the negated method733 * to the overall test suite. */734 private void addTestSuiteFor$TestNegated735 (junit.framework.TestSuite overallTestSuite$)736 {737 junit.framework.TestSuite methodTests$738 = this.emptyTestSuiteFor("negated");739 try {740 org.jmlspecs.jmlunit.strategies.IndefiniteIterator741 receivers$iter742 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator743 (this.vorg_jmlspecs_models_JMLIntegerIter("negated", 0));744 this.check_has_data745 (receivers$iter,746 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"negated\", 0))");747 while (!receivers$iter.atEnd()) {748 final org.jmlspecs.models.JMLInteger receiver$749 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();750 methodTests$.addTest751 (new TestNegated(receiver$));752 receivers$iter.advance();753 }754 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {755 // methodTests$ doesn't want more tests756 }757 overallTestSuite$.addTest(methodTests$);758 }759 /** Test for the negated method. */760 protected static class TestNegated extends OneTest {761 /** The receiver */762 private org.jmlspecs.models.JMLInteger receiver$;763 /** Initialize this instance. */764 public TestNegated(org.jmlspecs.models.JMLInteger receiver$) {765 super("negated");766 this.receiver$ = receiver$;767 }768 protected void doCall() throws java.lang.Throwable {769 receiver$.negated();770 }771 protected java.lang.String failMessage772 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)773 {774 java.lang.String msg = "\n\tMethod 'negated' applied to";775 msg += "\n\tReceiver: " + this.receiver$;776 return msg;777 }778 }779 /** Add tests for the plus method780 * to the overall test suite. */781 private void addTestSuiteFor$TestPlus782 (junit.framework.TestSuite overallTestSuite$)783 {784 junit.framework.TestSuite methodTests$785 = this.emptyTestSuiteFor("plus");786 try {787 org.jmlspecs.jmlunit.strategies.IndefiniteIterator788 receivers$iter789 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator790 (this.vorg_jmlspecs_models_JMLIntegerIter("plus", 1));791 this.check_has_data792 (receivers$iter,793 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"plus\", 1))");794 while (!receivers$iter.atEnd()) {795 org.jmlspecs.jmlunit.strategies.IndefiniteIterator796 vorg_jmlspecs_models_JMLInteger$1$iter797 = this.vorg_jmlspecs_models_JMLIntegerIter("plus", 0);798 this.check_has_data799 (vorg_jmlspecs_models_JMLInteger$1$iter,800 "this.vorg_jmlspecs_models_JMLIntegerIter(\"plus\", 0)");801 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {802 final org.jmlspecs.models.JMLInteger receiver$803 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();804 final org.jmlspecs.models.JMLInteger i2805 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();806 methodTests$.addTest807 (new TestPlus(receiver$, i2));808 vorg_jmlspecs_models_JMLInteger$1$iter.advance();809 }810 receivers$iter.advance();811 }812 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {813 // methodTests$ doesn't want more tests814 }815 overallTestSuite$.addTest(methodTests$);816 }817 /** Test for the plus method. */818 protected static class TestPlus extends OneTest {819 /** The receiver */820 private org.jmlspecs.models.JMLInteger receiver$;821 /** Argument i2 */822 private org.jmlspecs.models.JMLInteger i2;823 /** Initialize this instance. */824 public TestPlus(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {825 super("plus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));826 this.receiver$ = receiver$;827 this.i2 = i2;828 }829 protected void doCall() throws java.lang.Throwable {830 receiver$.plus(i2);831 }832 protected java.lang.String failMessage833 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)834 {835 java.lang.String msg = "\n\tMethod 'plus' applied to";836 msg += "\n\tReceiver: " + this.receiver$;837 msg += "\n\tArgument i2: " + this.i2;838 return msg;839 }840 }841 /** Add tests for the minus method842 * to the overall test suite. */843 private void addTestSuiteFor$TestMinus844 (junit.framework.TestSuite overallTestSuite$)845 {846 junit.framework.TestSuite methodTests$847 = this.emptyTestSuiteFor("minus");848 try {849 org.jmlspecs.jmlunit.strategies.IndefiniteIterator850 receivers$iter851 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator852 (this.vorg_jmlspecs_models_JMLIntegerIter("minus", 1));853 this.check_has_data854 (receivers$iter,855 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"minus\", 1))");856 while (!receivers$iter.atEnd()) {857 org.jmlspecs.jmlunit.strategies.IndefiniteIterator858 vorg_jmlspecs_models_JMLInteger$1$iter859 = this.vorg_jmlspecs_models_JMLIntegerIter("minus", 0);860 this.check_has_data861 (vorg_jmlspecs_models_JMLInteger$1$iter,862 "this.vorg_jmlspecs_models_JMLIntegerIter(\"minus\", 0)");863 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {864 final org.jmlspecs.models.JMLInteger receiver$865 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();866 final org.jmlspecs.models.JMLInteger i2867 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();868 methodTests$.addTest869 (new TestMinus(receiver$, i2));870 vorg_jmlspecs_models_JMLInteger$1$iter.advance();871 }872 receivers$iter.advance();873 }874 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {875 // methodTests$ doesn't want more tests876 }877 overallTestSuite$.addTest(methodTests$);878 }879 /** Test for the minus method. */880 protected static class TestMinus extends OneTest {881 /** The receiver */882 private org.jmlspecs.models.JMLInteger receiver$;883 /** Argument i2 */884 private org.jmlspecs.models.JMLInteger i2;885 /** Initialize this instance. */886 public TestMinus(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {887 super("minus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));888 this.receiver$ = receiver$;889 this.i2 = i2;890 }891 protected void doCall() throws java.lang.Throwable {892 receiver$.minus(i2);893 }894 protected java.lang.String failMessage895 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)896 {897 java.lang.String msg = "\n\tMethod 'minus' applied to";898 msg += "\n\tReceiver: " + this.receiver$;899 msg += "\n\tArgument i2: " + this.i2;900 return msg;901 }902 }903 /** Add tests for the times method904 * to the overall test suite. */905 private void addTestSuiteFor$TestTimes906 (junit.framework.TestSuite overallTestSuite$)907 {908 junit.framework.TestSuite methodTests$909 = this.emptyTestSuiteFor("times");910 try {911 org.jmlspecs.jmlunit.strategies.IndefiniteIterator912 receivers$iter913 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator914 (this.vorg_jmlspecs_models_JMLIntegerIter("times", 1));915 this.check_has_data916 (receivers$iter,917 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"times\", 1))");918 while (!receivers$iter.atEnd()) {919 org.jmlspecs.jmlunit.strategies.IndefiniteIterator920 vorg_jmlspecs_models_JMLInteger$1$iter921 = this.vorg_jmlspecs_models_JMLIntegerIter("times", 0);922 this.check_has_data923 (vorg_jmlspecs_models_JMLInteger$1$iter,924 "this.vorg_jmlspecs_models_JMLIntegerIter(\"times\", 0)");925 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {926 final org.jmlspecs.models.JMLInteger receiver$927 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();928 final org.jmlspecs.models.JMLInteger i2929 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();930 methodTests$.addTest931 (new TestTimes(receiver$, i2));932 vorg_jmlspecs_models_JMLInteger$1$iter.advance();933 }934 receivers$iter.advance();935 }936 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {937 // methodTests$ doesn't want more tests938 }939 overallTestSuite$.addTest(methodTests$);940 }941 /** Test for the times method. */942 protected static class TestTimes extends OneTest {943 /** The receiver */944 private org.jmlspecs.models.JMLInteger receiver$;945 /** Argument i2 */946 private org.jmlspecs.models.JMLInteger i2;947 /** Initialize this instance. */948 public TestTimes(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {949 super("times"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));950 this.receiver$ = receiver$;951 this.i2 = i2;952 }953 protected void doCall() throws java.lang.Throwable {954 receiver$.times(i2);955 }956 protected java.lang.String failMessage957 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)958 {959 java.lang.String msg = "\n\tMethod 'times' applied to";960 msg += "\n\tReceiver: " + this.receiver$;961 msg += "\n\tArgument i2: " + this.i2;962 return msg;963 }964 }965 /** Add tests for the dividedBy method966 * to the overall test suite. */967 private void addTestSuiteFor$TestDividedBy968 (junit.framework.TestSuite overallTestSuite$)969 {970 junit.framework.TestSuite methodTests$971 = this.emptyTestSuiteFor("dividedBy");972 try {973 org.jmlspecs.jmlunit.strategies.IndefiniteIterator974 receivers$iter975 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator976 (this.vorg_jmlspecs_models_JMLIntegerIter("dividedBy", 1));977 this.check_has_data978 (receivers$iter,979 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"dividedBy\", 1))");980 while (!receivers$iter.atEnd()) {981 org.jmlspecs.jmlunit.strategies.IndefiniteIterator982 vorg_jmlspecs_models_JMLInteger$1$iter983 = this.vorg_jmlspecs_models_JMLIntegerIter("dividedBy", 0);984 this.check_has_data985 (vorg_jmlspecs_models_JMLInteger$1$iter,986 "this.vorg_jmlspecs_models_JMLIntegerIter(\"dividedBy\", 0)");987 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {988 final org.jmlspecs.models.JMLInteger receiver$989 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();990 final org.jmlspecs.models.JMLInteger i2991 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();992 methodTests$.addTest993 (new TestDividedBy(receiver$, i2));994 vorg_jmlspecs_models_JMLInteger$1$iter.advance();995 }996 receivers$iter.advance();997 }998 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {999 // methodTests$ doesn't want more tests1000 }1001 overallTestSuite$.addTest(methodTests$);1002 }1003 /** Test for the dividedBy method. */1004 protected static class TestDividedBy extends OneTest {1005 /** The receiver */1006 private org.jmlspecs.models.JMLInteger receiver$;1007 /** Argument i2 */1008 private org.jmlspecs.models.JMLInteger i2;1009 /** Initialize this instance. */1010 public TestDividedBy(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1011 super("dividedBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1012 this.receiver$ = receiver$;1013 this.i2 = i2;1014 }1015 protected void doCall() throws java.lang.Throwable {1016 receiver$.dividedBy(i2);1017 }1018 protected java.lang.String failMessage1019 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1020 {1021 java.lang.String msg = "\n\tMethod 'dividedBy' applied to";1022 msg += "\n\tReceiver: " + this.receiver$;1023 msg += "\n\tArgument i2: " + this.i2;1024 return msg;1025 }1026 }1027 /** Add tests for the remainderBy method1028 * to the overall test suite. */1029 private void addTestSuiteFor$TestRemainderBy1030 (junit.framework.TestSuite overallTestSuite$)1031 {1032 junit.framework.TestSuite methodTests$1033 = this.emptyTestSuiteFor("remainderBy");1034 try {1035 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1036 receivers$iter1037 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1038 (this.vorg_jmlspecs_models_JMLIntegerIter("remainderBy", 1));1039 this.check_has_data1040 (receivers$iter,1041 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"remainderBy\", 1))");1042 while (!receivers$iter.atEnd()) {1043 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1044 vorg_jmlspecs_models_JMLInteger$1$iter1045 = this.vorg_jmlspecs_models_JMLIntegerIter("remainderBy", 0);1046 this.check_has_data1047 (vorg_jmlspecs_models_JMLInteger$1$iter,1048 "this.vorg_jmlspecs_models_JMLIntegerIter(\"remainderBy\", 0)");1049 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {1050 final org.jmlspecs.models.JMLInteger receiver$1051 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1052 final org.jmlspecs.models.JMLInteger i21053 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();1054 methodTests$.addTest1055 (new TestRemainderBy(receiver$, i2));1056 vorg_jmlspecs_models_JMLInteger$1$iter.advance();1057 }1058 receivers$iter.advance();1059 }1060 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1061 // methodTests$ doesn't want more tests1062 }1063 overallTestSuite$.addTest(methodTests$);1064 }1065 /** Test for the remainderBy method. */1066 protected static class TestRemainderBy extends OneTest {1067 /** The receiver */1068 private org.jmlspecs.models.JMLInteger receiver$;1069 /** Argument i2 */1070 private org.jmlspecs.models.JMLInteger i2;1071 /** Initialize this instance. */1072 public TestRemainderBy(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1073 super("remainderBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1074 this.receiver$ = receiver$;1075 this.i2 = i2;1076 }1077 protected void doCall() throws java.lang.Throwable {1078 receiver$.remainderBy(i2);1079 }1080 protected java.lang.String failMessage1081 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1082 {1083 java.lang.String msg = "\n\tMethod 'remainderBy' applied to";1084 msg += "\n\tReceiver: " + this.receiver$;1085 msg += "\n\tArgument i2: " + this.i2;1086 return msg;1087 }1088 }1089 /** Add tests for the greaterThan method1090 * to the overall test suite. */1091 private void addTestSuiteFor$TestGreaterThan1092 (junit.framework.TestSuite overallTestSuite$)1093 {1094 junit.framework.TestSuite methodTests$1095 = this.emptyTestSuiteFor("greaterThan");1096 try {1097 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1098 receivers$iter1099 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1100 (this.vorg_jmlspecs_models_JMLIntegerIter("greaterThan", 1));1101 this.check_has_data1102 (receivers$iter,1103 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"greaterThan\", 1))");1104 while (!receivers$iter.atEnd()) {1105 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1106 vorg_jmlspecs_models_JMLInteger$1$iter1107 = this.vorg_jmlspecs_models_JMLIntegerIter("greaterThan", 0);1108 this.check_has_data1109 (vorg_jmlspecs_models_JMLInteger$1$iter,1110 "this.vorg_jmlspecs_models_JMLIntegerIter(\"greaterThan\", 0)");1111 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {1112 final org.jmlspecs.models.JMLInteger receiver$1113 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1114 final org.jmlspecs.models.JMLInteger i21115 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();1116 methodTests$.addTest1117 (new TestGreaterThan(receiver$, i2));1118 vorg_jmlspecs_models_JMLInteger$1$iter.advance();1119 }1120 receivers$iter.advance();1121 }1122 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1123 // methodTests$ doesn't want more tests1124 }1125 overallTestSuite$.addTest(methodTests$);1126 }1127 /** Test for the greaterThan method. */1128 protected static class TestGreaterThan extends OneTest {1129 /** The receiver */1130 private org.jmlspecs.models.JMLInteger receiver$;1131 /** Argument i2 */1132 private org.jmlspecs.models.JMLInteger i2;1133 /** Initialize this instance. */1134 public TestGreaterThan(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1135 super("greaterThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1136 this.receiver$ = receiver$;1137 this.i2 = i2;1138 }1139 protected void doCall() throws java.lang.Throwable {1140 receiver$.greaterThan(i2);1141 }1142 protected java.lang.String failMessage1143 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1144 {1145 java.lang.String msg = "\n\tMethod 'greaterThan' applied to";1146 msg += "\n\tReceiver: " + this.receiver$;1147 msg += "\n\tArgument i2: " + this.i2;1148 return msg;1149 }1150 }1151 /** Add tests for the lessThan method1152 * to the overall test suite. */1153 private void addTestSuiteFor$TestLessThan1154 (junit.framework.TestSuite overallTestSuite$)1155 {1156 junit.framework.TestSuite methodTests$1157 = this.emptyTestSuiteFor("lessThan");1158 try {1159 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1160 receivers$iter1161 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1162 (this.vorg_jmlspecs_models_JMLIntegerIter("lessThan", 1));1163 this.check_has_data1164 (receivers$iter,1165 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"lessThan\", 1))");1166 while (!receivers$iter.atEnd()) {1167 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1168 vorg_jmlspecs_models_JMLInteger$1$iter1169 = this.vorg_jmlspecs_models_JMLIntegerIter("lessThan", 0);1170 this.check_has_data1171 (vorg_jmlspecs_models_JMLInteger$1$iter,1172 "this.vorg_jmlspecs_models_JMLIntegerIter(\"lessThan\", 0)");1173 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {1174 final org.jmlspecs.models.JMLInteger receiver$1175 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1176 final org.jmlspecs.models.JMLInteger i21177 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();1178 methodTests$.addTest1179 (new TestLessThan(receiver$, i2));1180 vorg_jmlspecs_models_JMLInteger$1$iter.advance();1181 }1182 receivers$iter.advance();1183 }1184 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1185 // methodTests$ doesn't want more tests1186 }1187 overallTestSuite$.addTest(methodTests$);1188 }1189 /** Test for the lessThan method. */1190 protected static class TestLessThan extends OneTest {1191 /** The receiver */1192 private org.jmlspecs.models.JMLInteger receiver$;1193 /** Argument i2 */1194 private org.jmlspecs.models.JMLInteger i2;1195 /** Initialize this instance. */1196 public TestLessThan(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1197 super("lessThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1198 this.receiver$ = receiver$;1199 this.i2 = i2;1200 }1201 protected void doCall() throws java.lang.Throwable {1202 receiver$.lessThan(i2);1203 }1204 protected java.lang.String failMessage1205 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1206 {1207 java.lang.String msg = "\n\tMethod 'lessThan' applied to";1208 msg += "\n\tReceiver: " + this.receiver$;1209 msg += "\n\tArgument i2: " + this.i2;1210 return msg;1211 }1212 }1213 /** Add tests for the greaterThanOrEqualTo method1214 * to the overall test suite. */1215 private void addTestSuiteFor$TestGreaterThanOrEqualTo1216 (junit.framework.TestSuite overallTestSuite$)1217 {1218 junit.framework.TestSuite methodTests$1219 = this.emptyTestSuiteFor("greaterThanOrEqualTo");1220 try {1221 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1222 receivers$iter1223 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1224 (this.vorg_jmlspecs_models_JMLIntegerIter("greaterThanOrEqualTo", 1));1225 this.check_has_data1226 (receivers$iter,1227 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"greaterThanOrEqualTo\", 1))");1228 while (!receivers$iter.atEnd()) {1229 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1230 vorg_jmlspecs_models_JMLInteger$1$iter1231 = this.vorg_jmlspecs_models_JMLIntegerIter("greaterThanOrEqualTo", 0);1232 this.check_has_data1233 (vorg_jmlspecs_models_JMLInteger$1$iter,1234 "this.vorg_jmlspecs_models_JMLIntegerIter(\"greaterThanOrEqualTo\", 0)");1235 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {1236 final org.jmlspecs.models.JMLInteger receiver$1237 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1238 final org.jmlspecs.models.JMLInteger i21239 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();1240 methodTests$.addTest1241 (new TestGreaterThanOrEqualTo(receiver$, i2));1242 vorg_jmlspecs_models_JMLInteger$1$iter.advance();1243 }1244 receivers$iter.advance();1245 }1246 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1247 // methodTests$ doesn't want more tests1248 }1249 overallTestSuite$.addTest(methodTests$);1250 }1251 /** Test for the greaterThanOrEqualTo method. */1252 protected static class TestGreaterThanOrEqualTo extends OneTest {1253 /** The receiver */1254 private org.jmlspecs.models.JMLInteger receiver$;1255 /** Argument i2 */1256 private org.jmlspecs.models.JMLInteger i2;1257 /** Initialize this instance. */1258 public TestGreaterThanOrEqualTo(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1259 super("greaterThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1260 this.receiver$ = receiver$;1261 this.i2 = i2;1262 }1263 protected void doCall() throws java.lang.Throwable {1264 receiver$.greaterThanOrEqualTo(i2);1265 }1266 protected java.lang.String failMessage1267 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1268 {1269 java.lang.String msg = "\n\tMethod 'greaterThanOrEqualTo' applied to";1270 msg += "\n\tReceiver: " + this.receiver$;1271 msg += "\n\tArgument i2: " + this.i2;1272 return msg;1273 }1274 }1275 /** Add tests for the lessThanOrEqualTo method1276 * to the overall test suite. */1277 private void addTestSuiteFor$TestLessThanOrEqualTo1278 (junit.framework.TestSuite overallTestSuite$)1279 {1280 junit.framework.TestSuite methodTests$1281 = this.emptyTestSuiteFor("lessThanOrEqualTo");1282 try {1283 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1284 receivers$iter1285 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1286 (this.vorg_jmlspecs_models_JMLIntegerIter("lessThanOrEqualTo", 1));1287 this.check_has_data1288 (receivers$iter,1289 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"lessThanOrEqualTo\", 1))");1290 while (!receivers$iter.atEnd()) {1291 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1292 vorg_jmlspecs_models_JMLInteger$1$iter1293 = this.vorg_jmlspecs_models_JMLIntegerIter("lessThanOrEqualTo", 0);1294 this.check_has_data1295 (vorg_jmlspecs_models_JMLInteger$1$iter,1296 "this.vorg_jmlspecs_models_JMLIntegerIter(\"lessThanOrEqualTo\", 0)");1297 while (!vorg_jmlspecs_models_JMLInteger$1$iter.atEnd()) {1298 final org.jmlspecs.models.JMLInteger receiver$1299 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1300 final org.jmlspecs.models.JMLInteger i21301 = (org.jmlspecs.models.JMLInteger) vorg_jmlspecs_models_JMLInteger$1$iter.get();1302 methodTests$.addTest1303 (new TestLessThanOrEqualTo(receiver$, i2));1304 vorg_jmlspecs_models_JMLInteger$1$iter.advance();1305 }1306 receivers$iter.advance();1307 }1308 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1309 // methodTests$ doesn't want more tests1310 }1311 overallTestSuite$.addTest(methodTests$);1312 }1313 /** Test for the lessThanOrEqualTo method. */1314 protected static class TestLessThanOrEqualTo extends OneTest {1315 /** The receiver */1316 private org.jmlspecs.models.JMLInteger receiver$;1317 /** Argument i2 */1318 private org.jmlspecs.models.JMLInteger i2;1319 /** Initialize this instance. */1320 public TestLessThanOrEqualTo(org.jmlspecs.models.JMLInteger receiver$, org.jmlspecs.models.JMLInteger i2) {1321 super("lessThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLInteger}"));1322 this.receiver$ = receiver$;1323 this.i2 = i2;1324 }1325 protected void doCall() throws java.lang.Throwable {1326 receiver$.lessThanOrEqualTo(i2);1327 }1328 protected java.lang.String failMessage1329 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1330 {1331 java.lang.String msg = "\n\tMethod 'lessThanOrEqualTo' applied to";1332 msg += "\n\tReceiver: " + this.receiver$;1333 msg += "\n\tArgument i2: " + this.i2;1334 return msg;1335 }1336 }1337 /** Add tests for the toString method1338 * to the overall test suite. */1339 private void addTestSuiteFor$TestToString1340 (junit.framework.TestSuite overallTestSuite$)1341 {1342 junit.framework.TestSuite methodTests$1343 = this.emptyTestSuiteFor("toString");1344 try {1345 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1346 receivers$iter1347 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1348 (this.vorg_jmlspecs_models_JMLIntegerIter("toString", 0));1349 this.check_has_data1350 (receivers$iter,1351 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLIntegerIter(\"toString\", 0))");1352 while (!receivers$iter.atEnd()) {1353 final org.jmlspecs.models.JMLInteger receiver$1354 = (org.jmlspecs.models.JMLInteger) receivers$iter.get();1355 methodTests$.addTest1356 (new TestToString(receiver$));1357 receivers$iter.advance();1358 }1359 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1360 // methodTests$ doesn't want more tests1361 }1362 overallTestSuite$.addTest(methodTests$);1363 }1364 /** Test for the toString method. */1365 protected static class TestToString extends OneTest {1366 /** The receiver */1367 private org.jmlspecs.models.JMLInteger receiver$;1368 /** Initialize this instance. */1369 public TestToString(org.jmlspecs.models.JMLInteger receiver$) {1370 super("toString");1371 this.receiver$ = receiver$;1372 }1373 protected void doCall() throws java.lang.Throwable {1374 receiver$.toString();...

Full Screen

Full Screen

Source:JMLChar_JML_Test.java Github

copy

Full Screen

...15 /** Initialize this class. */16 public JMLChar_JML_Test(java.lang.String name) {17 super(name);18 }19 /** Run the tests. */20 public static void main(java.lang.String[] args) {21 org.jmlspecs.jmlunit.JMLTestRunner.run(suite());22 // You can also use a JUnit test runner such as:23 // junit.textui.TestRunner.run(suite());24 }25 /** Test to see if the code for class JMLChar26 * has been compiled with runtime assertion checking (i.e., by jmlc).27 * Code that is not compiled with jmlc would not make an effective test,28 * since no assertion checking would be done. */29 public void test$IsRACCompiled() {30 junit.framework.Assert.assertTrue("code for class JMLChar"31 + " was not compiled with jmlc"32 + " so no assertions will be checked!",33 org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLChar.class)34 );35 }36 /** Return the test suite for this test class. This will have37 * added to it at least test$IsRACCompiled(), and any test methods38 * written explicitly by the user in the superclass. It will also39 * have added test suites for each testing each method and40 * constructor.41 */42 //@ ensures \result != null;43 public static junit.framework.Test suite() {44 JMLChar_JML_Test testobj45 = new JMLChar_JML_Test("JMLChar_JML_Test");46 junit.framework.TestSuite testsuite = testobj.overallTestSuite();47 // Add instances of Test found by the reflection mechanism.48 testsuite.addTestSuite(JMLChar_JML_Test.class);49 testobj.addTestSuiteForEachMethod(testsuite);50 return testsuite;51 }52 /** A JUnit test object that can run a single test method. This53 * is defined as a nested class solely for convenience; it can't54 * be defined once and for all because it must subclass its55 * enclosing class.56 */57 protected static abstract class OneTest extends JMLChar_JML_Test {58 /** Initialize this test object. */59 public OneTest(String name) {60 super(name);61 }62 /** The result object that holds information about testing. */63 protected junit.framework.TestResult result;64 //@ also65 //@ requires result != null;66 public void run(junit.framework.TestResult result) {67 this.result = result;68 super.run(result);69 }70 /* Run a single test and decide whether the test was71 * successful, meaningless, or a failure. This is the72 * Template Method pattern abstraction of the inner loop in a73 * JML/JUnit test. */74 public void runTest() throws java.lang.Throwable {75 try {76 // The call being tested!77 doCall();78 }79 catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) {80 // meaningless test input81 addMeaningless();82 } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) {83 // test failure84 int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel();85 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel86 (org.jmlspecs.jmlrac.runtime.JMLOption.NONE);87 try {88 java.lang.String failmsg = this.failMessage(e);89 junit.framework.AssertionFailedError err90 = new junit.framework.AssertionFailedError(failmsg);91 err.setStackTrace(new java.lang.StackTraceElement[]{});92 err.initCause(e);93 result.addFailure(this, err);94 } finally {95 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l);96 }97 } catch (java.lang.Throwable e) {98 // test success99 }100 }101 /** Call the method to be tested with the appropriate arguments. */102 protected abstract void doCall() throws java.lang.Throwable;103 /** Format the error message for a test failure, based on the104 * method's arguments. */105 protected abstract java.lang.String failMessage106 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e);107 /** Inform listeners that a meaningless test was run. */108 private void addMeaningless() {109 if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) {110 ((org.jmlspecs.jmlunit.JMLTestResult)result)111 .addMeaningless(this);112 }113 }114 }115 /** Create the tests that are to be run for testing the class116 * JMLChar. The framework will then run them.117 * @param overallTestSuite$ The suite accumulating all of the tests118 * for this driver class.119 */120 //@ requires overallTestSuite$ != null;121 public void addTestSuiteForEachMethod122 (junit.framework.TestSuite overallTestSuite$)123 {124 try {125 this.addTestSuiteFor$TestJMLChar(overallTestSuite$);126 } catch (java.lang.Throwable ex) {127 overallTestSuite$.addTest128 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));129 }130 try {131 this.addTestSuiteFor$TestJMLChar$1(overallTestSuite$);132 } catch (java.lang.Throwable ex) {133 overallTestSuite$.addTest134 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));135 }136 try {137 this.addTestSuiteFor$TestJMLChar$2(overallTestSuite$);138 } catch (java.lang.Throwable ex) {139 overallTestSuite$.addTest140 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));141 }142 try {143 this.addTestSuiteFor$TestClone(overallTestSuite$);144 } catch (java.lang.Throwable ex) {145 overallTestSuite$.addTest146 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));147 }148 try {149 this.addTestSuiteFor$TestCharValue(overallTestSuite$);150 } catch (java.lang.Throwable ex) {151 overallTestSuite$.addTest152 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));153 }154 try {155 this.addTestSuiteFor$TestGetChar(overallTestSuite$);156 } catch (java.lang.Throwable ex) {157 overallTestSuite$.addTest158 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));159 }160 try {161 this.addTestSuiteFor$TestHashCode(overallTestSuite$);162 } catch (java.lang.Throwable ex) {163 overallTestSuite$.addTest164 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));165 }166 try {167 this.addTestSuiteFor$TestCompareTo(overallTestSuite$);168 } catch (java.lang.Throwable ex) {169 overallTestSuite$.addTest170 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));171 }172 try {173 this.addTestSuiteFor$TestEquals(overallTestSuite$);174 } catch (java.lang.Throwable ex) {175 overallTestSuite$.addTest176 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));177 }178 try {179 this.addTestSuiteFor$TestToString(overallTestSuite$);180 } catch (java.lang.Throwable ex) {181 overallTestSuite$.addTest182 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));183 }184 try {185 this.addTestSuiteFor$TestIntValue(overallTestSuite$);186 } catch (java.lang.Throwable ex) {187 overallTestSuite$.addTest188 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));189 }190 try {191 this.addTestSuiteFor$TestPlus(overallTestSuite$);192 } catch (java.lang.Throwable ex) {193 overallTestSuite$.addTest194 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));195 }196 try {197 this.addTestSuiteFor$TestMinus(overallTestSuite$);198 } catch (java.lang.Throwable ex) {199 overallTestSuite$.addTest200 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));201 }202 try {203 this.addTestSuiteFor$TestTimes(overallTestSuite$);204 } catch (java.lang.Throwable ex) {205 overallTestSuite$.addTest206 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));207 }208 try {209 this.addTestSuiteFor$TestDividedBy(overallTestSuite$);210 } catch (java.lang.Throwable ex) {211 overallTestSuite$.addTest212 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));213 }214 try {215 this.addTestSuiteFor$TestRemainderBy(overallTestSuite$);216 } catch (java.lang.Throwable ex) {217 overallTestSuite$.addTest218 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));219 }220 try {221 this.addTestSuiteFor$TestGreaterThan(overallTestSuite$);222 } catch (java.lang.Throwable ex) {223 overallTestSuite$.addTest224 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));225 }226 try {227 this.addTestSuiteFor$TestLessThan(overallTestSuite$);228 } catch (java.lang.Throwable ex) {229 overallTestSuite$.addTest230 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));231 }232 try {233 this.addTestSuiteFor$TestGreaterThanOrEqualTo(overallTestSuite$);234 } catch (java.lang.Throwable ex) {235 overallTestSuite$.addTest236 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));237 }238 try {239 this.addTestSuiteFor$TestLessThanOrEqualTo(overallTestSuite$);240 } catch (java.lang.Throwable ex) {241 overallTestSuite$.addTest242 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));243 }244 }245 /** Add tests for the JMLChar contructor246 * to the overall test suite. */247 private void addTestSuiteFor$TestJMLChar248 (junit.framework.TestSuite overallTestSuite$)249 {250 junit.framework.TestSuite methodTests$251 = this.emptyTestSuiteFor("JMLChar");252 try {253 methodTests$.addTest254 (new TestJMLChar());255 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {256 // methodTests$ doesn't want more tests257 }258 overallTestSuite$.addTest(methodTests$);259 }260 /** Test for the JMLChar contructor. */261 protected static class TestJMLChar extends OneTest {262 /** Initialize this instance. */263 public TestJMLChar() {264 super("JMLChar");265 }266 protected void doCall() throws java.lang.Throwable {267 new JMLChar();268 }269 protected java.lang.String failMessage270 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)271 {272 java.lang.String msg = "\n\tContructor 'JMLChar'";273 return msg;274 }275 }276 /** Add tests for the JMLChar contructor277 * to the overall test suite. */278 private void addTestSuiteFor$TestJMLChar$1279 (junit.framework.TestSuite overallTestSuite$)280 {281 junit.framework.TestSuite methodTests$282 = this.emptyTestSuiteFor("JMLChar");283 try {284 org.jmlspecs.jmlunit.strategies.CharIterator285 vchar$1$iter286 = this.vcharIter("JMLChar", 0);287 this.check_has_data288 (vchar$1$iter,289 "this.vcharIter(\"JMLChar\", 0)");290 while (!vchar$1$iter.atEnd()) {291 final char c292 = vchar$1$iter.getChar();293 methodTests$.addTest294 (new TestJMLChar$1(c));295 vchar$1$iter.advance();296 }297 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {298 // methodTests$ doesn't want more tests299 }300 overallTestSuite$.addTest(methodTests$);301 }302 /** Test for the JMLChar contructor. */303 protected static class TestJMLChar$1 extends OneTest {304 /** Argument c */305 private char c;306 /** Initialize this instance. */307 public TestJMLChar$1(char c) {308 super("JMLChar"+ ":" + "\'"+charToString(c)+"\'");309 this.c = c;310 }311 protected void doCall() throws java.lang.Throwable {312 new JMLChar(c);313 }314 protected java.lang.String failMessage315 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)316 {317 java.lang.String msg = "\n\tContructor 'JMLChar' applied to";318 msg += "\n\tArgument c: " + this.c;319 return msg;320 }321 }322 /** Add tests for the JMLChar contructor323 * to the overall test suite. */324 private void addTestSuiteFor$TestJMLChar$2325 (junit.framework.TestSuite overallTestSuite$)326 {327 junit.framework.TestSuite methodTests$328 = this.emptyTestSuiteFor("JMLChar");329 try {330 org.jmlspecs.jmlunit.strategies.IndefiniteIterator331 vjava_lang_Character$1$iter332 = this.vjava_lang_CharacterIter("JMLChar", 0);333 this.check_has_data334 (vjava_lang_Character$1$iter,335 "this.vjava_lang_CharacterIter(\"JMLChar\", 0)");336 while (!vjava_lang_Character$1$iter.atEnd()) {337 final java.lang.Character inChar338 = (java.lang.Character) vjava_lang_Character$1$iter.get();339 methodTests$.addTest340 (new TestJMLChar$2(inChar));341 vjava_lang_Character$1$iter.advance();342 }343 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {344 // methodTests$ doesn't want more tests345 }346 overallTestSuite$.addTest(methodTests$);347 }348 /** Test for the JMLChar contructor. */349 protected static class TestJMLChar$2 extends OneTest {350 /** Argument inChar */351 private java.lang.Character inChar;352 /** Initialize this instance. */353 public TestJMLChar$2(java.lang.Character inChar) {354 super("JMLChar"+ ":" + (inChar==null? "null" :"{java.lang.Character}"));355 this.inChar = inChar;356 }357 protected void doCall() throws java.lang.Throwable {358 new JMLChar(inChar);359 }360 protected java.lang.String failMessage361 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)362 {363 java.lang.String msg = "\n\tContructor 'JMLChar' applied to";364 msg += "\n\tArgument inChar: " + this.inChar;365 return msg;366 }367 }368 /** Add tests for the clone method369 * to the overall test suite. */370 private void addTestSuiteFor$TestClone371 (junit.framework.TestSuite overallTestSuite$)372 {373 junit.framework.TestSuite methodTests$374 = this.emptyTestSuiteFor("clone");375 try {376 org.jmlspecs.jmlunit.strategies.IndefiniteIterator377 receivers$iter378 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator379 (this.vorg_jmlspecs_models_JMLCharIter("clone", 0));380 this.check_has_data381 (receivers$iter,382 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"clone\", 0))");383 while (!receivers$iter.atEnd()) {384 final org.jmlspecs.models.JMLChar receiver$385 = (org.jmlspecs.models.JMLChar) receivers$iter.get();386 methodTests$.addTest387 (new TestClone(receiver$));388 receivers$iter.advance();389 }390 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {391 // methodTests$ doesn't want more tests392 }393 overallTestSuite$.addTest(methodTests$);394 }395 /** Test for the clone method. */396 protected static class TestClone extends OneTest {397 /** The receiver */398 private org.jmlspecs.models.JMLChar receiver$;399 /** Initialize this instance. */400 public TestClone(org.jmlspecs.models.JMLChar receiver$) {401 super("clone");402 this.receiver$ = receiver$;403 }404 protected void doCall() throws java.lang.Throwable {405 receiver$.clone();406 }407 protected java.lang.String failMessage408 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)409 {410 java.lang.String msg = "\n\tMethod 'clone' applied to";411 msg += "\n\tReceiver: " + this.receiver$;412 return msg;413 }414 }415 /** Add tests for the charValue method416 * to the overall test suite. */417 private void addTestSuiteFor$TestCharValue418 (junit.framework.TestSuite overallTestSuite$)419 {420 junit.framework.TestSuite methodTests$421 = this.emptyTestSuiteFor("charValue");422 try {423 org.jmlspecs.jmlunit.strategies.IndefiniteIterator424 receivers$iter425 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator426 (this.vorg_jmlspecs_models_JMLCharIter("charValue", 0));427 this.check_has_data428 (receivers$iter,429 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"charValue\", 0))");430 while (!receivers$iter.atEnd()) {431 final org.jmlspecs.models.JMLChar receiver$432 = (org.jmlspecs.models.JMLChar) receivers$iter.get();433 methodTests$.addTest434 (new TestCharValue(receiver$));435 receivers$iter.advance();436 }437 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {438 // methodTests$ doesn't want more tests439 }440 overallTestSuite$.addTest(methodTests$);441 }442 /** Test for the charValue method. */443 protected static class TestCharValue extends OneTest {444 /** The receiver */445 private org.jmlspecs.models.JMLChar receiver$;446 /** Initialize this instance. */447 public TestCharValue(org.jmlspecs.models.JMLChar receiver$) {448 super("charValue");449 this.receiver$ = receiver$;450 }451 protected void doCall() throws java.lang.Throwable {452 receiver$.charValue();453 }454 protected java.lang.String failMessage455 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)456 {457 java.lang.String msg = "\n\tMethod 'charValue' applied to";458 msg += "\n\tReceiver: " + this.receiver$;459 return msg;460 }461 }462 /** Add tests for the getChar method463 * to the overall test suite. */464 private void addTestSuiteFor$TestGetChar465 (junit.framework.TestSuite overallTestSuite$)466 {467 junit.framework.TestSuite methodTests$468 = this.emptyTestSuiteFor("getChar");469 try {470 org.jmlspecs.jmlunit.strategies.IndefiniteIterator471 receivers$iter472 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator473 (this.vorg_jmlspecs_models_JMLCharIter("getChar", 0));474 this.check_has_data475 (receivers$iter,476 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"getChar\", 0))");477 while (!receivers$iter.atEnd()) {478 final org.jmlspecs.models.JMLChar receiver$479 = (org.jmlspecs.models.JMLChar) receivers$iter.get();480 methodTests$.addTest481 (new TestGetChar(receiver$));482 receivers$iter.advance();483 }484 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {485 // methodTests$ doesn't want more tests486 }487 overallTestSuite$.addTest(methodTests$);488 }489 /** Test for the getChar method. */490 protected static class TestGetChar extends OneTest {491 /** The receiver */492 private org.jmlspecs.models.JMLChar receiver$;493 /** Initialize this instance. */494 public TestGetChar(org.jmlspecs.models.JMLChar receiver$) {495 super("getChar");496 this.receiver$ = receiver$;497 }498 protected void doCall() throws java.lang.Throwable {499 receiver$.getChar();500 }501 protected java.lang.String failMessage502 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)503 {504 java.lang.String msg = "\n\tMethod 'getChar' applied to";505 msg += "\n\tReceiver: " + this.receiver$;506 return msg;507 }508 }509 /** Add tests for the hashCode method510 * to the overall test suite. */511 private void addTestSuiteFor$TestHashCode512 (junit.framework.TestSuite overallTestSuite$)513 {514 junit.framework.TestSuite methodTests$515 = this.emptyTestSuiteFor("hashCode");516 try {517 org.jmlspecs.jmlunit.strategies.IndefiniteIterator518 receivers$iter519 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator520 (this.vorg_jmlspecs_models_JMLCharIter("hashCode", 0));521 this.check_has_data522 (receivers$iter,523 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"hashCode\", 0))");524 while (!receivers$iter.atEnd()) {525 final org.jmlspecs.models.JMLChar receiver$526 = (org.jmlspecs.models.JMLChar) receivers$iter.get();527 methodTests$.addTest528 (new TestHashCode(receiver$));529 receivers$iter.advance();530 }531 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {532 // methodTests$ doesn't want more tests533 }534 overallTestSuite$.addTest(methodTests$);535 }536 /** Test for the hashCode method. */537 protected static class TestHashCode extends OneTest {538 /** The receiver */539 private org.jmlspecs.models.JMLChar receiver$;540 /** Initialize this instance. */541 public TestHashCode(org.jmlspecs.models.JMLChar receiver$) {542 super("hashCode");543 this.receiver$ = receiver$;544 }545 protected void doCall() throws java.lang.Throwable {546 receiver$.hashCode();547 }548 protected java.lang.String failMessage549 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)550 {551 java.lang.String msg = "\n\tMethod 'hashCode' applied to";552 msg += "\n\tReceiver: " + this.receiver$;553 return msg;554 }555 }556 /** Add tests for the compareTo method557 * to the overall test suite. */558 private void addTestSuiteFor$TestCompareTo559 (junit.framework.TestSuite overallTestSuite$)560 {561 junit.framework.TestSuite methodTests$562 = this.emptyTestSuiteFor("compareTo");563 try {564 org.jmlspecs.jmlunit.strategies.IndefiniteIterator565 receivers$iter566 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator567 (this.vorg_jmlspecs_models_JMLCharIter("compareTo", 1));568 this.check_has_data569 (receivers$iter,570 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"compareTo\", 1))");571 while (!receivers$iter.atEnd()) {572 org.jmlspecs.jmlunit.strategies.IndefiniteIterator573 vjava_lang_Object$1$iter574 = this.vjava_lang_ObjectIter("compareTo", 0);575 this.check_has_data576 (vjava_lang_Object$1$iter,577 "this.vjava_lang_ObjectIter(\"compareTo\", 0)");578 while (!vjava_lang_Object$1$iter.atEnd()) {579 final org.jmlspecs.models.JMLChar receiver$580 = (org.jmlspecs.models.JMLChar) receivers$iter.get();581 final java.lang.Object op2582 = (java.lang.Object) vjava_lang_Object$1$iter.get();583 methodTests$.addTest584 (new TestCompareTo(receiver$, op2));585 vjava_lang_Object$1$iter.advance();586 }587 receivers$iter.advance();588 }589 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {590 // methodTests$ doesn't want more tests591 }592 overallTestSuite$.addTest(methodTests$);593 }594 /** Test for the compareTo method. */595 protected static class TestCompareTo extends OneTest {596 /** The receiver */597 private org.jmlspecs.models.JMLChar receiver$;598 /** Argument op2 */599 private java.lang.Object op2;600 /** Initialize this instance. */601 public TestCompareTo(org.jmlspecs.models.JMLChar receiver$, java.lang.Object op2) {602 super("compareTo"+ ":" + (op2==null? "null" :"{java.lang.Object}"));603 this.receiver$ = receiver$;604 this.op2 = op2;605 }606 protected void doCall() throws java.lang.Throwable {607 receiver$.compareTo(op2);608 }609 protected java.lang.String failMessage610 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)611 {612 java.lang.String msg = "\n\tMethod 'compareTo' applied to";613 msg += "\n\tReceiver: " + this.receiver$;614 msg += "\n\tArgument op2: " + this.op2;615 return msg;616 }617 }618 /** Add tests for the equals method619 * to the overall test suite. */620 private void addTestSuiteFor$TestEquals621 (junit.framework.TestSuite overallTestSuite$)622 {623 junit.framework.TestSuite methodTests$624 = this.emptyTestSuiteFor("equals");625 try {626 org.jmlspecs.jmlunit.strategies.IndefiniteIterator627 receivers$iter628 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator629 (this.vorg_jmlspecs_models_JMLCharIter("equals", 1));630 this.check_has_data631 (receivers$iter,632 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"equals\", 1))");633 while (!receivers$iter.atEnd()) {634 org.jmlspecs.jmlunit.strategies.IndefiniteIterator635 vjava_lang_Object$1$iter636 = this.vjava_lang_ObjectIter("equals", 0);637 this.check_has_data638 (vjava_lang_Object$1$iter,639 "this.vjava_lang_ObjectIter(\"equals\", 0)");640 while (!vjava_lang_Object$1$iter.atEnd()) {641 final org.jmlspecs.models.JMLChar receiver$642 = (org.jmlspecs.models.JMLChar) receivers$iter.get();643 final java.lang.Object obj644 = (java.lang.Object) vjava_lang_Object$1$iter.get();645 methodTests$.addTest646 (new TestEquals(receiver$, obj));647 vjava_lang_Object$1$iter.advance();648 }649 receivers$iter.advance();650 }651 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {652 // methodTests$ doesn't want more tests653 }654 overallTestSuite$.addTest(methodTests$);655 }656 /** Test for the equals method. */657 protected static class TestEquals extends OneTest {658 /** The receiver */659 private org.jmlspecs.models.JMLChar receiver$;660 /** Argument obj */661 private java.lang.Object obj;662 /** Initialize this instance. */663 public TestEquals(org.jmlspecs.models.JMLChar receiver$, java.lang.Object obj) {664 super("equals"+ ":" + (obj==null? "null" :"{java.lang.Object}"));665 this.receiver$ = receiver$;666 this.obj = obj;667 }668 protected void doCall() throws java.lang.Throwable {669 receiver$.equals(obj);670 }671 protected java.lang.String failMessage672 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)673 {674 java.lang.String msg = "\n\tMethod 'equals' applied to";675 msg += "\n\tReceiver: " + this.receiver$;676 msg += "\n\tArgument obj: " + this.obj;677 return msg;678 }679 }680 /** Add tests for the toString method681 * to the overall test suite. */682 private void addTestSuiteFor$TestToString683 (junit.framework.TestSuite overallTestSuite$)684 {685 junit.framework.TestSuite methodTests$686 = this.emptyTestSuiteFor("toString");687 try {688 org.jmlspecs.jmlunit.strategies.IndefiniteIterator689 receivers$iter690 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator691 (this.vorg_jmlspecs_models_JMLCharIter("toString", 0));692 this.check_has_data693 (receivers$iter,694 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"toString\", 0))");695 while (!receivers$iter.atEnd()) {696 final org.jmlspecs.models.JMLChar receiver$697 = (org.jmlspecs.models.JMLChar) receivers$iter.get();698 methodTests$.addTest699 (new TestToString(receiver$));700 receivers$iter.advance();701 }702 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {703 // methodTests$ doesn't want more tests704 }705 overallTestSuite$.addTest(methodTests$);706 }707 /** Test for the toString method. */708 protected static class TestToString extends OneTest {709 /** The receiver */710 private org.jmlspecs.models.JMLChar receiver$;711 /** Initialize this instance. */712 public TestToString(org.jmlspecs.models.JMLChar receiver$) {713 super("toString");714 this.receiver$ = receiver$;715 }716 protected void doCall() throws java.lang.Throwable {717 receiver$.toString();718 }719 protected java.lang.String failMessage720 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)721 {722 java.lang.String msg = "\n\tMethod 'toString' applied to";723 msg += "\n\tReceiver: " + this.receiver$;724 return msg;725 }726 }727 /** Add tests for the intValue method728 * to the overall test suite. */729 private void addTestSuiteFor$TestIntValue730 (junit.framework.TestSuite overallTestSuite$)731 {732 junit.framework.TestSuite methodTests$733 = this.emptyTestSuiteFor("intValue");734 try {735 org.jmlspecs.jmlunit.strategies.IndefiniteIterator736 receivers$iter737 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator738 (this.vorg_jmlspecs_models_JMLCharIter("intValue", 0));739 this.check_has_data740 (receivers$iter,741 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"intValue\", 0))");742 while (!receivers$iter.atEnd()) {743 final org.jmlspecs.models.JMLChar receiver$744 = (org.jmlspecs.models.JMLChar) receivers$iter.get();745 methodTests$.addTest746 (new TestIntValue(receiver$));747 receivers$iter.advance();748 }749 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {750 // methodTests$ doesn't want more tests751 }752 overallTestSuite$.addTest(methodTests$);753 }754 /** Test for the intValue method. */755 protected static class TestIntValue extends OneTest {756 /** The receiver */757 private org.jmlspecs.models.JMLChar receiver$;758 /** Initialize this instance. */759 public TestIntValue(org.jmlspecs.models.JMLChar receiver$) {760 super("intValue");761 this.receiver$ = receiver$;762 }763 protected void doCall() throws java.lang.Throwable {764 receiver$.intValue();765 }766 protected java.lang.String failMessage767 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)768 {769 java.lang.String msg = "\n\tMethod 'intValue' applied to";770 msg += "\n\tReceiver: " + this.receiver$;771 return msg;772 }773 }774 /** Add tests for the plus method775 * to the overall test suite. */776 private void addTestSuiteFor$TestPlus777 (junit.framework.TestSuite overallTestSuite$)778 {779 junit.framework.TestSuite methodTests$780 = this.emptyTestSuiteFor("plus");781 try {782 org.jmlspecs.jmlunit.strategies.IndefiniteIterator783 receivers$iter784 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator785 (this.vorg_jmlspecs_models_JMLCharIter("plus", 1));786 this.check_has_data787 (receivers$iter,788 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"plus\", 1))");789 while (!receivers$iter.atEnd()) {790 org.jmlspecs.jmlunit.strategies.IndefiniteIterator791 vorg_jmlspecs_models_JMLChar$1$iter792 = this.vorg_jmlspecs_models_JMLCharIter("plus", 0);793 this.check_has_data794 (vorg_jmlspecs_models_JMLChar$1$iter,795 "this.vorg_jmlspecs_models_JMLCharIter(\"plus\", 0)");796 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {797 final org.jmlspecs.models.JMLChar receiver$798 = (org.jmlspecs.models.JMLChar) receivers$iter.get();799 final org.jmlspecs.models.JMLChar i2800 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();801 methodTests$.addTest802 (new TestPlus(receiver$, i2));803 vorg_jmlspecs_models_JMLChar$1$iter.advance();804 }805 receivers$iter.advance();806 }807 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {808 // methodTests$ doesn't want more tests809 }810 overallTestSuite$.addTest(methodTests$);811 }812 /** Test for the plus method. */813 protected static class TestPlus extends OneTest {814 /** The receiver */815 private org.jmlspecs.models.JMLChar receiver$;816 /** Argument i2 */817 private org.jmlspecs.models.JMLChar i2;818 /** Initialize this instance. */819 public TestPlus(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {820 super("plus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));821 this.receiver$ = receiver$;822 this.i2 = i2;823 }824 protected void doCall() throws java.lang.Throwable {825 receiver$.plus(i2);826 }827 protected java.lang.String failMessage828 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)829 {830 java.lang.String msg = "\n\tMethod 'plus' applied to";831 msg += "\n\tReceiver: " + this.receiver$;832 msg += "\n\tArgument i2: " + this.i2;833 return msg;834 }835 }836 /** Add tests for the minus method837 * to the overall test suite. */838 private void addTestSuiteFor$TestMinus839 (junit.framework.TestSuite overallTestSuite$)840 {841 junit.framework.TestSuite methodTests$842 = this.emptyTestSuiteFor("minus");843 try {844 org.jmlspecs.jmlunit.strategies.IndefiniteIterator845 receivers$iter846 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator847 (this.vorg_jmlspecs_models_JMLCharIter("minus", 1));848 this.check_has_data849 (receivers$iter,850 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"minus\", 1))");851 while (!receivers$iter.atEnd()) {852 org.jmlspecs.jmlunit.strategies.IndefiniteIterator853 vorg_jmlspecs_models_JMLChar$1$iter854 = this.vorg_jmlspecs_models_JMLCharIter("minus", 0);855 this.check_has_data856 (vorg_jmlspecs_models_JMLChar$1$iter,857 "this.vorg_jmlspecs_models_JMLCharIter(\"minus\", 0)");858 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {859 final org.jmlspecs.models.JMLChar receiver$860 = (org.jmlspecs.models.JMLChar) receivers$iter.get();861 final org.jmlspecs.models.JMLChar i2862 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();863 methodTests$.addTest864 (new TestMinus(receiver$, i2));865 vorg_jmlspecs_models_JMLChar$1$iter.advance();866 }867 receivers$iter.advance();868 }869 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {870 // methodTests$ doesn't want more tests871 }872 overallTestSuite$.addTest(methodTests$);873 }874 /** Test for the minus method. */875 protected static class TestMinus extends OneTest {876 /** The receiver */877 private org.jmlspecs.models.JMLChar receiver$;878 /** Argument i2 */879 private org.jmlspecs.models.JMLChar i2;880 /** Initialize this instance. */881 public TestMinus(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {882 super("minus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));883 this.receiver$ = receiver$;884 this.i2 = i2;885 }886 protected void doCall() throws java.lang.Throwable {887 receiver$.minus(i2);888 }889 protected java.lang.String failMessage890 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)891 {892 java.lang.String msg = "\n\tMethod 'minus' applied to";893 msg += "\n\tReceiver: " + this.receiver$;894 msg += "\n\tArgument i2: " + this.i2;895 return msg;896 }897 }898 /** Add tests for the times method899 * to the overall test suite. */900 private void addTestSuiteFor$TestTimes901 (junit.framework.TestSuite overallTestSuite$)902 {903 junit.framework.TestSuite methodTests$904 = this.emptyTestSuiteFor("times");905 try {906 org.jmlspecs.jmlunit.strategies.IndefiniteIterator907 receivers$iter908 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator909 (this.vorg_jmlspecs_models_JMLCharIter("times", 1));910 this.check_has_data911 (receivers$iter,912 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"times\", 1))");913 while (!receivers$iter.atEnd()) {914 org.jmlspecs.jmlunit.strategies.IndefiniteIterator915 vorg_jmlspecs_models_JMLChar$1$iter916 = this.vorg_jmlspecs_models_JMLCharIter("times", 0);917 this.check_has_data918 (vorg_jmlspecs_models_JMLChar$1$iter,919 "this.vorg_jmlspecs_models_JMLCharIter(\"times\", 0)");920 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {921 final org.jmlspecs.models.JMLChar receiver$922 = (org.jmlspecs.models.JMLChar) receivers$iter.get();923 final org.jmlspecs.models.JMLChar i2924 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();925 methodTests$.addTest926 (new TestTimes(receiver$, i2));927 vorg_jmlspecs_models_JMLChar$1$iter.advance();928 }929 receivers$iter.advance();930 }931 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {932 // methodTests$ doesn't want more tests933 }934 overallTestSuite$.addTest(methodTests$);935 }936 /** Test for the times method. */937 protected static class TestTimes extends OneTest {938 /** The receiver */939 private org.jmlspecs.models.JMLChar receiver$;940 /** Argument i2 */941 private org.jmlspecs.models.JMLChar i2;942 /** Initialize this instance. */943 public TestTimes(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {944 super("times"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));945 this.receiver$ = receiver$;946 this.i2 = i2;947 }948 protected void doCall() throws java.lang.Throwable {949 receiver$.times(i2);950 }951 protected java.lang.String failMessage952 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)953 {954 java.lang.String msg = "\n\tMethod 'times' applied to";955 msg += "\n\tReceiver: " + this.receiver$;956 msg += "\n\tArgument i2: " + this.i2;957 return msg;958 }959 }960 /** Add tests for the dividedBy method961 * to the overall test suite. */962 private void addTestSuiteFor$TestDividedBy963 (junit.framework.TestSuite overallTestSuite$)964 {965 junit.framework.TestSuite methodTests$966 = this.emptyTestSuiteFor("dividedBy");967 try {968 org.jmlspecs.jmlunit.strategies.IndefiniteIterator969 receivers$iter970 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator971 (this.vorg_jmlspecs_models_JMLCharIter("dividedBy", 1));972 this.check_has_data973 (receivers$iter,974 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"dividedBy\", 1))");975 while (!receivers$iter.atEnd()) {976 org.jmlspecs.jmlunit.strategies.IndefiniteIterator977 vorg_jmlspecs_models_JMLChar$1$iter978 = this.vorg_jmlspecs_models_JMLCharIter("dividedBy", 0);979 this.check_has_data980 (vorg_jmlspecs_models_JMLChar$1$iter,981 "this.vorg_jmlspecs_models_JMLCharIter(\"dividedBy\", 0)");982 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {983 final org.jmlspecs.models.JMLChar receiver$984 = (org.jmlspecs.models.JMLChar) receivers$iter.get();985 final org.jmlspecs.models.JMLChar i2986 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();987 methodTests$.addTest988 (new TestDividedBy(receiver$, i2));989 vorg_jmlspecs_models_JMLChar$1$iter.advance();990 }991 receivers$iter.advance();992 }993 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {994 // methodTests$ doesn't want more tests995 }996 overallTestSuite$.addTest(methodTests$);997 }998 /** Test for the dividedBy method. */999 protected static class TestDividedBy extends OneTest {1000 /** The receiver */1001 private org.jmlspecs.models.JMLChar receiver$;1002 /** Argument i2 */1003 private org.jmlspecs.models.JMLChar i2;1004 /** Initialize this instance. */1005 public TestDividedBy(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1006 super("dividedBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1007 this.receiver$ = receiver$;1008 this.i2 = i2;1009 }1010 protected void doCall() throws java.lang.Throwable {1011 receiver$.dividedBy(i2);1012 }1013 protected java.lang.String failMessage1014 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1015 {1016 java.lang.String msg = "\n\tMethod 'dividedBy' applied to";1017 msg += "\n\tReceiver: " + this.receiver$;1018 msg += "\n\tArgument i2: " + this.i2;1019 return msg;1020 }1021 }1022 /** Add tests for the remainderBy method1023 * to the overall test suite. */1024 private void addTestSuiteFor$TestRemainderBy1025 (junit.framework.TestSuite overallTestSuite$)1026 {1027 junit.framework.TestSuite methodTests$1028 = this.emptyTestSuiteFor("remainderBy");1029 try {1030 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1031 receivers$iter1032 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1033 (this.vorg_jmlspecs_models_JMLCharIter("remainderBy", 1));1034 this.check_has_data1035 (receivers$iter,1036 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"remainderBy\", 1))");1037 while (!receivers$iter.atEnd()) {1038 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1039 vorg_jmlspecs_models_JMLChar$1$iter1040 = this.vorg_jmlspecs_models_JMLCharIter("remainderBy", 0);1041 this.check_has_data1042 (vorg_jmlspecs_models_JMLChar$1$iter,1043 "this.vorg_jmlspecs_models_JMLCharIter(\"remainderBy\", 0)");1044 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {1045 final org.jmlspecs.models.JMLChar receiver$1046 = (org.jmlspecs.models.JMLChar) receivers$iter.get();1047 final org.jmlspecs.models.JMLChar i21048 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();1049 methodTests$.addTest1050 (new TestRemainderBy(receiver$, i2));1051 vorg_jmlspecs_models_JMLChar$1$iter.advance();1052 }1053 receivers$iter.advance();1054 }1055 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1056 // methodTests$ doesn't want more tests1057 }1058 overallTestSuite$.addTest(methodTests$);1059 }1060 /** Test for the remainderBy method. */1061 protected static class TestRemainderBy extends OneTest {1062 /** The receiver */1063 private org.jmlspecs.models.JMLChar receiver$;1064 /** Argument i2 */1065 private org.jmlspecs.models.JMLChar i2;1066 /** Initialize this instance. */1067 public TestRemainderBy(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1068 super("remainderBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1069 this.receiver$ = receiver$;1070 this.i2 = i2;1071 }1072 protected void doCall() throws java.lang.Throwable {1073 receiver$.remainderBy(i2);1074 }1075 protected java.lang.String failMessage1076 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1077 {1078 java.lang.String msg = "\n\tMethod 'remainderBy' applied to";1079 msg += "\n\tReceiver: " + this.receiver$;1080 msg += "\n\tArgument i2: " + this.i2;1081 return msg;1082 }1083 }1084 /** Add tests for the greaterThan method1085 * to the overall test suite. */1086 private void addTestSuiteFor$TestGreaterThan1087 (junit.framework.TestSuite overallTestSuite$)1088 {1089 junit.framework.TestSuite methodTests$1090 = this.emptyTestSuiteFor("greaterThan");1091 try {1092 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1093 receivers$iter1094 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1095 (this.vorg_jmlspecs_models_JMLCharIter("greaterThan", 1));1096 this.check_has_data1097 (receivers$iter,1098 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"greaterThan\", 1))");1099 while (!receivers$iter.atEnd()) {1100 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1101 vorg_jmlspecs_models_JMLChar$1$iter1102 = this.vorg_jmlspecs_models_JMLCharIter("greaterThan", 0);1103 this.check_has_data1104 (vorg_jmlspecs_models_JMLChar$1$iter,1105 "this.vorg_jmlspecs_models_JMLCharIter(\"greaterThan\", 0)");1106 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {1107 final org.jmlspecs.models.JMLChar receiver$1108 = (org.jmlspecs.models.JMLChar) receivers$iter.get();1109 final org.jmlspecs.models.JMLChar i21110 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();1111 methodTests$.addTest1112 (new TestGreaterThan(receiver$, i2));1113 vorg_jmlspecs_models_JMLChar$1$iter.advance();1114 }1115 receivers$iter.advance();1116 }1117 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1118 // methodTests$ doesn't want more tests1119 }1120 overallTestSuite$.addTest(methodTests$);1121 }1122 /** Test for the greaterThan method. */1123 protected static class TestGreaterThan extends OneTest {1124 /** The receiver */1125 private org.jmlspecs.models.JMLChar receiver$;1126 /** Argument i2 */1127 private org.jmlspecs.models.JMLChar i2;1128 /** Initialize this instance. */1129 public TestGreaterThan(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1130 super("greaterThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1131 this.receiver$ = receiver$;1132 this.i2 = i2;1133 }1134 protected void doCall() throws java.lang.Throwable {1135 receiver$.greaterThan(i2);1136 }1137 protected java.lang.String failMessage1138 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1139 {1140 java.lang.String msg = "\n\tMethod 'greaterThan' applied to";1141 msg += "\n\tReceiver: " + this.receiver$;1142 msg += "\n\tArgument i2: " + this.i2;1143 return msg;1144 }1145 }1146 /** Add tests for the lessThan method1147 * to the overall test suite. */1148 private void addTestSuiteFor$TestLessThan1149 (junit.framework.TestSuite overallTestSuite$)1150 {1151 junit.framework.TestSuite methodTests$1152 = this.emptyTestSuiteFor("lessThan");1153 try {1154 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1155 receivers$iter1156 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1157 (this.vorg_jmlspecs_models_JMLCharIter("lessThan", 1));1158 this.check_has_data1159 (receivers$iter,1160 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"lessThan\", 1))");1161 while (!receivers$iter.atEnd()) {1162 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1163 vorg_jmlspecs_models_JMLChar$1$iter1164 = this.vorg_jmlspecs_models_JMLCharIter("lessThan", 0);1165 this.check_has_data1166 (vorg_jmlspecs_models_JMLChar$1$iter,1167 "this.vorg_jmlspecs_models_JMLCharIter(\"lessThan\", 0)");1168 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {1169 final org.jmlspecs.models.JMLChar receiver$1170 = (org.jmlspecs.models.JMLChar) receivers$iter.get();1171 final org.jmlspecs.models.JMLChar i21172 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();1173 methodTests$.addTest1174 (new TestLessThan(receiver$, i2));1175 vorg_jmlspecs_models_JMLChar$1$iter.advance();1176 }1177 receivers$iter.advance();1178 }1179 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1180 // methodTests$ doesn't want more tests1181 }1182 overallTestSuite$.addTest(methodTests$);1183 }1184 /** Test for the lessThan method. */1185 protected static class TestLessThan extends OneTest {1186 /** The receiver */1187 private org.jmlspecs.models.JMLChar receiver$;1188 /** Argument i2 */1189 private org.jmlspecs.models.JMLChar i2;1190 /** Initialize this instance. */1191 public TestLessThan(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1192 super("lessThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1193 this.receiver$ = receiver$;1194 this.i2 = i2;1195 }1196 protected void doCall() throws java.lang.Throwable {1197 receiver$.lessThan(i2);1198 }1199 protected java.lang.String failMessage1200 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1201 {1202 java.lang.String msg = "\n\tMethod 'lessThan' applied to";1203 msg += "\n\tReceiver: " + this.receiver$;1204 msg += "\n\tArgument i2: " + this.i2;1205 return msg;1206 }1207 }1208 /** Add tests for the greaterThanOrEqualTo method1209 * to the overall test suite. */1210 private void addTestSuiteFor$TestGreaterThanOrEqualTo1211 (junit.framework.TestSuite overallTestSuite$)1212 {1213 junit.framework.TestSuite methodTests$1214 = this.emptyTestSuiteFor("greaterThanOrEqualTo");1215 try {1216 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1217 receivers$iter1218 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1219 (this.vorg_jmlspecs_models_JMLCharIter("greaterThanOrEqualTo", 1));1220 this.check_has_data1221 (receivers$iter,1222 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"greaterThanOrEqualTo\", 1))");1223 while (!receivers$iter.atEnd()) {1224 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1225 vorg_jmlspecs_models_JMLChar$1$iter1226 = this.vorg_jmlspecs_models_JMLCharIter("greaterThanOrEqualTo", 0);1227 this.check_has_data1228 (vorg_jmlspecs_models_JMLChar$1$iter,1229 "this.vorg_jmlspecs_models_JMLCharIter(\"greaterThanOrEqualTo\", 0)");1230 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {1231 final org.jmlspecs.models.JMLChar receiver$1232 = (org.jmlspecs.models.JMLChar) receivers$iter.get();1233 final org.jmlspecs.models.JMLChar i21234 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();1235 methodTests$.addTest1236 (new TestGreaterThanOrEqualTo(receiver$, i2));1237 vorg_jmlspecs_models_JMLChar$1$iter.advance();1238 }1239 receivers$iter.advance();1240 }1241 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1242 // methodTests$ doesn't want more tests1243 }1244 overallTestSuite$.addTest(methodTests$);1245 }1246 /** Test for the greaterThanOrEqualTo method. */1247 protected static class TestGreaterThanOrEqualTo extends OneTest {1248 /** The receiver */1249 private org.jmlspecs.models.JMLChar receiver$;1250 /** Argument i2 */1251 private org.jmlspecs.models.JMLChar i2;1252 /** Initialize this instance. */1253 public TestGreaterThanOrEqualTo(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1254 super("greaterThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1255 this.receiver$ = receiver$;1256 this.i2 = i2;1257 }1258 protected void doCall() throws java.lang.Throwable {1259 receiver$.greaterThanOrEqualTo(i2);1260 }1261 protected java.lang.String failMessage1262 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)1263 {1264 java.lang.String msg = "\n\tMethod 'greaterThanOrEqualTo' applied to";1265 msg += "\n\tReceiver: " + this.receiver$;1266 msg += "\n\tArgument i2: " + this.i2;1267 return msg;1268 }1269 }1270 /** Add tests for the lessThanOrEqualTo method1271 * to the overall test suite. */1272 private void addTestSuiteFor$TestLessThanOrEqualTo1273 (junit.framework.TestSuite overallTestSuite$)1274 {1275 junit.framework.TestSuite methodTests$1276 = this.emptyTestSuiteFor("lessThanOrEqualTo");1277 try {1278 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1279 receivers$iter1280 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator1281 (this.vorg_jmlspecs_models_JMLCharIter("lessThanOrEqualTo", 1));1282 this.check_has_data1283 (receivers$iter,1284 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"lessThanOrEqualTo\", 1))");1285 while (!receivers$iter.atEnd()) {1286 org.jmlspecs.jmlunit.strategies.IndefiniteIterator1287 vorg_jmlspecs_models_JMLChar$1$iter1288 = this.vorg_jmlspecs_models_JMLCharIter("lessThanOrEqualTo", 0);1289 this.check_has_data1290 (vorg_jmlspecs_models_JMLChar$1$iter,1291 "this.vorg_jmlspecs_models_JMLCharIter(\"lessThanOrEqualTo\", 0)");1292 while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) {1293 final org.jmlspecs.models.JMLChar receiver$1294 = (org.jmlspecs.models.JMLChar) receivers$iter.get();1295 final org.jmlspecs.models.JMLChar i21296 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get();1297 methodTests$.addTest1298 (new TestLessThanOrEqualTo(receiver$, i2));1299 vorg_jmlspecs_models_JMLChar$1$iter.advance();1300 }1301 receivers$iter.advance();1302 }1303 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {1304 // methodTests$ doesn't want more tests1305 }1306 overallTestSuite$.addTest(methodTests$);1307 }1308 /** Test for the lessThanOrEqualTo method. */1309 protected static class TestLessThanOrEqualTo extends OneTest {1310 /** The receiver */1311 private org.jmlspecs.models.JMLChar receiver$;1312 /** Argument i2 */1313 private org.jmlspecs.models.JMLChar i2;1314 /** Initialize this instance. */1315 public TestLessThanOrEqualTo(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) {1316 super("lessThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}"));1317 this.receiver$ = receiver$;1318 this.i2 = i2;...

Full Screen

Full Screen

Source:JMLString_JML_Test.java Github

copy

Full Screen

...15 /** Initialize this class. */16 public JMLString_JML_Test(java.lang.String name) {17 super(name);18 }19 /** Run the tests. */20 public static void main(java.lang.String[] args) {21 org.jmlspecs.jmlunit.JMLTestRunner.run(suite());22 // You can also use a JUnit test runner such as:23 // junit.textui.TestRunner.run(suite());24 }25 /** Test to see if the code for class JMLString26 * has been compiled with runtime assertion checking (i.e., by jmlc).27 * Code that is not compiled with jmlc would not make an effective test,28 * since no assertion checking would be done. */29 public void test$IsRACCompiled() {30 junit.framework.Assert.assertTrue("code for class JMLString"31 + " was not compiled with jmlc"32 + " so no assertions will be checked!",33 org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLString.class)34 );35 }36 /** Return the test suite for this test class. This will have37 * added to it at least test$IsRACCompiled(), and any test methods38 * written explicitly by the user in the superclass. It will also39 * have added test suites for each testing each method and40 * constructor.41 */42 //@ ensures \result != null;43 public static junit.framework.Test suite() {44 JMLString_JML_Test testobj45 = new JMLString_JML_Test("JMLString_JML_Test");46 junit.framework.TestSuite testsuite = testobj.overallTestSuite();47 // Add instances of Test found by the reflection mechanism.48 testsuite.addTestSuite(JMLString_JML_Test.class);49 testobj.addTestSuiteForEachMethod(testsuite);50 return testsuite;51 }52 /** A JUnit test object that can run a single test method. This53 * is defined as a nested class solely for convenience; it can't54 * be defined once and for all because it must subclass its55 * enclosing class.56 */57 protected static abstract class OneTest extends JMLString_JML_Test {58 /** Initialize this test object. */59 public OneTest(String name) {60 super(name);61 }62 /** The result object that holds information about testing. */63 protected junit.framework.TestResult result;64 //@ also65 //@ requires result != null;66 public void run(junit.framework.TestResult result) {67 this.result = result;68 super.run(result);69 }70 /* Run a single test and decide whether the test was71 * successful, meaningless, or a failure. This is the72 * Template Method pattern abstraction of the inner loop in a73 * JML/JUnit test. */74 public void runTest() throws java.lang.Throwable {75 try {76 // The call being tested!77 doCall();78 }79 catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) {80 // meaningless test input81 addMeaningless();82 } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) {83 // test failure84 int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel();85 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel86 (org.jmlspecs.jmlrac.runtime.JMLOption.NONE);87 try {88 java.lang.String failmsg = this.failMessage(e);89 junit.framework.AssertionFailedError err90 = new junit.framework.AssertionFailedError(failmsg);91 err.setStackTrace(new java.lang.StackTraceElement[]{});92 err.initCause(e);93 result.addFailure(this, err);94 } finally {95 org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l);96 }97 } catch (java.lang.Throwable e) {98 // test success99 }100 }101 /** Call the method to be tested with the appropriate arguments. */102 protected abstract void doCall() throws java.lang.Throwable;103 /** Format the error message for a test failure, based on the104 * method's arguments. */105 protected abstract java.lang.String failMessage106 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e);107 /** Inform listeners that a meaningless test was run. */108 private void addMeaningless() {109 if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) {110 ((org.jmlspecs.jmlunit.JMLTestResult)result)111 .addMeaningless(this);112 }113 }114 }115 /** Create the tests that are to be run for testing the class116 * JMLString. The framework will then run them.117 * @param overallTestSuite$ The suite accumulating all of the tests118 * for this driver class.119 */120 //@ requires overallTestSuite$ != null;121 public void addTestSuiteForEachMethod122 (junit.framework.TestSuite overallTestSuite$)123 {124 try {125 this.addTestSuiteFor$TestJMLString(overallTestSuite$);126 } catch (java.lang.Throwable ex) {127 overallTestSuite$.addTest128 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));129 }130 try {131 this.addTestSuiteFor$TestJMLString$1(overallTestSuite$);132 } catch (java.lang.Throwable ex) {133 overallTestSuite$.addTest134 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));135 }136 try {137 this.addTestSuiteFor$TestClone(overallTestSuite$);138 } catch (java.lang.Throwable ex) {139 overallTestSuite$.addTest140 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));141 }142 try {143 this.addTestSuiteFor$TestCompareTo(overallTestSuite$);144 } catch (java.lang.Throwable ex) {145 overallTestSuite$.addTest146 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));147 }148 try {149 this.addTestSuiteFor$TestCompareTo$1(overallTestSuite$);150 } catch (java.lang.Throwable ex) {151 overallTestSuite$.addTest152 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));153 }154 try {155 this.addTestSuiteFor$TestEquals(overallTestSuite$);156 } catch (java.lang.Throwable ex) {157 overallTestSuite$.addTest158 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));159 }160 try {161 this.addTestSuiteFor$TestEqualsIgnoreCase(overallTestSuite$);162 } catch (java.lang.Throwable ex) {163 overallTestSuite$.addTest164 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));165 }166 try {167 this.addTestSuiteFor$TestEqualsIgnoreCase$1(overallTestSuite$);168 } catch (java.lang.Throwable ex) {169 overallTestSuite$.addTest170 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));171 }172 try {173 this.addTestSuiteFor$TestHashCode(overallTestSuite$);174 } catch (java.lang.Throwable ex) {175 overallTestSuite$.addTest176 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));177 }178 try {179 this.addTestSuiteFor$TestToString(overallTestSuite$);180 } catch (java.lang.Throwable ex) {181 overallTestSuite$.addTest182 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));183 }184 try {185 this.addTestSuiteFor$TestConcat(overallTestSuite$);186 } catch (java.lang.Throwable ex) {187 overallTestSuite$.addTest188 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));189 }190 try {191 this.addTestSuiteFor$TestConcat$1(overallTestSuite$);192 } catch (java.lang.Throwable ex) {193 overallTestSuite$.addTest194 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));195 }196 try {197 this.addTestSuiteFor$TestConcat$2(overallTestSuite$);198 } catch (java.lang.Throwable ex) {199 overallTestSuite$.addTest200 (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex));201 }202 }203 /** Add tests for the JMLString contructor204 * to the overall test suite. */205 private void addTestSuiteFor$TestJMLString206 (junit.framework.TestSuite overallTestSuite$)207 {208 junit.framework.TestSuite methodTests$209 = this.emptyTestSuiteFor("JMLString");210 try {211 methodTests$.addTest212 (new TestJMLString());213 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {214 // methodTests$ doesn't want more tests215 }216 overallTestSuite$.addTest(methodTests$);217 }218 /** Test for the JMLString contructor. */219 protected static class TestJMLString extends OneTest {220 /** Initialize this instance. */221 public TestJMLString() {222 super("JMLString");223 }224 protected void doCall() throws java.lang.Throwable {225 new JMLString();226 }227 protected java.lang.String failMessage228 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)229 {230 java.lang.String msg = "\n\tContructor 'JMLString'";231 return msg;232 }233 }234 /** Add tests for the JMLString contructor235 * to the overall test suite. */236 private void addTestSuiteFor$TestJMLString$1237 (junit.framework.TestSuite overallTestSuite$)238 {239 junit.framework.TestSuite methodTests$240 = this.emptyTestSuiteFor("JMLString");241 try {242 org.jmlspecs.jmlunit.strategies.IndefiniteIterator243 vjava_lang_String$1$iter244 = this.vjava_lang_StringIter("JMLString", 0);245 this.check_has_data246 (vjava_lang_String$1$iter,247 "this.vjava_lang_StringIter(\"JMLString\", 0)");248 while (!vjava_lang_String$1$iter.atEnd()) {249 final java.lang.String s250 = (java.lang.String) vjava_lang_String$1$iter.get();251 methodTests$.addTest252 (new TestJMLString$1(s));253 vjava_lang_String$1$iter.advance();254 }255 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {256 // methodTests$ doesn't want more tests257 }258 overallTestSuite$.addTest(methodTests$);259 }260 /** Test for the JMLString contructor. */261 protected static class TestJMLString$1 extends OneTest {262 /** Argument s */263 private java.lang.String s;264 /** Initialize this instance. */265 public TestJMLString$1(java.lang.String s) {266 super("JMLString"+ ":" + (s==null? "null" :("\""+s+"\"")));267 this.s = s;268 }269 protected void doCall() throws java.lang.Throwable {270 new JMLString(s);271 }272 protected java.lang.String failMessage273 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)274 {275 java.lang.String msg = "\n\tContructor 'JMLString' applied to";276 msg += "\n\tArgument s: " + this.s;277 return msg;278 }279 }280 /** Add tests for the clone method281 * to the overall test suite. */282 private void addTestSuiteFor$TestClone283 (junit.framework.TestSuite overallTestSuite$)284 {285 junit.framework.TestSuite methodTests$286 = this.emptyTestSuiteFor("clone");287 try {288 org.jmlspecs.jmlunit.strategies.IndefiniteIterator289 receivers$iter290 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator291 (this.vorg_jmlspecs_models_JMLStringIter("clone", 0));292 this.check_has_data293 (receivers$iter,294 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"clone\", 0))");295 while (!receivers$iter.atEnd()) {296 final org.jmlspecs.models.JMLString receiver$297 = (org.jmlspecs.models.JMLString) receivers$iter.get();298 methodTests$.addTest299 (new TestClone(receiver$));300 receivers$iter.advance();301 }302 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {303 // methodTests$ doesn't want more tests304 }305 overallTestSuite$.addTest(methodTests$);306 }307 /** Test for the clone method. */308 protected static class TestClone extends OneTest {309 /** The receiver */310 private org.jmlspecs.models.JMLString receiver$;311 /** Initialize this instance. */312 public TestClone(org.jmlspecs.models.JMLString receiver$) {313 super("clone");314 this.receiver$ = receiver$;315 }316 protected void doCall() throws java.lang.Throwable {317 receiver$.clone();318 }319 protected java.lang.String failMessage320 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)321 {322 java.lang.String msg = "\n\tMethod 'clone' applied to";323 msg += "\n\tReceiver: " + this.receiver$;324 return msg;325 }326 }327 /** Add tests for the compareTo method328 * to the overall test suite. */329 private void addTestSuiteFor$TestCompareTo330 (junit.framework.TestSuite overallTestSuite$)331 {332 junit.framework.TestSuite methodTests$333 = this.emptyTestSuiteFor("compareTo");334 try {335 org.jmlspecs.jmlunit.strategies.IndefiniteIterator336 receivers$iter337 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator338 (this.vorg_jmlspecs_models_JMLStringIter("compareTo", 1));339 this.check_has_data340 (receivers$iter,341 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"compareTo\", 1))");342 while (!receivers$iter.atEnd()) {343 org.jmlspecs.jmlunit.strategies.IndefiniteIterator344 vjava_lang_Object$1$iter345 = this.vjava_lang_ObjectIter("compareTo", 0);346 this.check_has_data347 (vjava_lang_Object$1$iter,348 "this.vjava_lang_ObjectIter(\"compareTo\", 0)");349 while (!vjava_lang_Object$1$iter.atEnd()) {350 final org.jmlspecs.models.JMLString receiver$351 = (org.jmlspecs.models.JMLString) receivers$iter.get();352 final java.lang.Object op2353 = (java.lang.Object) vjava_lang_Object$1$iter.get();354 methodTests$.addTest355 (new TestCompareTo(receiver$, op2));356 vjava_lang_Object$1$iter.advance();357 }358 receivers$iter.advance();359 }360 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {361 // methodTests$ doesn't want more tests362 }363 overallTestSuite$.addTest(methodTests$);364 }365 /** Test for the compareTo method. */366 protected static class TestCompareTo extends OneTest {367 /** The receiver */368 private org.jmlspecs.models.JMLString receiver$;369 /** Argument op2 */370 private java.lang.Object op2;371 /** Initialize this instance. */372 public TestCompareTo(org.jmlspecs.models.JMLString receiver$, java.lang.Object op2) {373 super("compareTo"+ ":" + (op2==null? "null" :"{java.lang.Object}"));374 this.receiver$ = receiver$;375 this.op2 = op2;376 }377 protected void doCall() throws java.lang.Throwable {378 receiver$.compareTo(op2);379 }380 protected java.lang.String failMessage381 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)382 {383 java.lang.String msg = "\n\tMethod 'compareTo' applied to";384 msg += "\n\tReceiver: " + this.receiver$;385 msg += "\n\tArgument op2: " + this.op2;386 return msg;387 }388 }389 /** Add tests for the compareTo method390 * to the overall test suite. */391 private void addTestSuiteFor$TestCompareTo$1392 (junit.framework.TestSuite overallTestSuite$)393 {394 junit.framework.TestSuite methodTests$395 = this.emptyTestSuiteFor("compareTo");396 try {397 org.jmlspecs.jmlunit.strategies.IndefiniteIterator398 receivers$iter399 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator400 (this.vorg_jmlspecs_models_JMLStringIter("compareTo", 1));401 this.check_has_data402 (receivers$iter,403 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"compareTo\", 1))");404 while (!receivers$iter.atEnd()) {405 org.jmlspecs.jmlunit.strategies.IndefiniteIterator406 vorg_jmlspecs_models_JMLString$1$iter407 = this.vorg_jmlspecs_models_JMLStringIter("compareTo", 0);408 this.check_has_data409 (vorg_jmlspecs_models_JMLString$1$iter,410 "this.vorg_jmlspecs_models_JMLStringIter(\"compareTo\", 0)");411 while (!vorg_jmlspecs_models_JMLString$1$iter.atEnd()) {412 final org.jmlspecs.models.JMLString receiver$413 = (org.jmlspecs.models.JMLString) receivers$iter.get();414 final org.jmlspecs.models.JMLString another415 = (org.jmlspecs.models.JMLString) vorg_jmlspecs_models_JMLString$1$iter.get();416 methodTests$.addTest417 (new TestCompareTo$1(receiver$, another));418 vorg_jmlspecs_models_JMLString$1$iter.advance();419 }420 receivers$iter.advance();421 }422 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {423 // methodTests$ doesn't want more tests424 }425 overallTestSuite$.addTest(methodTests$);426 }427 /** Test for the compareTo method. */428 protected static class TestCompareTo$1 extends OneTest {429 /** The receiver */430 private org.jmlspecs.models.JMLString receiver$;431 /** Argument another */432 private org.jmlspecs.models.JMLString another;433 /** Initialize this instance. */434 public TestCompareTo$1(org.jmlspecs.models.JMLString receiver$, org.jmlspecs.models.JMLString another) {435 super("compareTo"+ ":" + (another==null? "null" :"{org.jmlspecs.models.JMLString}"));436 this.receiver$ = receiver$;437 this.another = another;438 }439 protected void doCall() throws java.lang.Throwable {440 receiver$.compareTo(another);441 }442 protected java.lang.String failMessage443 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)444 {445 java.lang.String msg = "\n\tMethod 'compareTo' applied to";446 msg += "\n\tReceiver: " + this.receiver$;447 msg += "\n\tArgument another: " + this.another;448 return msg;449 }450 }451 /** Add tests for the equals method452 * to the overall test suite. */453 private void addTestSuiteFor$TestEquals454 (junit.framework.TestSuite overallTestSuite$)455 {456 junit.framework.TestSuite methodTests$457 = this.emptyTestSuiteFor("equals");458 try {459 org.jmlspecs.jmlunit.strategies.IndefiniteIterator460 receivers$iter461 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator462 (this.vorg_jmlspecs_models_JMLStringIter("equals", 1));463 this.check_has_data464 (receivers$iter,465 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"equals\", 1))");466 while (!receivers$iter.atEnd()) {467 org.jmlspecs.jmlunit.strategies.IndefiniteIterator468 vjava_lang_Object$1$iter469 = this.vjava_lang_ObjectIter("equals", 0);470 this.check_has_data471 (vjava_lang_Object$1$iter,472 "this.vjava_lang_ObjectIter(\"equals\", 0)");473 while (!vjava_lang_Object$1$iter.atEnd()) {474 final org.jmlspecs.models.JMLString receiver$475 = (org.jmlspecs.models.JMLString) receivers$iter.get();476 final java.lang.Object s477 = (java.lang.Object) vjava_lang_Object$1$iter.get();478 methodTests$.addTest479 (new TestEquals(receiver$, s));480 vjava_lang_Object$1$iter.advance();481 }482 receivers$iter.advance();483 }484 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {485 // methodTests$ doesn't want more tests486 }487 overallTestSuite$.addTest(methodTests$);488 }489 /** Test for the equals method. */490 protected static class TestEquals extends OneTest {491 /** The receiver */492 private org.jmlspecs.models.JMLString receiver$;493 /** Argument s */494 private java.lang.Object s;495 /** Initialize this instance. */496 public TestEquals(org.jmlspecs.models.JMLString receiver$, java.lang.Object s) {497 super("equals"+ ":" + (s==null? "null" :"{java.lang.Object}"));498 this.receiver$ = receiver$;499 this.s = s;500 }501 protected void doCall() throws java.lang.Throwable {502 receiver$.equals(s);503 }504 protected java.lang.String failMessage505 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)506 {507 java.lang.String msg = "\n\tMethod 'equals' applied to";508 msg += "\n\tReceiver: " + this.receiver$;509 msg += "\n\tArgument s: " + this.s;510 return msg;511 }512 }513 /** Add tests for the equalsIgnoreCase method514 * to the overall test suite. */515 private void addTestSuiteFor$TestEqualsIgnoreCase516 (junit.framework.TestSuite overallTestSuite$)517 {518 junit.framework.TestSuite methodTests$519 = this.emptyTestSuiteFor("equalsIgnoreCase");520 try {521 org.jmlspecs.jmlunit.strategies.IndefiniteIterator522 receivers$iter523 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator524 (this.vorg_jmlspecs_models_JMLStringIter("equalsIgnoreCase", 1));525 this.check_has_data526 (receivers$iter,527 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"equalsIgnoreCase\", 1))");528 while (!receivers$iter.atEnd()) {529 org.jmlspecs.jmlunit.strategies.IndefiniteIterator530 vorg_jmlspecs_models_JMLString$1$iter531 = this.vorg_jmlspecs_models_JMLStringIter("equalsIgnoreCase", 0);532 this.check_has_data533 (vorg_jmlspecs_models_JMLString$1$iter,534 "this.vorg_jmlspecs_models_JMLStringIter(\"equalsIgnoreCase\", 0)");535 while (!vorg_jmlspecs_models_JMLString$1$iter.atEnd()) {536 final org.jmlspecs.models.JMLString receiver$537 = (org.jmlspecs.models.JMLString) receivers$iter.get();538 final org.jmlspecs.models.JMLString another539 = (org.jmlspecs.models.JMLString) vorg_jmlspecs_models_JMLString$1$iter.get();540 methodTests$.addTest541 (new TestEqualsIgnoreCase(receiver$, another));542 vorg_jmlspecs_models_JMLString$1$iter.advance();543 }544 receivers$iter.advance();545 }546 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {547 // methodTests$ doesn't want more tests548 }549 overallTestSuite$.addTest(methodTests$);550 }551 /** Test for the equalsIgnoreCase method. */552 protected static class TestEqualsIgnoreCase extends OneTest {553 /** The receiver */554 private org.jmlspecs.models.JMLString receiver$;555 /** Argument another */556 private org.jmlspecs.models.JMLString another;557 /** Initialize this instance. */558 public TestEqualsIgnoreCase(org.jmlspecs.models.JMLString receiver$, org.jmlspecs.models.JMLString another) {559 super("equalsIgnoreCase"+ ":" + (another==null? "null" :"{org.jmlspecs.models.JMLString}"));560 this.receiver$ = receiver$;561 this.another = another;562 }563 protected void doCall() throws java.lang.Throwable {564 receiver$.equalsIgnoreCase(another);565 }566 protected java.lang.String failMessage567 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)568 {569 java.lang.String msg = "\n\tMethod 'equalsIgnoreCase' applied to";570 msg += "\n\tReceiver: " + this.receiver$;571 msg += "\n\tArgument another: " + this.another;572 return msg;573 }574 }575 /** Add tests for the equalsIgnoreCase method576 * to the overall test suite. */577 private void addTestSuiteFor$TestEqualsIgnoreCase$1578 (junit.framework.TestSuite overallTestSuite$)579 {580 junit.framework.TestSuite methodTests$581 = this.emptyTestSuiteFor("equalsIgnoreCase");582 try {583 org.jmlspecs.jmlunit.strategies.IndefiniteIterator584 receivers$iter585 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator586 (this.vorg_jmlspecs_models_JMLStringIter("equalsIgnoreCase", 1));587 this.check_has_data588 (receivers$iter,589 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"equalsIgnoreCase\", 1))");590 while (!receivers$iter.atEnd()) {591 org.jmlspecs.jmlunit.strategies.IndefiniteIterator592 vjava_lang_String$1$iter593 = this.vjava_lang_StringIter("equalsIgnoreCase", 0);594 this.check_has_data595 (vjava_lang_String$1$iter,596 "this.vjava_lang_StringIter(\"equalsIgnoreCase\", 0)");597 while (!vjava_lang_String$1$iter.atEnd()) {598 final org.jmlspecs.models.JMLString receiver$599 = (org.jmlspecs.models.JMLString) receivers$iter.get();600 final java.lang.String another601 = (java.lang.String) vjava_lang_String$1$iter.get();602 methodTests$.addTest603 (new TestEqualsIgnoreCase$1(receiver$, another));604 vjava_lang_String$1$iter.advance();605 }606 receivers$iter.advance();607 }608 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {609 // methodTests$ doesn't want more tests610 }611 overallTestSuite$.addTest(methodTests$);612 }613 /** Test for the equalsIgnoreCase method. */614 protected static class TestEqualsIgnoreCase$1 extends OneTest {615 /** The receiver */616 private org.jmlspecs.models.JMLString receiver$;617 /** Argument another */618 private java.lang.String another;619 /** Initialize this instance. */620 public TestEqualsIgnoreCase$1(org.jmlspecs.models.JMLString receiver$, java.lang.String another) {621 super("equalsIgnoreCase"+ ":" + (another==null? "null" :("\""+another+"\"")));622 this.receiver$ = receiver$;623 this.another = another;624 }625 protected void doCall() throws java.lang.Throwable {626 receiver$.equalsIgnoreCase(another);627 }628 protected java.lang.String failMessage629 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)630 {631 java.lang.String msg = "\n\tMethod 'equalsIgnoreCase' applied to";632 msg += "\n\tReceiver: " + this.receiver$;633 msg += "\n\tArgument another: " + this.another;634 return msg;635 }636 }637 /** Add tests for the hashCode method638 * to the overall test suite. */639 private void addTestSuiteFor$TestHashCode640 (junit.framework.TestSuite overallTestSuite$)641 {642 junit.framework.TestSuite methodTests$643 = this.emptyTestSuiteFor("hashCode");644 try {645 org.jmlspecs.jmlunit.strategies.IndefiniteIterator646 receivers$iter647 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator648 (this.vorg_jmlspecs_models_JMLStringIter("hashCode", 0));649 this.check_has_data650 (receivers$iter,651 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"hashCode\", 0))");652 while (!receivers$iter.atEnd()) {653 final org.jmlspecs.models.JMLString receiver$654 = (org.jmlspecs.models.JMLString) receivers$iter.get();655 methodTests$.addTest656 (new TestHashCode(receiver$));657 receivers$iter.advance();658 }659 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {660 // methodTests$ doesn't want more tests661 }662 overallTestSuite$.addTest(methodTests$);663 }664 /** Test for the hashCode method. */665 protected static class TestHashCode extends OneTest {666 /** The receiver */667 private org.jmlspecs.models.JMLString receiver$;668 /** Initialize this instance. */669 public TestHashCode(org.jmlspecs.models.JMLString receiver$) {670 super("hashCode");671 this.receiver$ = receiver$;672 }673 protected void doCall() throws java.lang.Throwable {674 receiver$.hashCode();675 }676 protected java.lang.String failMessage677 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)678 {679 java.lang.String msg = "\n\tMethod 'hashCode' applied to";680 msg += "\n\tReceiver: " + this.receiver$;681 return msg;682 }683 }684 /** Add tests for the toString method685 * to the overall test suite. */686 private void addTestSuiteFor$TestToString687 (junit.framework.TestSuite overallTestSuite$)688 {689 junit.framework.TestSuite methodTests$690 = this.emptyTestSuiteFor("toString");691 try {692 org.jmlspecs.jmlunit.strategies.IndefiniteIterator693 receivers$iter694 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator695 (this.vorg_jmlspecs_models_JMLStringIter("toString", 0));696 this.check_has_data697 (receivers$iter,698 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"toString\", 0))");699 while (!receivers$iter.atEnd()) {700 final org.jmlspecs.models.JMLString receiver$701 = (org.jmlspecs.models.JMLString) receivers$iter.get();702 methodTests$.addTest703 (new TestToString(receiver$));704 receivers$iter.advance();705 }706 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {707 // methodTests$ doesn't want more tests708 }709 overallTestSuite$.addTest(methodTests$);710 }711 /** Test for the toString method. */712 protected static class TestToString extends OneTest {713 /** The receiver */714 private org.jmlspecs.models.JMLString receiver$;715 /** Initialize this instance. */716 public TestToString(org.jmlspecs.models.JMLString receiver$) {717 super("toString");718 this.receiver$ = receiver$;719 }720 protected void doCall() throws java.lang.Throwable {721 receiver$.toString();722 }723 protected java.lang.String failMessage724 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)725 {726 java.lang.String msg = "\n\tMethod 'toString' applied to";727 msg += "\n\tReceiver: " + this.receiver$;728 return msg;729 }730 }731 /** Add tests for the concat method732 * to the overall test suite. */733 private void addTestSuiteFor$TestConcat734 (junit.framework.TestSuite overallTestSuite$)735 {736 junit.framework.TestSuite methodTests$737 = this.emptyTestSuiteFor("concat");738 try {739 org.jmlspecs.jmlunit.strategies.IndefiniteIterator740 receivers$iter741 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator742 (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));743 this.check_has_data744 (receivers$iter,745 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");746 while (!receivers$iter.atEnd()) {747 org.jmlspecs.jmlunit.strategies.IndefiniteIterator748 vorg_jmlspecs_models_JMLString$1$iter749 = this.vorg_jmlspecs_models_JMLStringIter("concat", 0);750 this.check_has_data751 (vorg_jmlspecs_models_JMLString$1$iter,752 "this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 0)");753 while (!vorg_jmlspecs_models_JMLString$1$iter.atEnd()) {754 final org.jmlspecs.models.JMLString receiver$755 = (org.jmlspecs.models.JMLString) receivers$iter.get();756 final org.jmlspecs.models.JMLString s757 = (org.jmlspecs.models.JMLString) vorg_jmlspecs_models_JMLString$1$iter.get();758 methodTests$.addTest759 (new TestConcat(receiver$, s));760 vorg_jmlspecs_models_JMLString$1$iter.advance();761 }762 receivers$iter.advance();763 }764 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {765 // methodTests$ doesn't want more tests766 }767 overallTestSuite$.addTest(methodTests$);768 }769 /** Test for the concat method. */770 protected static class TestConcat extends OneTest {771 /** The receiver */772 private org.jmlspecs.models.JMLString receiver$;773 /** Argument s */774 private org.jmlspecs.models.JMLString s;775 /** Initialize this instance. */776 public TestConcat(org.jmlspecs.models.JMLString receiver$, org.jmlspecs.models.JMLString s) {777 super("concat"+ ":" + (s==null? "null" :"{org.jmlspecs.models.JMLString}"));778 this.receiver$ = receiver$;779 this.s = s;780 }781 protected void doCall() throws java.lang.Throwable {782 receiver$.concat(s);783 }784 protected java.lang.String failMessage785 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)786 {787 java.lang.String msg = "\n\tMethod 'concat' applied to";788 msg += "\n\tReceiver: " + this.receiver$;789 msg += "\n\tArgument s: " + this.s;790 return msg;791 }792 }793 /** Add tests for the concat method794 * to the overall test suite. */795 private void addTestSuiteFor$TestConcat$1796 (junit.framework.TestSuite overallTestSuite$)797 {798 junit.framework.TestSuite methodTests$799 = this.emptyTestSuiteFor("concat");800 try {801 org.jmlspecs.jmlunit.strategies.IndefiniteIterator802 receivers$iter803 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator804 (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));805 this.check_has_data806 (receivers$iter,807 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");808 while (!receivers$iter.atEnd()) {809 org.jmlspecs.jmlunit.strategies.IndefiniteIterator810 vjava_lang_String$1$iter811 = this.vjava_lang_StringIter("concat", 0);812 this.check_has_data813 (vjava_lang_String$1$iter,814 "this.vjava_lang_StringIter(\"concat\", 0)");815 while (!vjava_lang_String$1$iter.atEnd()) {816 final org.jmlspecs.models.JMLString receiver$817 = (org.jmlspecs.models.JMLString) receivers$iter.get();818 final java.lang.String s819 = (java.lang.String) vjava_lang_String$1$iter.get();820 methodTests$.addTest821 (new TestConcat$1(receiver$, s));822 vjava_lang_String$1$iter.advance();823 }824 receivers$iter.advance();825 }826 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {827 // methodTests$ doesn't want more tests828 }829 overallTestSuite$.addTest(methodTests$);830 }831 /** Test for the concat method. */832 protected static class TestConcat$1 extends OneTest {833 /** The receiver */834 private org.jmlspecs.models.JMLString receiver$;835 /** Argument s */836 private java.lang.String s;837 /** Initialize this instance. */838 public TestConcat$1(org.jmlspecs.models.JMLString receiver$, java.lang.String s) {839 super("concat"+ ":" + (s==null? "null" :("\""+s+"\"")));840 this.receiver$ = receiver$;841 this.s = s;842 }843 protected void doCall() throws java.lang.Throwable {844 receiver$.concat(s);845 }846 protected java.lang.String failMessage847 (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)848 {849 java.lang.String msg = "\n\tMethod 'concat' applied to";850 msg += "\n\tReceiver: " + this.receiver$;851 msg += "\n\tArgument s: " + this.s;852 return msg;853 }854 }855 /** Add tests for the concat method856 * to the overall test suite. */857 private void addTestSuiteFor$TestConcat$2858 (junit.framework.TestSuite overallTestSuite$)859 {860 junit.framework.TestSuite methodTests$861 = this.emptyTestSuiteFor("concat");862 try {863 org.jmlspecs.jmlunit.strategies.IndefiniteIterator864 receivers$iter865 = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator866 (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));867 this.check_has_data868 (receivers$iter,869 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");870 while (!receivers$iter.atEnd()) {871 org.jmlspecs.jmlunit.strategies.CharIterator872 vchar$1$iter873 = this.vcharIter("concat", 0);874 this.check_has_data875 (vchar$1$iter,876 "this.vcharIter(\"concat\", 0)");877 while (!vchar$1$iter.atEnd()) {878 final org.jmlspecs.models.JMLString receiver$879 = (org.jmlspecs.models.JMLString) receivers$iter.get();880 final char c881 = vchar$1$iter.getChar();882 methodTests$.addTest883 (new TestConcat$2(receiver$, c));884 vchar$1$iter.advance();885 }886 receivers$iter.advance();887 }888 } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {889 // methodTests$ doesn't want more tests890 }891 overallTestSuite$.addTest(methodTests$);892 }893 /** Test for the concat method. */894 protected static class TestConcat$2 extends OneTest {895 /** The receiver */896 private org.jmlspecs.models.JMLString receiver$;897 /** Argument c */898 private char c;899 /** Initialize this instance. */900 public TestConcat$2(org.jmlspecs.models.JMLString receiver$, char c) {901 super("concat"+ ":" + "\'"+charToString(c)+"\'");902 this.receiver$ = receiver$;903 this.c = c;...

Full Screen

Full Screen

Source:AbstractTestSuite.java Github

copy

Full Screen

...31import java.lang.reflect.Modifier;32import java.util.Enumeration;33import java.util.Vector;34/**35 * Test Suite that wraps all the tests of the suite in Cactus Test Case 36 * objects so that pure JUnit tests can be run on the server side.37 *38 * @version $Id: AbstractTestSuite.java 238991 2004-05-22 11:34:50Z vmassol $39 * @since 1.540 */41public abstract class AbstractTestSuite implements Test42{43 /**44 * Lists of tests to execute (Test objects).45 */46 private Vector tests = new Vector(10);47 /**48 * Name of the current test suite.49 */50 private String name;51 52 /**53 * {@inheritDoc}54 * @see junit.framework.TestSuite#TestSuite()55 */56 public AbstractTestSuite()57 {58 }59 /**60 * {@inheritDoc}61 * @see junit.framework.TestSuite#TestSuite(Class)62 */63 public AbstractTestSuite(final Class theClass)64 {65 setName(theClass.getName());66 Constructor constructor;67 try68 {69 // Avoid generating multiple error messages70 constructor = getTestConstructor(theClass); 71 }72 catch (NoSuchMethodException e)73 {74 addTest(warning("Class " + theClass.getName()75 + " has no public constructor TestCase(String name)"));76 return;77 }78 if (!Modifier.isPublic(theClass.getModifiers()))79 {80 addTest(warning("Class " + theClass.getName() + " is not public"));81 return;82 }83 Class superClass = theClass;84 Vector names = new Vector();85 while (Test.class.isAssignableFrom(superClass))86 {87 Method[] methods = superClass.getDeclaredMethods();88 for (int i = 0; i < methods.length; i++)89 {90 addTestMethod(methods[i], names, constructor);91 }92 superClass = superClass.getSuperclass();93 }94 if (this.tests.size() == 0)95 {96 addTest(warning("No tests found in " + theClass.getName()));97 }98 }99 /**100 * {@inheritDoc}101 * @see junit.framework.TestSuite#TestSuite(String)102 */103 public AbstractTestSuite(String theName)104 {105 setName(theName);106 }107 /**108 * {@inheritDoc}109 * @see junit.framework.TestSuite#addTest(Test)110 */111 protected void addTest(Test theTest)112 {113 this.tests.addElement(theTest);114 }115 /**116 * {@inheritDoc}117 * @see junit.framework.TestSuite#addTestSuite(Class)118 */119 protected void addTestSuite(Class theTestClass)120 {121 addTest(createTestSuite(theTestClass));122 }123 /**124 * {@inheritDoc}125 * @see junit.framework.TestSuite#addTestMethod(Method, Vector, Constructor)126 */127 private void addTestMethod(Method theMethod, Vector theNames, 128 Constructor theConstructor)129 {130 String name = theMethod.getName();131 if (theNames.contains(name))132 {133 return;134 }135 if (isPublicTestMethod(theMethod))136 {137 theNames.addElement(name);138 try139 {140 // Note: We wrap the Test in a Cactus Test Case141 Object constructorInstance;142 if (theConstructor.getParameterTypes().length == 0)143 {144 constructorInstance = theConstructor.newInstance(145 new Object[0]);146 if (constructorInstance instanceof TestCase)147 {148 ((TestCase) constructorInstance).setName(name);149 }150 }151 else152 {153 constructorInstance = theConstructor.newInstance(154 new Object[] {name});155 }156 addTest(new ServletTestCase(name, (Test) constructorInstance));157 }158 catch (InstantiationException e)159 {160 addTest(warning("Cannot instantiate test case: " + name161 + " (" + exceptionToString(e) + ")"));162 }163 catch (InvocationTargetException e)164 {165 addTest(warning("Exception in constructor: " + name + " (" 166 + exceptionToString(e.getTargetException()) + ")"));167 }168 catch (IllegalAccessException e)169 {170 addTest(warning("Cannot access test case: " + name + " ("171 + exceptionToString(e) + ")"));172 }173 }174 else175 { 176 // Almost a test method177 if (isTestMethod(theMethod))178 {179 addTest(warning("Test method isn't public: " 180 + theMethod.getName()));181 }182 }183 }184 /**185 * {@inheritDoc}186 * @see junit.framework.TestSuite#exceptionToString(Throwable)187 */188 private String exceptionToString(Throwable theThrowable)189 {190 StringWriter stringWriter = new StringWriter();191 PrintWriter writer = new PrintWriter(stringWriter);192 theThrowable.printStackTrace(writer);193 return stringWriter.toString();194 }195 /**196 * {@inheritDoc}197 * @see junit.framework.TestSuite#countTestCases()198 */199 public int countTestCases()200 {201 int count = 0;202 for (Enumeration e = tests(); e.hasMoreElements();)203 {204 Test test = (Test) e.nextElement();205 count = count + test.countTestCases();206 }207 return count;208 }209 /**210 * {@inheritDoc}211 * @see junit.framework.TestSuite#isPublicTestMethod(Method)212 */213 private boolean isPublicTestMethod(Method theMethod)214 {215 return isTestMethod(theMethod) 216 && Modifier.isPublic(theMethod.getModifiers());217 }218 /**219 * {@inheritDoc}220 * @see junit.framework.TestSuite#isTestMethod(Method)221 */222 private boolean isTestMethod(Method theMethod)223 {224 String name = theMethod.getName();225 Class[] parameters = theMethod.getParameterTypes();226 Class returnType = theMethod.getReturnType();227 return parameters.length == 0228 && name.startsWith("test")229 && returnType.equals(Void.TYPE);230 }231 /**232 * {@inheritDoc}233 * @see junit.framework.TestSuite#run(TestResult)234 */235 public void run(TestResult theResult)236 {237 for (Enumeration e = tests(); e.hasMoreElements();)238 {239 if (theResult.shouldStop())240 {241 break;242 }243 Test test = (Test) e.nextElement();244 runTest(test, theResult);245 }246 }247 248 /**249 * {@inheritDoc}250 * @see junit.framework.TestSuite#runTest(Test, TestResult)251 */252 protected void runTest(Test theTest, TestResult theResult)253 {254 theTest.run(theResult);255 }256 257 /**258 * {@inheritDoc}259 * @see junit.framework.TestSuite#testAt(int)260 */261 protected Test testAt(int theIndex)262 {263 return (Test) this.tests.elementAt(theIndex);264 }265 /**266 * Gets a constructor which takes a single String as267 * its argument or a no arg constructor.268 * 269 * @param theClass the class for which to find the constructor270 * @return the valid constructor found271 * @exception NoSuchMethodException if no valid constructor is272 * found273 */274 protected static Constructor getTestConstructor(Class theClass) 275 throws NoSuchMethodException276 {277 Constructor result;278 try279 {280 result = theClass.getConstructor(new Class[] {String.class});281 }282 catch (NoSuchMethodException e)283 {284 result = theClass.getConstructor(new Class[0]);285 }286 return result; 287 }288 /**289 * {@inheritDoc}290 * @see junit.framework.TestSuite#testCount()291 */292 protected int testCount()293 {294 return this.tests.size();295 }296 /**297 * {@inheritDoc}298 * @see junit.framework.TestSuite#tests()299 */300 protected Enumeration tests()301 {302 return this.tests.elements();303 }304 /**305 * {@inheritDoc}306 * @see junit.framework.TestSuite#toString()307 */308 public String toString()309 {310 if (getName() != null)311 {312 return getName();313 }314 return super.toString();315 }316 /**317 * {@inheritDoc}318 * @see junit.framework.TestSuite#setName(String)319 */320 protected void setName(String theName)321 {322 this.name = theName;323 }324 /**325 * {@inheritDoc}326 * @see junit.framework.TestSuite#getName()327 */328 protected String getName()329 {330 return this.name;331 }332 /**333 * {@inheritDoc}334 * @see junit.framework.TestSuite#warning(String)335 */336 private static Test warning(final String theMessage)337 {338 return new TestCase("warning")339 {340 protected void runTest()341 {342 fail(theMessage);343 }344 };345 }346 /**347 * @param theTestClass the test class containing the tests to be included348 * in the Cactus Test Suite349 * @return a Cactus Test Suite (ex: ServletTestSuite) initialized with a350 * test class351 */352 protected abstract Test createTestSuite(Class theTestClass);353 /**354 * @param theName the name of the Cactus Test Case355 * @param theTest the wrapped test356 * @return a Cactus Test Case object initialized with the give name and357 * wrapped test358 */359 protected abstract Test createCactusTestCase(String theName, Test theTest);360}...

Full Screen

Full Screen

Source:AllTestsTest.java Github

copy

Full Screen

1package org.junit.tests.junit3compatibility;2import static org.hamcrest.CoreMatchers.containsString;3import static org.junit.Assert.assertEquals;4import static org.junit.Assert.assertThat;5import static org.junit.Assert.assertTrue;6import junit.framework.JUnit4TestAdapter;7import junit.framework.TestCase;8import junit.framework.TestSuite;9import org.junit.runner.JUnitCore;10import org.junit.runner.RunWith;11import org.junit.runners.AllTests;12public class AllTestsTest {13 private static boolean run;14 public static class OneTest extends TestCase {15 public void testSomething() {16 run = true;17 }18 }19 @RunWith(AllTests.class)20 public static class All {21 static public junit.framework.Test suite() {22 TestSuite suite = new TestSuite();23 suite.addTestSuite(OneTest.class);24 return suite;25 }26 }27 @org.junit.Test28 public void ensureTestIsRun() {29 JUnitCore runner = new JUnitCore();30 run = false; // Have to explicitly set run here because the runner might independently run OneTest above31 runner.run(All.class);32 assertTrue(run);33 }34 @org.junit.Test35 public void correctTestCount() throws Throwable {36 AllTests tests = new AllTests(All.class);37 assertEquals(1, tests.testCount());38 }39 @org.junit.Test40 public void someUsefulDescription() throws Throwable {41 AllTests tests = new AllTests(All.class);42 assertThat(tests.getDescription().toString(), containsString("OneTest"));43 }44 public static class JUnit4Test {45 @org.junit.Test46 public void testSomething() {47 run = true;48 }49 }50 @RunWith(AllTests.class)51 public static class AllJUnit4 {52 static public junit.framework.Test suite() {53 TestSuite suite = new TestSuite();54 suite.addTest(new JUnit4TestAdapter(JUnit4Test.class));55 return suite;56 }57 }58 @org.junit.Test59 public void correctTestCountAdapted() throws Throwable {60 AllTests tests = new AllTests(AllJUnit4.class);61 assertEquals(1, tests.testCount());62 }63 @RunWith(AllTests.class)64 public static class BadSuiteMethod {65 public static junit.framework.Test suite() {66 throw new RuntimeException("can't construct");67 }68 }69 @org.junit.Test(expected = RuntimeException.class)70 public void exceptionThrownWhenSuiteIsBad() throws Throwable {71 new AllTests(BadSuiteMethod.class);72 }73}...

Full Screen

Full Screen

Source:TestSuite.java Github

copy

Full Screen

...3 *4 * TestSuite.java5 */67package com.arjuna.wst.tests.junit;89public class TestSuite extends junit.framework.TestSuite10{11 public TestSuite()12 {13 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionParticipantTestCase.class));14 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionCoordinatorTestCase.class));15 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionWithAckParticipantTestCase.class));16 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionWithAckCoordinatorTestCase.class));17 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.PhaseZeroParticipantTestCase.class));18 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.PhaseZeroCoordinatorTestCase.class));19 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.TwoPCParticipantTestCase.class));20 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.TwoPCCoordinatorTestCase.class));21 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.OutcomeNotificationParticipantTestCase.class));22 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.OutcomeNotificationCoordinatorTestCase.class));23 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionServiceTestCase.class));24 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.CompletionWithAckServiceTestCase.class));25 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.PhaseZeroServiceTestCase.class));26 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.TwoPCServiceTestCase.class));27 addTest(new junit.framework.TestSuite(com.arjuna.wst.tests.junit.OutcomeNotificationServiceTestCase.class));28 }29} ...

Full Screen

Full Screen

Source:Str2IntTest.java Github

copy

Full Screen

1// package com.tsj.oj;23// import junit.framework.Test;4// import junit.framework.TestCase;5// import junit.framework.TestSuite;67// public class Str2IntTest extends TestCase{8// public Str2IntTest(){}9// public Str2IntTest(String name){10// super(name);11// }1213// @Override14// public void setUp(){15// }1617// @Override18// public void tearDown(){}1920// public void testValidNum(){21// String[] trueTests = new String[]{"2", "0089", "-0.1", "+3.14", "4.", "-.9", "2e10", "-90E3", "3e+7", "+6e-1", "53.5e93", "-123.456e789"};22// for(int i=0; i<trueTests.length; i++){23// System.out.println(trueTests[i]);24// assertEquals(true, Str2Int.validNum(trueTests[i]));25// }26// String[] falseTests = new String[]{"abc", "1a", "1e", "e3", "99e2.5", "--6", "-+3", "95a54e53"};27// for(int i=0; i<falseTests.length; i++){28// assertEquals(false, Str2Int.validNum(falseTests[i]));29// }30// }3132// public static Test suite(){33// TestSuite testSuite=new TestSuite("All Test From TestCaseExample");34// // 第一种方法35// // testSuite.addTestSuite(Str2IntTest.class);36// // 第二种方法37// // Test test = TestSuite.createTest(Str2IntTest.class, "testValidNum");38// // testSuite.addTest(test);39// return testSuite;40// }4142// } ...

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2public class TestRunner {3 public static void main(String[] args) {4 TestSuite suite = new TestSuite(TestJunit1.class, TestJunit2.class);5 junit.textui.TestRunner.run(suite);6 }7}8package com.tutorialspoint.junit;9import org.junit.runner.JUnitCore;10import org.junit.runner.Result;11import org.junit.runner.notification.Failure;12public class TestRunner {13 public static void main(String[] args) {14 Result result = JUnitCore.runClasses(TestJunit1.class, TestJunit2.class);15 for (Failure failure : result.getFailures()) {16 System.out.println(failure.toString());17 }18 System.out.println(result.wasSuccessful());19 }20}21package com.tutorialspoint.junit;22import org.junit.runner.JUnitCore;23import org.junit.runner.Result;24import org.junit.runner.notification.Failure;25public class TestRunner {26 public static void main(String[] args) {27 Result result = JUnitCore.runClasses(TestSuite.class);28 for (Failure failure : result.getFailures()) {29 System.out.println(failure.toString());30 }31 System.out.println(result.wasSuccessful());32 }33}34package com.tutorialspoint.junit;35import org.junit.runner.JUnitCore;36import org.junit.runner.Result;37import org.junit.runner.notification.Failure;38public class TestRunner {39 public static void main(String[] args) {40 Result result = JUnitCore.runClasses(TestJunit1.class);41 for (Failure failure : result.getFailures()) {42 System.out.println(failure.toString());43 }44 System.out.println(result.wasSuccessful());45 }46}47package com.tutorialspoint.junit;48import org.junit.runner.JUnitCore;49import org.junit.runner.Result;50import org.junit.runner.notification.Failure;51public class TestRunner {52 public static void main(String[] args) {53 Result result = JUnitCore.runClasses(TestJunit2.class);54 for (Failure failure : result.getFailures()) {55 System.out.println(failure

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1public class TestSuiteExample {2 public static void main(String[] args) {3 TestSuite suite = new TestSuite();4 suite.addTestSuite(TestJunit1.class);5 suite.addTestSuite(TestJunit2.class);6 TestResult result = new TestResult();7 suite.run(result);8 System.out.println("Number of test cases = " + result.runCount());9 }10}

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2public class TestRunner {3public static void main(String[] args) {4TestSuite suite = new TestSuite();5suite.addTestSuite(TestJunit1.class);6suite.addTestSuite(TestJunit2.class);7junit.textui.TestRunner.run(suite);8}9}10import junit.framework.Test;11import junit.framework.TestSuite;12public class TestRunner {13public static void main(String[] args) {14TestSuite suite = new TestSuite();15suite.addTest(new TestJunit1("testAdd"));16suite.addTest(new TestJunit1("testDivideByZero"));17suite.addTest(new TestJunit2("testAdd"));18suite.addTest(new TestJunit2("testDivideByZero"));19junit.textui.TestRunner.run(suite);20}21}22junit.textui.TestRunner.run(suite);23package com.javatpoint; 24import org.junit.runner.JUnitCore; 25import org.junit.runner.Result; 26import org.junit.runner.notification.Failure; 27public class TestRunner { 28public static void main(String[] args) { 29Result result = JUnitCore.runClasses(TestJunit.class); 30for (Failure failure : result.getFailures()) { 31System.out.println(failure.toString()); 32} 33System.out.println(result.wasSuccessful()); 34} 35}

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2import junit.framework.Test;3import junit.framework.TestCase;4public class TestSuiteExample extends TestCase {5 protected int value1, value2;6 protected void setUp(){7 value1 = 3;8 value2 = 3;9 }10 public void testAdd(){11 double result = value1 + value2;12 assertTrue(result == 6);13 }14}15public class TestSuiteTest extends TestCase {16 public static Test suite() {17 TestSuite suite = new TestSuite();18 suite.addTest(new TestSuiteExample("testAdd"));19 suite.addTest(new TestSuiteExample("testAdd"));20 return suite;21 }22 public static void main(String args[]) {23 junit.textui.TestRunner.run(suite());24 }25}26OK (2 tests)27import junit.framework.TestSuite;28import junit.framework.Test;29import junit.framework.TestCase;30public class TestSuiteExample extends TestCase {31 protected int value1, value2;32 protected void setUp(){33 value1 = 3;34 value2 = 3;35 }36 public void testAdd(){37 double result = value1 + value2;38 assertTrue(result == 6);39 }40 public void testSubtract(){41 double result = value1 - value2;42 assertTrue(result == 0);43 }44}45public class TestSuiteTest extends TestCase {46 public static Test suite() {47 TestSuite suite = new TestSuite();48 suite.addTest(new TestSuiteExample("testAdd"));49 suite.addTest(new TestSuiteExample("testSubtract"));50 return suite;51 }

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2public class TestAll {3 public static void main(String[] args) {4 junit.textui.TestRunner.run(suite());5 }6 public static TestSuite suite() {7 TestSuite suite = new TestSuite();8 suite.addTestSuite(TestOne.class);9 suite.addTestSuite(TestTwo.class);10 return suite;11 }12}13package com.test;14import junit.framework.TestCase;15public class TestOne extends TestCase {16 public void testOne() {17 assertTrue(true);18 }19}20package com.test;21import junit.framework.TestCase;22public class TestTwo extends TestCase {23 public void testTwo() {24 assertTrue(true);25 }26}27OK (2 tests)28TestSuite(Class<? extends TestCase> theClass, Class<? extends TestCase>... classes) : It

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2public class TestSuiteExample{3 public static void main(String args[]){4 TestSuite suite = new TestSuite(TestJunit1.class, TestJunit2.class);5 TestResult result = new TestResult();6 suite.run(result);7 System.out.println("Number of test cases = " + result.runCount());8 }9}10import junit.framework.TestSuite;11public class TestSuiteExample{12 public static void main(String args[]){13 TestSuite suite = new TestSuite();14 suite.addTest(new TestJunit1("testAdd"));15 suite.addTest(new TestJunit1("testMultiply"));16 TestResult result = new TestResult();17 suite.run(result);18 System.out.println("Number of test cases = " + result.runCount());19 }20}21import junit.framework.TestSuite;22public class TestSuiteExample{23 public static void main(String args[]){24 TestSuite suite = new TestSuite();25 suite.addTestSuite(TestJunit1.class);26 suite.addTestSuite(TestJunit2.class);27 TestResult result = new TestResult();28 suite.run(result);29 System.out.println("Number of test cases = " + result.runCount());30 }31}

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1package com.journaldev.junit;2import junit.framework.Test;3import junit.framework.TestCase;4import junit.framework.TestResult;5import junit.framework.TestSuite;6public class TestSuiteExample extends TestCase {7 public static Test suite() {8 TestSuite suite = new TestSuite();9 suite.addTest(new TestSuite(Test1.class));10 suite.addTest(new TestSuite(Test2.class));11 suite.addTest(new TestSuite(Test3.class));12 return suite;13 }14 public static void main(String[] args) {15 TestResult result = new TestResult();16 Test suite = suite();17 suite.run(result);18 System.out.println("Number of test cases = " + result.runCount());19 }20}21package com.journaldev.junit;22import junit.framework.Test;23import junit.framework.TestResult;24import junit.framework.TestSuite;25import junit.textui.TestRunner;26public class TestRunnerExample {27 public static void main(String[] args) {28 TestResult result = new TestResult();29 Test suite = TestSuiteExample.suite();30 TestRunner.run(suite);31 }32}33endTest(Test test) – This method is invoked after the test is run

Full Screen

Full Screen

tests

Using AI Code Generation

copy

Full Screen

1import junit.framework.TestSuite;2import junit.framework.Test;3import junit.textui.TestRunner;4{5 public static void main(String[] args)6 {7 TestRunner.run(suite());8 }9 public static Test suite()10 {11 TestSuite suite = new TestSuite();12 suite.addTestSuite(TestAdd.class);13 suite.addTestSuite(TestSub.class);14 suite.addTestSuite(TestMul.class);15 suite.addTestSuite(TestDiv.class);16 return suite;17 }18}19import junit.framework.TestSuite;20import junit.framework.Test;21import junit.textui.TestRunner;22{23 public static void main(String[] args)24 {25 TestRunner.run(suite());26 }27 public static Test suite()28 {29 TestSuite suite = new TestSuite();30 suite.addTestSuite(TestAdd.class);31 suite.addTestSuite(TestSub.class);32 suite.addTestSuite(TestMul.class);33 suite.addTestSuite(TestDiv.class);34 return suite;35 }36}37import junit.framework.TestCase;38{39 public void testAdd()40 {41 Calculator calc = new Calculator();42 assertEquals(3, calc.add(1, 2));43 }44}45import junit.framework.TestCase;46{47 public void testSub()48 {49 Calculator calc = new Calculator();50 assertEquals(1, calc.sub(2, 1));51 }52}53import junit.framework.TestCase;54{55 public void testMul()56 {57 Calculator calc = new Calculator();58 assertEquals(2, calc.mul(2, 1));59 }60}61import junit.framework.TestCase;62{63 public void testDiv()64 {65 Calculator calc = new Calculator();66 assertEquals(2, calc.div(4, 2));67 }68}69{70 public int add(int a, int b)71 {72 return a + b;73 }74 public int sub(int a, int b)75 {

Full Screen

Full Screen

JUnit Tutorial:

LambdaTest also has a detailed JUnit tutorial explaining its features, importance, advanced use cases, best practices, and more to help you get started with running your automation testing scripts.

JUnit Tutorial Chapters:

Here are the detailed JUnit testing chapters to help you get started:

  • Importance of Unit testing - Learn why Unit testing is essential during the development phase to identify bugs and errors.
  • Top Java Unit testing frameworks - Here are the upcoming JUnit automation testing frameworks that you can use in 2023 to boost your unit testing.
  • What is the JUnit framework
  • Why is JUnit testing important - Learn the importance and numerous benefits of using the JUnit testing framework.
  • Features of JUnit - Learn about the numerous features of JUnit and why developers prefer it.
  • JUnit 5 vs. JUnit 4: Differences - Here is a complete comparison between JUnit 5 and JUnit 4 testing frameworks.
  • Setting up the JUnit environment - Learn how to set up your JUnit testing environment.
  • Getting started with JUnit testing - After successfully setting up your JUnit environment, this chapter will help you get started with JUnit testing in no time.
  • Parallel testing with JUnit - Parallel Testing can be used to reduce test execution time and improve test efficiency. Learn how to perform parallel testing with JUnit.
  • Annotations in JUnit - When writing automation scripts with JUnit, we can use JUnit annotations to specify the type of methods in our test code. This helps us identify those methods when we run JUnit tests using Selenium WebDriver. Learn in detail what annotations are in JUnit.
  • Assertions in JUnit - Assertions are used to validate or test that the result of an action/functionality is the same as expected. Learn in detail what assertions are and how to use them while performing JUnit testing.
  • Parameterization in JUnit - Parameterized Test enables you to run the same automated test scripts with different variables. By collecting data on each method's test parameters, you can minimize time spent on writing tests. Learn how to use parameterization in JUnit.
  • Nested Tests In JUnit 5 - A nested class is a non-static class contained within another class in a hierarchical structure. It can share the state and setup of the outer class. Learn about nested annotations in JUnit 5 with examples.
  • Best practices for JUnit testing - Learn about the best practices, such as always testing key methods and classes, integrating JUnit tests with your build, and more to get the best possible results.
  • Advanced Use Cases for JUnit testing - Take a deep dive into the advanced use cases, such as how to run JUnit tests in Jupiter, how to use JUnit 5 Mockito for Unit testing, and more for JUnit testing.

JUnit Certification:

You can also check out our JUnit certification if you wish to take your career in Selenium automation testing with JUnit to the next level.

Run junit automation tests on LambdaTest cloud grid

Perform automation testing on 3000+ real desktop and mobile devices online.

Try LambdaTest Now !!

Get 100 minutes of automation test minutes FREE!!

Next-Gen App & Browser Testing Cloud

Was this article helpful?

Helpful

NotHelpful