// This file was generated by jmlunit on Mon Mar 16 13:11:59 EDT 2009. package org.jmlspecs.models.resolve; import java.math.BigInteger; /** Automatically-generated test driver for JML and JUnit based * testing of NaturalNumber. The superclass of this class should be edited * to supply test data. However it's best not to edit this class * directly; instead use the command *
* jmlunit NaturalNumber.java ** to regenerate this class whenever NaturalNumber.java changes. */ public class NaturalNumber_JML_Test extends NaturalNumber_JML_TestData { /** Initialize this class. */ public NaturalNumber_JML_Test(java.lang.String name) { super(name); } /** Run the tests. */ public static void main(java.lang.String[] args) { org.jmlspecs.jmlunit.JMLTestRunner.run(suite()); // You can also use a JUnit test runner such as: // junit.textui.TestRunner.run(suite()); } /** Test to see if the code for class NaturalNumber * has been compiled with runtime assertion checking (i.e., by jmlc). * Code that is not compiled with jmlc would not make an effective test, * since no assertion checking would be done. */ public void test$IsRACCompiled() { junit.framework.Assert.assertTrue("code for class NaturalNumber" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(NaturalNumber.class) ); } /** Return the test suite for this test class. This will have * added to it at least test$IsRACCompiled(), and any test methods * written explicitly by the user in the superclass. It will also * have added test suites for each testing each method and * constructor. */ //@ ensures \result != null; public static junit.framework.Test suite() { NaturalNumber_JML_Test testobj = new NaturalNumber_JML_Test("NaturalNumber_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(NaturalNumber_JML_Test.class); testobj.addTestSuiteForEachMethod(testsuite); return testsuite; } /** A JUnit test object that can run a single test method. This * is defined as a nested class solely for convenience; it can't * be defined once and for all because it must subclass its * enclosing class. */ protected static abstract class OneTest extends NaturalNumber_JML_Test { /** Initialize this test object. */ public OneTest(String name) { super(name); } /** The result object that holds information about testing. */ protected junit.framework.TestResult result; //@ also //@ requires result != null; public void run(junit.framework.TestResult result) { this.result = result; super.run(result); } /* Run a single test and decide whether the test was * successful, meaningless, or a failure. This is the * Template Method pattern abstraction of the inner loop in a * JML/JUnit test. */ public void runTest() throws java.lang.Throwable { try { // The call being tested! doCall(); } catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) { // meaningless test input addMeaningless(); } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) { // test failure int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel(); org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel (org.jmlspecs.jmlrac.runtime.JMLOption.NONE); try { java.lang.String failmsg = this.failMessage(e); junit.framework.AssertionFailedError err = new junit.framework.AssertionFailedError(failmsg); err.setStackTrace(new java.lang.StackTraceElement[]{}); err.initCause(e); result.addFailure(this, err); } finally { org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l); } } catch (java.lang.Throwable e) { // test success } } /** Call the method to be tested with the appropriate arguments. */ protected abstract void doCall() throws java.lang.Throwable; /** Format the error message for a test failure, based on the * method's arguments. */ protected abstract java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e); /** Inform listeners that a meaningless test was run. */ private void addMeaningless() { if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) { ((org.jmlspecs.jmlunit.JMLTestResult)result) .addMeaningless(this); } } } /** Create the tests that are to be run for testing the class * NaturalNumber. The framework will then run them. * @param overallTestSuite$ The suite accumulating all of the tests * for this driver class. */ //@ requires overallTestSuite$ != null; public void addTestSuiteForEachMethod (junit.framework.TestSuite overallTestSuite$) { try { this.addTestSuiteFor$TestNaturalNumber(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestNaturalNumber$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestNaturalNumber$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestValueOf(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSuc(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSuc$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAdd(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestMultiply(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDivide(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemainder(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestPow(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestPow$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGcd(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestMod(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestShiftLeft(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestShiftRight(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompareTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompareTo$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompareTo$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestEquals(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestClone(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsZero(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDivides(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestMin(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestMax(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHashCode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToString(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestBigIntegerValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIntValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestLongValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestFloatValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDoubleValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestByteValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestShortValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } } /** Add tests for the NaturalNumber contructor * to the overall test suite. */ private void addTestSuiteFor$TestNaturalNumber (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("NaturalNumber"); try { methodTests$.addTest (new TestNaturalNumber()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the NaturalNumber contructor. */ protected static class TestNaturalNumber extends OneTest { /** Initialize this instance. */ public TestNaturalNumber() { super("NaturalNumber"); } protected void doCall() throws java.lang.Throwable { new NaturalNumber(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'NaturalNumber'"; return msg; } } /** Add tests for the NaturalNumber contructor * to the overall test suite. */ private void addTestSuiteFor$TestNaturalNumber$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("NaturalNumber"); try { org.jmlspecs.jmlunit.strategies.LongIterator vlong$1$iter = this.vlongIter("NaturalNumber", 0); this.check_has_data (vlong$1$iter, "this.vlongIter(\"NaturalNumber\", 0)"); while (!vlong$1$iter.atEnd()) { final long val = vlong$1$iter.getLong(); methodTests$.addTest (new TestNaturalNumber$1(val)); vlong$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the NaturalNumber contructor. */ protected static class TestNaturalNumber$1 extends OneTest { /** Argument val */ private long val; /** Initialize this instance. */ public TestNaturalNumber$1(long val) { super("NaturalNumber"+ ":" + val); this.val = val; } protected void doCall() throws java.lang.Throwable { new NaturalNumber(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'NaturalNumber' applied to"; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the NaturalNumber contructor * to the overall test suite. */ private void addTestSuiteFor$TestNaturalNumber$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("NaturalNumber"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_math_BigInteger$1$iter = this.vjava_math_BigIntegerIter("NaturalNumber", 0); this.check_has_data (vjava_math_BigInteger$1$iter, "this.vjava_math_BigIntegerIter(\"NaturalNumber\", 0)"); while (!vjava_math_BigInteger$1$iter.atEnd()) { final java.math.BigInteger val = (java.math.BigInteger) vjava_math_BigInteger$1$iter.get(); methodTests$.addTest (new TestNaturalNumber$2(val)); vjava_math_BigInteger$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the NaturalNumber contructor. */ protected static class TestNaturalNumber$2 extends OneTest { /** Argument val */ private java.math.BigInteger val; /** Initialize this instance. */ public TestNaturalNumber$2(java.math.BigInteger val) { super("NaturalNumber"+ ":" + (val==null? "null" :"{java.math.BigInteger}")); this.val = val; } protected void doCall() throws java.lang.Throwable { new NaturalNumber(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'NaturalNumber' applied to"; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the valueOf method * to the overall test suite. */ private void addTestSuiteFor$TestValueOf (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("valueOf"); try { org.jmlspecs.jmlunit.strategies.LongIterator vlong$1$iter = this.vlongIter("valueOf", 0); this.check_has_data (vlong$1$iter, "this.vlongIter(\"valueOf\", 0)"); while (!vlong$1$iter.atEnd()) { final long val = vlong$1$iter.getLong(); methodTests$.addTest (new TestValueOf(val)); vlong$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the valueOf method. */ protected static class TestValueOf extends OneTest { /** Argument val */ private long val; /** Initialize this instance. */ public TestValueOf(long val) { super("valueOf"+ ":" + val); this.val = val; } protected void doCall() throws java.lang.Throwable { NaturalNumber.valueOf(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'valueOf' applied to"; msg += "\n\tReceiver class NaturalNumber"; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the suc method * to the overall test suite. */ private void addTestSuiteFor$TestSuc (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("suc"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("suc", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"suc\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestSuc(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the suc method. */ protected static class TestSuc extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestSuc(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("suc"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.suc(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'suc' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the suc method * to the overall test suite. */ private void addTestSuiteFor$TestSuc$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("suc"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("suc", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"suc\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber v = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestSuc$1(v)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the suc method. */ protected static class TestSuc$1 extends OneTest { /** Argument v */ private org.jmlspecs.models.resolve.NaturalNumber v; /** Initialize this instance. */ public TestSuc$1(org.jmlspecs.models.resolve.NaturalNumber v) { super("suc"+ ":" + (v==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.v = v; } protected void doCall() throws java.lang.Throwable { NaturalNumber.suc(v); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'suc' applied to"; msg += "\n\tReceiver class NaturalNumber"; msg += "\n\tArgument v: " + this.v; return msg; } } /** Add tests for the add method * to the overall test suite. */ private void addTestSuiteFor$TestAdd (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("add"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("add", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"add\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("add", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"add\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestAdd(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the add method. */ protected static class TestAdd extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestAdd(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("add"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.add(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'add' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the multiply method * to the overall test suite. */ private void addTestSuiteFor$TestMultiply (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("multiply"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("multiply", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"multiply\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("multiply", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"multiply\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestMultiply(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the multiply method. */ protected static class TestMultiply extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestMultiply(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("multiply"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.multiply(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'multiply' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the divide method * to the overall test suite. */ private void addTestSuiteFor$TestDivide (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("divide"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("divide", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"divide\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("divide", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"divide\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestDivide(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the divide method. */ protected static class TestDivide extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestDivide(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("divide"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.divide(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'divide' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the remainder method * to the overall test suite. */ private void addTestSuiteFor$TestRemainder (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("remainder"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("remainder", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"remainder\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("remainder", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"remainder\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestRemainder(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the remainder method. */ protected static class TestRemainder extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestRemainder(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("remainder"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.remainder(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'remainder' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the pow method * to the overall test suite. */ private void addTestSuiteFor$TestPow (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("pow"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("pow", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"pow\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("pow", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"pow\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber exponent = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestPow(receiver$, exponent)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the pow method. */ protected static class TestPow extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument exponent */ private org.jmlspecs.models.resolve.NaturalNumber exponent; /** Initialize this instance. */ public TestPow(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber exponent) { super("pow"+ ":" + (exponent==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.exponent = exponent; } protected void doCall() throws java.lang.Throwable { receiver$.pow(exponent); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'pow' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument exponent: " + this.exponent; return msg; } } /** Add tests for the pow method * to the overall test suite. */ private void addTestSuiteFor$TestPow$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("pow"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("pow", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"pow\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("pow", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"pow\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final int exponent = vint$1$iter.getInt(); methodTests$.addTest (new TestPow$1(receiver$, exponent)); vint$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the pow method. */ protected static class TestPow$1 extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument exponent */ private int exponent; /** Initialize this instance. */ public TestPow$1(org.jmlspecs.models.resolve.NaturalNumber receiver$, int exponent) { super("pow"+ ":" + exponent); this.receiver$ = receiver$; this.exponent = exponent; } protected void doCall() throws java.lang.Throwable { receiver$.pow(exponent); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'pow' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument exponent: " + this.exponent; return msg; } } /** Add tests for the gcd method * to the overall test suite. */ private void addTestSuiteFor$TestGcd (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("gcd"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("gcd", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"gcd\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("gcd", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"gcd\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestGcd(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the gcd method. */ protected static class TestGcd extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestGcd(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("gcd"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.gcd(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'gcd' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the mod method * to the overall test suite. */ private void addTestSuiteFor$TestMod (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("mod"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("mod", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"mod\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("mod", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"mod\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber m = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestMod(receiver$, m)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the mod method. */ protected static class TestMod extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument m */ private org.jmlspecs.models.resolve.NaturalNumber m; /** Initialize this instance. */ public TestMod(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber m) { super("mod"+ ":" + (m==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.m = m; } protected void doCall() throws java.lang.Throwable { receiver$.mod(m); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'mod' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument m: " + this.m; return msg; } } /** Add tests for the shiftLeft method * to the overall test suite. */ private void addTestSuiteFor$TestShiftLeft (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("shiftLeft"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("shiftLeft", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"shiftLeft\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("shiftLeft", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"shiftLeft\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final int n = vint$1$iter.getInt(); methodTests$.addTest (new TestShiftLeft(receiver$, n)); vint$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the shiftLeft method. */ protected static class TestShiftLeft extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument n */ private int n; /** Initialize this instance. */ public TestShiftLeft(org.jmlspecs.models.resolve.NaturalNumber receiver$, int n) { super("shiftLeft"+ ":" + n); this.receiver$ = receiver$; this.n = n; } protected void doCall() throws java.lang.Throwable { receiver$.shiftLeft(n); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'shiftLeft' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; return msg; } } /** Add tests for the shiftRight method * to the overall test suite. */ private void addTestSuiteFor$TestShiftRight (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("shiftRight"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("shiftRight", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"shiftRight\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("shiftRight", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"shiftRight\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final int n = vint$1$iter.getInt(); methodTests$.addTest (new TestShiftRight(receiver$, n)); vint$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the shiftRight method. */ protected static class TestShiftRight extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument n */ private int n; /** Initialize this instance. */ public TestShiftRight(org.jmlspecs.models.resolve.NaturalNumber receiver$, int n) { super("shiftRight"+ ":" + n); this.receiver$ = receiver$; this.n = n; } protected void doCall() throws java.lang.Throwable { receiver$.shiftRight(n); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'shiftRight' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; return msg; } } /** Add tests for the compareTo method * to the overall test suite. */ private void addTestSuiteFor$TestCompareTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compareTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("compareTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"compareTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("compareTo", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"compareTo\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestCompareTo(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compareTo method. */ protected static class TestCompareTo extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestCompareTo(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("compareTo"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.compareTo(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compareTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the compareTo method * to the overall test suite. */ private void addTestSuiteFor$TestCompareTo$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compareTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("compareTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"compareTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_math_BigInteger$1$iter = this.vjava_math_BigIntegerIter("compareTo", 0); this.check_has_data (vjava_math_BigInteger$1$iter, "this.vjava_math_BigIntegerIter(\"compareTo\", 0)"); while (!vjava_math_BigInteger$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final java.math.BigInteger val = (java.math.BigInteger) vjava_math_BigInteger$1$iter.get(); methodTests$.addTest (new TestCompareTo$1(receiver$, val)); vjava_math_BigInteger$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compareTo method. */ protected static class TestCompareTo$1 extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private java.math.BigInteger val; /** Initialize this instance. */ public TestCompareTo$1(org.jmlspecs.models.resolve.NaturalNumber receiver$, java.math.BigInteger val) { super("compareTo"+ ":" + (val==null? "null" :"{java.math.BigInteger}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.compareTo(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compareTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the compareTo method * to the overall test suite. */ private void addTestSuiteFor$TestCompareTo$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compareTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("compareTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"compareTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("compareTo", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"compareTo\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final java.lang.Object o = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestCompareTo$2(receiver$, o)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compareTo method. */ protected static class TestCompareTo$2 extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument o */ private java.lang.Object o; /** Initialize this instance. */ public TestCompareTo$2(org.jmlspecs.models.resolve.NaturalNumber receiver$, java.lang.Object o) { super("compareTo"+ ":" + (o==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.o = o; } protected void doCall() throws java.lang.Throwable { receiver$.compareTo(o); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compareTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument o: " + this.o; return msg; } } /** Add tests for the equals method * to the overall test suite. */ private void addTestSuiteFor$TestEquals (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("equals"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"equals\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("equals", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"equals\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final java.lang.Object x = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestEquals(receiver$, x)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the equals method. */ protected static class TestEquals extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument x */ private java.lang.Object x; /** Initialize this instance. */ public TestEquals(org.jmlspecs.models.resolve.NaturalNumber receiver$, java.lang.Object x) { super("equals"+ ":" + (x==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.x = x; } protected void doCall() throws java.lang.Throwable { receiver$.equals(x); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'equals' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument x: " + this.x; return msg; } } /** Add tests for the clone method * to the overall test suite. */ private void addTestSuiteFor$TestClone (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("clone"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestClone(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the clone method. */ protected static class TestClone extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("clone"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.clone(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'clone' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the isZero method * to the overall test suite. */ private void addTestSuiteFor$TestIsZero (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isZero"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("isZero", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"isZero\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestIsZero(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isZero method. */ protected static class TestIsZero extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestIsZero(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("isZero"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isZero(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isZero' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the divides method * to the overall test suite. */ private void addTestSuiteFor$TestDivides (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("divides"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("divides", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"divides\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("divides", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"divides\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestDivides(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the divides method. */ protected static class TestDivides extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestDivides(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("divides"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.divides(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'divides' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the min method * to the overall test suite. */ private void addTestSuiteFor$TestMin (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("min"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("min", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"min\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("min", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"min\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestMin(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the min method. */ protected static class TestMin extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestMin(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("min"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.min(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'min' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the max method * to the overall test suite. */ private void addTestSuiteFor$TestMax (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("max"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("max", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"max\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_resolve_NaturalNumber$1$iter = this.vorg_jmlspecs_models_resolve_NaturalNumberIter("max", 0); this.check_has_data (vorg_jmlspecs_models_resolve_NaturalNumber$1$iter, "this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"max\", 0)"); while (!vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); final org.jmlspecs.models.resolve.NaturalNumber val = (org.jmlspecs.models.resolve.NaturalNumber) vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.get(); methodTests$.addTest (new TestMax(receiver$, val)); vorg_jmlspecs_models_resolve_NaturalNumber$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the max method. */ protected static class TestMax extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Argument val */ private org.jmlspecs.models.resolve.NaturalNumber val; /** Initialize this instance. */ public TestMax(org.jmlspecs.models.resolve.NaturalNumber receiver$, org.jmlspecs.models.resolve.NaturalNumber val) { super("max"+ ":" + (val==null? "null" :"{org.jmlspecs.models.resolve.NaturalNumber}")); this.receiver$ = receiver$; this.val = val; } protected void doCall() throws java.lang.Throwable { receiver$.max(val); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'max' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument val: " + this.val; return msg; } } /** Add tests for the hashCode method * to the overall test suite. */ private void addTestSuiteFor$TestHashCode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("hashCode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestHashCode(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the hashCode method. */ protected static class TestHashCode extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("hashCode"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.hashCode(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'hashCode' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the toString method * to the overall test suite. */ private void addTestSuiteFor$TestToString (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toString"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestToString(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toString method. */ protected static class TestToString extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("toString"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toString(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toString' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the bigIntegerValue method * to the overall test suite. */ private void addTestSuiteFor$TestBigIntegerValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("bigIntegerValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("bigIntegerValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"bigIntegerValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestBigIntegerValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the bigIntegerValue method. */ protected static class TestBigIntegerValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestBigIntegerValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("bigIntegerValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.bigIntegerValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'bigIntegerValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the intValue method * to the overall test suite. */ private void addTestSuiteFor$TestIntValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("intValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("intValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"intValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestIntValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the intValue method. */ protected static class TestIntValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestIntValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("intValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.intValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'intValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the longValue method * to the overall test suite. */ private void addTestSuiteFor$TestLongValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("longValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("longValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"longValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestLongValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the longValue method. */ protected static class TestLongValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestLongValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("longValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.longValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'longValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the floatValue method * to the overall test suite. */ private void addTestSuiteFor$TestFloatValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("floatValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("floatValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"floatValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestFloatValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the floatValue method. */ protected static class TestFloatValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestFloatValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("floatValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.floatValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'floatValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the doubleValue method * to the overall test suite. */ private void addTestSuiteFor$TestDoubleValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("doubleValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("doubleValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"doubleValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestDoubleValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the doubleValue method. */ protected static class TestDoubleValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestDoubleValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("doubleValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.doubleValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'doubleValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the byteValue method * to the overall test suite. */ private void addTestSuiteFor$TestByteValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("byteValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("byteValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"byteValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestByteValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the byteValue method. */ protected static class TestByteValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestByteValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("byteValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.byteValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'byteValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the shortValue method * to the overall test suite. */ private void addTestSuiteFor$TestShortValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("shortValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_resolve_NaturalNumberIter("shortValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_resolve_NaturalNumberIter(\"shortValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.resolve.NaturalNumber receiver$ = (org.jmlspecs.models.resolve.NaturalNumber) receivers$iter.get(); methodTests$.addTest (new TestShortValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the shortValue method. */ protected static class TestShortValue extends OneTest { /** The receiver */ private org.jmlspecs.models.resolve.NaturalNumber receiver$; /** Initialize this instance. */ public TestShortValue(org.jmlspecs.models.resolve.NaturalNumber receiver$) { super("shortValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.shortValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'shortValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Check that the iterator is non-null and not empty. */ private void check_has_data(org.jmlspecs.jmlunit.strategies.IndefiniteIterator iter, String call) { if (iter == null) { junit.framework.Assert.fail(call + " returned null"); } if (iter.atEnd()) { junit.framework.Assert.fail(call + " returned an empty iterator"); } } /** Converts a char to a printable String for display */ public static String charToString(char c) { if (c == '\n') { return "NL"; } else if (c == '\r') { return "CR"; } else if (c == '\t') { return "TAB"; } else if (Character.isISOControl(c)) { int i = (int)c; return "\\u" + Character.forDigit((i/2048)%16,16) + Character.forDigit((i/256)%16,16) + Character.forDigit((i/16)%16,16) + Character.forDigit((i)%16,16); } return Character.toString(c); } }