Unlock 30% off on Manual Testing Annual Plans this Holiday Season.

Copied to Clipboard!

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            }706        } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {707            // methodTests$ doesn't want more tests708        }709        overallTestSuite$.addTest(methodTests$);710    }711    /** Test for the toString method. */712    protected static class TestToString extends OneTest {713        /** The receiver */714        private org.jmlspecs.models.JMLString receiver$;715        /** Initialize this instance. */716        public TestToString(org.jmlspecs.models.JMLString receiver$) {717            super("toString");718            this.receiver$ = receiver$;719        }720        protected void doCall() throws java.lang.Throwable {721            receiver$.toString();722        }723        protected java.lang.String failMessage724            (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)725        {726            java.lang.String msg = "\n\tMethod 'toString' applied to";727            msg += "\n\tReceiver: " + this.receiver$;728            return msg;729        }730    }731    /** Add tests for the concat method732     * to the overall test suite. */733    private void addTestSuiteFor$TestConcat734        (junit.framework.TestSuite overallTestSuite$)735    {736        junit.framework.TestSuite methodTests$737            = this.emptyTestSuiteFor("concat");738        try {739            org.jmlspecs.jmlunit.strategies.IndefiniteIterator740                receivers$iter741                = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator742                    (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));743            this.check_has_data744                (receivers$iter,745                 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");746            while (!receivers$iter.atEnd()) {747                org.jmlspecs.jmlunit.strategies.IndefiniteIterator748                    vorg_jmlspecs_models_JMLString$1$iter749                    = this.vorg_jmlspecs_models_JMLStringIter("concat", 0);750                this.check_has_data751                    (vorg_jmlspecs_models_JMLString$1$iter,752                     "this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 0)");753                while (!vorg_jmlspecs_models_JMLString$1$iter.atEnd()) {754                    final org.jmlspecs.models.JMLString receiver$755                        = (org.jmlspecs.models.JMLString) receivers$iter.get();756                    final org.jmlspecs.models.JMLString s757                        = (org.jmlspecs.models.JMLString) vorg_jmlspecs_models_JMLString$1$iter.get();758                    methodTests$.addTest759                        (new TestConcat(receiver$, s));760                    vorg_jmlspecs_models_JMLString$1$iter.advance();761                }762                receivers$iter.advance();763            }764        } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {765            // methodTests$ doesn't want more tests766        }767        overallTestSuite$.addTest(methodTests$);768    }769    /** Test for the concat method. */770    protected static class TestConcat extends OneTest {771        /** The receiver */772        private org.jmlspecs.models.JMLString receiver$;773        /** Argument s */774        private org.jmlspecs.models.JMLString s;775        /** Initialize this instance. */776        public TestConcat(org.jmlspecs.models.JMLString receiver$, org.jmlspecs.models.JMLString s) {777            super("concat"+ ":" + (s==null? "null" :"{org.jmlspecs.models.JMLString}"));778            this.receiver$ = receiver$;779            this.s = s;780        }781        protected void doCall() throws java.lang.Throwable {782            receiver$.concat(s);783        }784        protected java.lang.String failMessage785            (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)786        {787            java.lang.String msg = "\n\tMethod 'concat' applied to";788            msg += "\n\tReceiver: " + this.receiver$;789            msg += "\n\tArgument s: " + this.s;790            return msg;791        }792    }793    /** Add tests for the concat method794     * to the overall test suite. */795    private void addTestSuiteFor$TestConcat$1796        (junit.framework.TestSuite overallTestSuite$)797    {798        junit.framework.TestSuite methodTests$799            = this.emptyTestSuiteFor("concat");800        try {801            org.jmlspecs.jmlunit.strategies.IndefiniteIterator802                receivers$iter803                = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator804                    (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));805            this.check_has_data806                (receivers$iter,807                 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");808            while (!receivers$iter.atEnd()) {809                org.jmlspecs.jmlunit.strategies.IndefiniteIterator810                    vjava_lang_String$1$iter811                    = this.vjava_lang_StringIter("concat", 0);812                this.check_has_data813                    (vjava_lang_String$1$iter,814                     "this.vjava_lang_StringIter(\"concat\", 0)");815                while (!vjava_lang_String$1$iter.atEnd()) {816                    final org.jmlspecs.models.JMLString receiver$817                        = (org.jmlspecs.models.JMLString) receivers$iter.get();818                    final java.lang.String s819                        = (java.lang.String) vjava_lang_String$1$iter.get();820                    methodTests$.addTest821                        (new TestConcat$1(receiver$, s));822                    vjava_lang_String$1$iter.advance();823                }824                receivers$iter.advance();825            }826        } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {827            // methodTests$ doesn't want more tests828        }829        overallTestSuite$.addTest(methodTests$);830    }831    /** Test for the concat method. */832    protected static class TestConcat$1 extends OneTest {833        /** The receiver */834        private org.jmlspecs.models.JMLString receiver$;835        /** Argument s */836        private java.lang.String s;837        /** Initialize this instance. */838        public TestConcat$1(org.jmlspecs.models.JMLString receiver$, java.lang.String s) {839            super("concat"+ ":" + (s==null? "null" :("\""+s+"\"")));840            this.receiver$ = receiver$;841            this.s = s;842        }843        protected void doCall() throws java.lang.Throwable {844            receiver$.concat(s);845        }846        protected java.lang.String failMessage847            (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$)848        {849            java.lang.String msg = "\n\tMethod 'concat' applied to";850            msg += "\n\tReceiver: " + this.receiver$;851            msg += "\n\tArgument s: " + this.s;852            return msg;853        }854    }855    /** Add tests for the concat method856     * to the overall test suite. */857    private void addTestSuiteFor$TestConcat$2858        (junit.framework.TestSuite overallTestSuite$)859    {860        junit.framework.TestSuite methodTests$861            = this.emptyTestSuiteFor("concat");862        try {863            org.jmlspecs.jmlunit.strategies.IndefiniteIterator864                receivers$iter865                = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator866                    (this.vorg_jmlspecs_models_JMLStringIter("concat", 1));867            this.check_has_data868                (receivers$iter,869                 "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLStringIter(\"concat\", 1))");870            while (!receivers$iter.atEnd()) {871                org.jmlspecs.jmlunit.strategies.CharIterator872                    vchar$1$iter873                    = this.vcharIter("concat", 0);874                this.check_has_data875                    (vchar$1$iter,876                     "this.vcharIter(\"concat\", 0)");877                while (!vchar$1$iter.atEnd()) {878                    final org.jmlspecs.models.JMLString receiver$879                        = (org.jmlspecs.models.JMLString) receivers$iter.get();880                    final char c881                        = vchar$1$iter.getChar();882                    methodTests$.addTest883                        (new TestConcat$2(receiver$, c));884                    vchar$1$iter.advance();885                }886                receivers$iter.advance();887            }888        } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) {889            // methodTests$ doesn't want more tests890        }891        overallTestSuite$.addTest(methodTests$);892    }893    /** Test for the concat method. */894    protected static class TestConcat$2 extends OneTest {895        /** The receiver */896        private org.jmlspecs.models.JMLString receiver$;897        /** Argument c */898        private char c;899        /** Initialize this instance. */900        public TestConcat$2(org.jmlspecs.models.JMLString receiver$, char c) {901            super("concat"+ ":" + "\'"+charToString(c)+"\'");902            this.receiver$ = receiver$;903            this.c = c;...

Source:AbstractTestSuite.java

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

Source:AllTestsTest.java

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

Source:TestSuite.java

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

Source:Str2IntTest.java

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

tests

Using AI Code Generation

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

JUnit Tutorial:

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

JUnit Tutorial Chapters:

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

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