KaneAI - World’s First E2E Software Testing Agent.Signup for Private Beta Join TestMu Conference

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

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

Source:JMLValueSet_JML_Test.java

...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;...

Source:JMLInteger_JML_Test.java

...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();...

Source:JMLChar_JML_Test.java

...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;...

Source:JMLString_JML_Test.java

...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