// This file was generated by jmlunit on Mon Mar 16 13:11:57 EDT 2009. package org.jmlspecs.models; import java.util.Enumeration; /** Automatically-generated test driver for JML and JUnit based * testing of JMLValueToValueMap. The superclass of this class should be edited * to supply test data. However it's best not to edit this class * directly; instead use the command *
* jmlunit JMLValueToValueMap.java ** to regenerate this class whenever JMLValueToValueMap.java changes. */ public class JMLValueToValueMap_JML_Test extends JMLValueToValueMap_JML_TestData { /** Initialize this class. */ public JMLValueToValueMap_JML_Test(java.lang.String name) { super(name); } /** Run the tests. */ public static void main(java.lang.String[] args) { org.jmlspecs.jmlunit.JMLTestRunner.run(suite()); // You can also use a JUnit test runner such as: // junit.textui.TestRunner.run(suite()); } /** Test to see if the code for class JMLValueToValueMap * has been compiled with runtime assertion checking (i.e., by jmlc). * Code that is not compiled with jmlc would not make an effective test, * since no assertion checking would be done. */ public void test$IsRACCompiled() { junit.framework.Assert.assertTrue("code for class JMLValueToValueMap" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLValueToValueMap.class) ); } /** Return the test suite for this test class. This will have * added to it at least test$IsRACCompiled(), and any test methods * written explicitly by the user in the superclass. It will also * have added test suites for each testing each method and * constructor. */ //@ ensures \result != null; public static junit.framework.Test suite() { JMLValueToValueMap_JML_Test testobj = new JMLValueToValueMap_JML_Test("JMLValueToValueMap_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(JMLValueToValueMap_JML_Test.class); testobj.addTestSuiteForEachMethod(testsuite); return testsuite; } /** A JUnit test object that can run a single test method. This * is defined as a nested class solely for convenience; it can't * be defined once and for all because it must subclass its * enclosing class. */ protected static abstract class OneTest extends JMLValueToValueMap_JML_Test { /** Initialize this test object. */ public OneTest(String name) { super(name); } /** The result object that holds information about testing. */ protected junit.framework.TestResult result; //@ also //@ requires result != null; public void run(junit.framework.TestResult result) { this.result = result; super.run(result); } /* Run a single test and decide whether the test was * successful, meaningless, or a failure. This is the * Template Method pattern abstraction of the inner loop in a * JML/JUnit test. */ public void runTest() throws java.lang.Throwable { try { // The call being tested! doCall(); } catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) { // meaningless test input addMeaningless(); } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) { // test failure int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel(); org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel (org.jmlspecs.jmlrac.runtime.JMLOption.NONE); try { java.lang.String failmsg = this.failMessage(e); junit.framework.AssertionFailedError err = new junit.framework.AssertionFailedError(failmsg); err.setStackTrace(new java.lang.StackTraceElement[]{}); err.initCause(e); result.addFailure(this, err); } finally { org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l); } } catch (java.lang.Throwable e) { // test success } } /** Call the method to be tested with the appropriate arguments. */ protected abstract void doCall() throws java.lang.Throwable; /** Format the error message for a test failure, based on the * method's arguments. */ protected abstract java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e); /** Inform listeners that a meaningless test was run. */ private void addMeaningless() { if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) { ((org.jmlspecs.jmlunit.JMLTestResult)result) .addMeaningless(this); } } } /** Create the tests that are to be run for testing the class * JMLValueToValueMap. The framework will then run them. * @param overallTestSuite$ The suite accumulating all of the tests * for this driver class. */ //@ requires overallTestSuite$ != null; public void addTestSuiteForEachMethod (junit.framework.TestSuite overallTestSuite$) { try { this.addTestSuiteFor$TestJMLValueToValueMap(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLValueToValueMap$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLValueToValueMap$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSingletonMap(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSingletonMap$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsaFunction(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestApply(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestClone(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestExtend(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveDomainElement(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompose(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompose$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRestrictedTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRangeRestrictedTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestExtendUnion(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestClashReplaceUnion(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDisjointUnion(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestElementImage(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestImage(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInverse(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInverseElementImage(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInverseImage(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsDefinedAt(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHas(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHas$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHas$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsEmpty(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestEquals(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHashCode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDomain(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRange(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAdd(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInsert(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveFromDomain(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemove(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemove$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompose$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCompose$3(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestUnion(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIntersection(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDifference(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRestrictDomainTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRestrictRangeTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToString(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAssociations(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestElements(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIterator(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToSet(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToBag(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToSequence(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestImagePairSet(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestImagePairs(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDomainElements(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRangeElements(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInt_size(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToFunction(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } } /** Add tests for the JMLValueToValueMap contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLValueToValueMap (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLValueToValueMap"); try { methodTests$.addTest (new TestJMLValueToValueMap()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLValueToValueMap contructor. */ protected static class TestJMLValueToValueMap extends OneTest { /** Initialize this instance. */ public TestJMLValueToValueMap() { super("JMLValueToValueMap"); } protected void doCall() throws java.lang.Throwable { new JMLValueToValueMap(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLValueToValueMap'"; return msg; } } /** Add tests for the JMLValueToValueMap contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLValueToValueMap$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLValueToValueMap"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("JMLValueToValueMap", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"JMLValueToValueMap\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("JMLValueToValueMap", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"JMLValueToValueMap\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLType dv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType rv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestJMLValueToValueMap$1(dv, rv)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLValueToValueMap contructor. */ protected static class TestJMLValueToValueMap$1 extends OneTest { /** Argument dv */ private org.jmlspecs.models.JMLType dv; /** Argument rv */ private org.jmlspecs.models.JMLType rv; /** Initialize this instance. */ public TestJMLValueToValueMap$1(org.jmlspecs.models.JMLType dv, org.jmlspecs.models.JMLType rv) { super("JMLValueToValueMap"+ ":" + (dv==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(rv==null? "null" :"{org.jmlspecs.models.JMLType}")); this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { new JMLValueToValueMap(dv, rv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLValueToValueMap' applied to"; msg += "\n\tArgument dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; return msg; } } /** Add tests for the JMLValueToValueMap contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLValueToValueMap$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLValueToValueMap"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePair$1$iter = this.vorg_jmlspecs_models_JMLValueValuePairIter("JMLValueToValueMap", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueValuePair$1$iter, "this.vorg_jmlspecs_models_JMLValueValuePairIter(\"JMLValueToValueMap\", 0)"); while (!vorg_jmlspecs_models_JMLValueValuePair$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueValuePair pair = (org.jmlspecs.models.JMLValueValuePair) vorg_jmlspecs_models_JMLValueValuePair$1$iter.get(); methodTests$.addTest (new TestJMLValueToValueMap$2(pair)); vorg_jmlspecs_models_JMLValueValuePair$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLValueToValueMap contructor. */ protected static class TestJMLValueToValueMap$2 extends OneTest { /** Argument pair */ private org.jmlspecs.models.JMLValueValuePair pair; /** Initialize this instance. */ public TestJMLValueToValueMap$2(org.jmlspecs.models.JMLValueValuePair pair) { super("JMLValueToValueMap"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLValueValuePair}")); this.pair = pair; } protected void doCall() throws java.lang.Throwable { new JMLValueToValueMap(pair); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLValueToValueMap' applied to"; msg += "\n\tArgument pair: " + this.pair; return msg; } } /** Add tests for the singletonMap method * to the overall test suite. */ private void addTestSuiteFor$TestSingletonMap (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("singletonMap"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("singletonMap", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"singletonMap\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("singletonMap", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"singletonMap\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLType dv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType rv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestSingletonMap(dv, rv)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the singletonMap method. */ protected static class TestSingletonMap extends OneTest { /** Argument dv */ private org.jmlspecs.models.JMLType dv; /** Argument rv */ private org.jmlspecs.models.JMLType rv; /** Initialize this instance. */ public TestSingletonMap(org.jmlspecs.models.JMLType dv, org.jmlspecs.models.JMLType rv) { super("singletonMap"+ ":" + (dv==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(rv==null? "null" :"{org.jmlspecs.models.JMLType}")); this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { JMLValueToValueMap.singletonMap(dv, rv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'singletonMap' applied to"; msg += "\n\tReceiver class JMLValueToValueMap"; msg += "\n\tArgument dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; return msg; } } /** Add tests for the singletonMap method * to the overall test suite. */ private void addTestSuiteFor$TestSingletonMap$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("singletonMap"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePair$1$iter = this.vorg_jmlspecs_models_JMLValueValuePairIter("singletonMap", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueValuePair$1$iter, "this.vorg_jmlspecs_models_JMLValueValuePairIter(\"singletonMap\", 0)"); while (!vorg_jmlspecs_models_JMLValueValuePair$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueValuePair pair = (org.jmlspecs.models.JMLValueValuePair) vorg_jmlspecs_models_JMLValueValuePair$1$iter.get(); methodTests$.addTest (new TestSingletonMap$1(pair)); vorg_jmlspecs_models_JMLValueValuePair$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the singletonMap method. */ protected static class TestSingletonMap$1 extends OneTest { /** Argument pair */ private org.jmlspecs.models.JMLValueValuePair pair; /** Initialize this instance. */ public TestSingletonMap$1(org.jmlspecs.models.JMLValueValuePair pair) { super("singletonMap"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLValueValuePair}")); this.pair = pair; } protected void doCall() throws java.lang.Throwable { JMLValueToValueMap.singletonMap(pair); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'singletonMap' applied to"; msg += "\n\tReceiver class JMLValueToValueMap"; msg += "\n\tArgument pair: " + this.pair; return msg; } } /** Add tests for the isaFunction method * to the overall test suite. */ private void addTestSuiteFor$TestIsaFunction (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isaFunction"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("isaFunction", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"isaFunction\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestIsaFunction(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isaFunction method. */ protected static class TestIsaFunction extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestIsaFunction(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("isaFunction"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isaFunction(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isaFunction' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the apply method * to the overall test suite. */ private void addTestSuiteFor$TestApply (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("apply"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("apply", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"apply\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("apply", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"apply\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType dv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestApply(receiver$, dv)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the apply method. */ protected static class TestApply extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument dv */ private org.jmlspecs.models.JMLType dv; /** Initialize this instance. */ public TestApply(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType dv) { super("apply"+ ":" + (dv==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.dv = dv; } protected void doCall() throws java.lang.Throwable { receiver$.apply(dv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'apply' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument dv: " + this.dv; return msg; } } /** Add tests for the clone method * to the overall test suite. */ private void addTestSuiteFor$TestClone (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("clone"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestClone(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the clone method. */ protected static class TestClone extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("clone"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.clone(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'clone' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the extend method * to the overall test suite. */ private void addTestSuiteFor$TestExtend (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("extend"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("extend", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"extend\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("extend", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"extend\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("extend", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"extend\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType dv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType rv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestExtend(receiver$, dv, rv)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the extend method. */ protected static class TestExtend extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument dv */ private org.jmlspecs.models.JMLType dv; /** Argument rv */ private org.jmlspecs.models.JMLType rv; /** Initialize this instance. */ public TestExtend(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType dv, org.jmlspecs.models.JMLType rv) { super("extend"+ ":" + (dv==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(rv==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { receiver$.extend(dv, rv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'extend' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; return msg; } } /** Add tests for the removeDomainElement method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveDomainElement (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeDomainElement"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("removeDomainElement", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"removeDomainElement\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("removeDomainElement", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"removeDomainElement\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType dv = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestRemoveDomainElement(receiver$, dv)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeDomainElement method. */ protected static class TestRemoveDomainElement extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument dv */ private org.jmlspecs.models.JMLType dv; /** Initialize this instance. */ public TestRemoveDomainElement(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType dv) { super("removeDomainElement"+ ":" + (dv==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.dv = dv; } protected void doCall() throws java.lang.Throwable { receiver$.removeDomainElement(dv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeDomainElement' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument dv: " + this.dv; return msg; } } /** Add tests for the compose method * to the overall test suite. */ private void addTestSuiteFor$TestCompose (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compose"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueMap$1$iter = this.vorg_jmlspecs_models_JMLValueToValueMapIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueMap$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueMap$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueMap othMap = (org.jmlspecs.models.JMLValueToValueMap) vorg_jmlspecs_models_JMLValueToValueMap$1$iter.get(); methodTests$.addTest (new TestCompose(receiver$, othMap)); vorg_jmlspecs_models_JMLValueToValueMap$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compose method. */ protected static class TestCompose extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument othMap */ private org.jmlspecs.models.JMLValueToValueMap othMap; /** Initialize this instance. */ public TestCompose(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueMap othMap) { super("compose"+ ":" + (othMap==null? "null" :"{org.jmlspecs.models.JMLValueToValueMap}")); this.receiver$ = receiver$; this.othMap = othMap; } protected void doCall() throws java.lang.Throwable { receiver$.compose(othMap); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compose' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument othMap: " + this.othMap; return msg; } } /** Add tests for the compose method * to the overall test suite. */ private void addTestSuiteFor$TestCompose$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compose"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToValueMap$1$iter = this.vorg_jmlspecs_models_JMLObjectToValueMapIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToValueMap$1$iter, "this.vorg_jmlspecs_models_JMLObjectToValueMapIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToValueMap$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToValueMap othMap = (org.jmlspecs.models.JMLObjectToValueMap) vorg_jmlspecs_models_JMLObjectToValueMap$1$iter.get(); methodTests$.addTest (new TestCompose$1(receiver$, othMap)); vorg_jmlspecs_models_JMLObjectToValueMap$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compose method. */ protected static class TestCompose$1 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument othMap */ private org.jmlspecs.models.JMLObjectToValueMap othMap; /** Initialize this instance. */ public TestCompose$1(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLObjectToValueMap othMap) { super("compose"+ ":" + (othMap==null? "null" :"{org.jmlspecs.models.JMLObjectToValueMap}")); this.receiver$ = receiver$; this.othMap = othMap; } protected void doCall() throws java.lang.Throwable { receiver$.compose(othMap); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compose' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument othMap: " + this.othMap; return msg; } } /** Add tests for the restrictedTo method * to the overall test suite. */ private void addTestSuiteFor$TestRestrictedTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("restrictedTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("restrictedTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"restrictedTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("restrictedTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"restrictedTo\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet dom = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestRestrictedTo(receiver$, dom)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the restrictedTo method. */ protected static class TestRestrictedTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument dom */ private org.jmlspecs.models.JMLValueSet dom; /** Initialize this instance. */ public TestRestrictedTo(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet dom) { super("restrictedTo"+ ":" + (dom==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.dom = dom; } protected void doCall() throws java.lang.Throwable { receiver$.restrictedTo(dom); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'restrictedTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument dom: " + this.dom; return msg; } } /** Add tests for the rangeRestrictedTo method * to the overall test suite. */ private void addTestSuiteFor$TestRangeRestrictedTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("rangeRestrictedTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("rangeRestrictedTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"rangeRestrictedTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("rangeRestrictedTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"rangeRestrictedTo\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet rng = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestRangeRestrictedTo(receiver$, rng)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the rangeRestrictedTo method. */ protected static class TestRangeRestrictedTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument rng */ private org.jmlspecs.models.JMLValueSet rng; /** Initialize this instance. */ public TestRangeRestrictedTo(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet rng) { super("rangeRestrictedTo"+ ":" + (rng==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.rng = rng; } protected void doCall() throws java.lang.Throwable { receiver$.rangeRestrictedTo(rng); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'rangeRestrictedTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument rng: " + this.rng; return msg; } } /** Add tests for the extendUnion method * to the overall test suite. */ private void addTestSuiteFor$TestExtendUnion (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("extendUnion"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("extendUnion", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"extendUnion\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueMap$1$iter = this.vorg_jmlspecs_models_JMLValueToValueMapIter("extendUnion", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueMap$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"extendUnion\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueMap$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueMap othMap = (org.jmlspecs.models.JMLValueToValueMap) vorg_jmlspecs_models_JMLValueToValueMap$1$iter.get(); methodTests$.addTest (new TestExtendUnion(receiver$, othMap)); vorg_jmlspecs_models_JMLValueToValueMap$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the extendUnion method. */ protected static class TestExtendUnion extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument othMap */ private org.jmlspecs.models.JMLValueToValueMap othMap; /** Initialize this instance. */ public TestExtendUnion(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueMap othMap) { super("extendUnion"+ ":" + (othMap==null? "null" :"{org.jmlspecs.models.JMLValueToValueMap}")); this.receiver$ = receiver$; this.othMap = othMap; } protected void doCall() throws java.lang.Throwable { receiver$.extendUnion(othMap); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'extendUnion' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument othMap: " + this.othMap; return msg; } } /** Add tests for the clashReplaceUnion method * to the overall test suite. */ private void addTestSuiteFor$TestClashReplaceUnion (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("clashReplaceUnion"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("clashReplaceUnion", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"clashReplaceUnion\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueMap$1$iter = this.vorg_jmlspecs_models_JMLValueToValueMapIter("clashReplaceUnion", 1); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueMap$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"clashReplaceUnion\", 1)"); while (!vorg_jmlspecs_models_JMLValueToValueMap$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("clashReplaceUnion", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"clashReplaceUnion\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueMap othMap = (org.jmlspecs.models.JMLValueToValueMap) vorg_jmlspecs_models_JMLValueToValueMap$1$iter.get(); final org.jmlspecs.models.JMLType errval = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestClashReplaceUnion(receiver$, othMap, errval)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLValueToValueMap$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the clashReplaceUnion method. */ protected static class TestClashReplaceUnion extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument othMap */ private org.jmlspecs.models.JMLValueToValueMap othMap; /** Argument errval */ private org.jmlspecs.models.JMLType errval; /** Initialize this instance. */ public TestClashReplaceUnion(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueMap othMap, org.jmlspecs.models.JMLType errval) { super("clashReplaceUnion"+ ":" + (othMap==null? "null" :"{org.jmlspecs.models.JMLValueToValueMap}")+ "," +(errval==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.othMap = othMap; this.errval = errval; } protected void doCall() throws java.lang.Throwable { receiver$.clashReplaceUnion(othMap, errval); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'clashReplaceUnion' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument othMap: " + this.othMap; msg += "\n\tArgument errval: " + this.errval; return msg; } } /** Add tests for the disjointUnion method * to the overall test suite. */ private void addTestSuiteFor$TestDisjointUnion (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("disjointUnion"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("disjointUnion", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"disjointUnion\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueMap$1$iter = this.vorg_jmlspecs_models_JMLValueToValueMapIter("disjointUnion", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueMap$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"disjointUnion\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueMap$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueMap othMap = (org.jmlspecs.models.JMLValueToValueMap) vorg_jmlspecs_models_JMLValueToValueMap$1$iter.get(); methodTests$.addTest (new TestDisjointUnion(receiver$, othMap)); vorg_jmlspecs_models_JMLValueToValueMap$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the disjointUnion method. */ protected static class TestDisjointUnion extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument othMap */ private org.jmlspecs.models.JMLValueToValueMap othMap; /** Initialize this instance. */ public TestDisjointUnion(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueMap othMap) { super("disjointUnion"+ ":" + (othMap==null? "null" :"{org.jmlspecs.models.JMLValueToValueMap}")); this.receiver$ = receiver$; this.othMap = othMap; } protected void doCall() throws java.lang.Throwable { receiver$.disjointUnion(othMap); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'disjointUnion' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument othMap: " + this.othMap; return msg; } } /** Add tests for the elementImage method * to the overall test suite. */ private void addTestSuiteFor$TestElementImage (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("elementImage"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("elementImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"elementImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("elementImage", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"elementImage\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestElementImage(receiver$, arg1)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the elementImage method. */ protected static class TestElementImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Initialize this instance. */ public TestElementImage(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1) { super("elementImage"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.elementImage(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'elementImage' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the image method * to the overall test suite. */ private void addTestSuiteFor$TestImage (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("image"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("image", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"image\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("image", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"image\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet arg1 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestImage(receiver$, arg1)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the image method. */ protected static class TestImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueSet arg1; /** Initialize this instance. */ public TestImage(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet arg1) { super("image"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.image(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'image' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the inverse method * to the overall test suite. */ private void addTestSuiteFor$TestInverse (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("inverse"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("inverse", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"inverse\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestInverse(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the inverse method. */ protected static class TestInverse extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestInverse(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("inverse"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.inverse(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'inverse' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the inverseElementImage method * to the overall test suite. */ private void addTestSuiteFor$TestInverseElementImage (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("inverseElementImage"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("inverseElementImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"inverseElementImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("inverseElementImage", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"inverseElementImage\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestInverseElementImage(receiver$, arg1)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the inverseElementImage method. */ protected static class TestInverseElementImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Initialize this instance. */ public TestInverseElementImage(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1) { super("inverseElementImage"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.inverseElementImage(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'inverseElementImage' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the inverseImage method * to the overall test suite. */ private void addTestSuiteFor$TestInverseImage (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("inverseImage"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("inverseImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"inverseImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("inverseImage", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"inverseImage\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet arg1 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestInverseImage(receiver$, arg1)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the inverseImage method. */ protected static class TestInverseImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueSet arg1; /** Initialize this instance. */ public TestInverseImage(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet arg1) { super("inverseImage"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.inverseImage(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'inverseImage' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the isDefinedAt method * to the overall test suite. */ private void addTestSuiteFor$TestIsDefinedAt (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isDefinedAt"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("isDefinedAt", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"isDefinedAt\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("isDefinedAt", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"isDefinedAt\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestIsDefinedAt(receiver$, arg1)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isDefinedAt method. */ protected static class TestIsDefinedAt extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Initialize this instance. */ public TestIsDefinedAt(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1) { super("isDefinedAt"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.isDefinedAt(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isDefinedAt' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the has method * to the overall test suite. */ private void addTestSuiteFor$TestHas (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("has"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("has", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"has\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("has", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"has\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("has", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"has\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType arg2 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestHas(receiver$, arg1, arg2)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the has method. */ protected static class TestHas extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Argument arg2 */ private org.jmlspecs.models.JMLType arg2; /** Initialize this instance. */ public TestHas(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1, org.jmlspecs.models.JMLType arg2) { super("has"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.has(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'has' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the has method * to the overall test suite. */ private void addTestSuiteFor$TestHas$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("has"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("has", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"has\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePair$1$iter = this.vorg_jmlspecs_models_JMLValueValuePairIter("has", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueValuePair$1$iter, "this.vorg_jmlspecs_models_JMLValueValuePairIter(\"has\", 0)"); while (!vorg_jmlspecs_models_JMLValueValuePair$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueValuePair arg1 = (org.jmlspecs.models.JMLValueValuePair) vorg_jmlspecs_models_JMLValueValuePair$1$iter.get(); methodTests$.addTest (new TestHas$1(receiver$, arg1)); vorg_jmlspecs_models_JMLValueValuePair$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the has method. */ protected static class TestHas$1 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueValuePair arg1; /** Initialize this instance. */ public TestHas$1(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueValuePair arg1) { super("has"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueValuePair}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.has(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'has' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the has method * to the overall test suite. */ private void addTestSuiteFor$TestHas$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("has"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("has", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"has\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("has", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"has\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final java.lang.Object arg1 = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestHas$2(receiver$, arg1)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the has method. */ protected static class TestHas$2 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private java.lang.Object arg1; /** Initialize this instance. */ public TestHas$2(org.jmlspecs.models.JMLValueToValueMap receiver$, java.lang.Object arg1) { super("has"+ ":" + (arg1==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.has(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'has' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the isEmpty method * to the overall test suite. */ private void addTestSuiteFor$TestIsEmpty (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isEmpty"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("isEmpty", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"isEmpty\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestIsEmpty(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isEmpty method. */ protected static class TestIsEmpty extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestIsEmpty(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("isEmpty"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isEmpty(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isEmpty' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the equals method * to the overall test suite. */ private void addTestSuiteFor$TestEquals (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("equals"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"equals\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("equals", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"equals\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final java.lang.Object arg1 = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestEquals(receiver$, arg1)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the equals method. */ protected static class TestEquals extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private java.lang.Object arg1; /** Initialize this instance. */ public TestEquals(org.jmlspecs.models.JMLValueToValueMap receiver$, java.lang.Object arg1) { super("equals"+ ":" + (arg1==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.equals(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'equals' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the hashCode method * to the overall test suite. */ private void addTestSuiteFor$TestHashCode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("hashCode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestHashCode(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the hashCode method. */ protected static class TestHashCode extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("hashCode"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.hashCode(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'hashCode' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the domain method * to the overall test suite. */ private void addTestSuiteFor$TestDomain (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("domain"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("domain", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"domain\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestDomain(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the domain method. */ protected static class TestDomain extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestDomain(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("domain"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.domain(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'domain' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the range method * to the overall test suite. */ private void addTestSuiteFor$TestRange (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("range"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("range", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"range\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestRange(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the range method. */ protected static class TestRange extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestRange(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("range"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.range(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'range' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the add method * to the overall test suite. */ private void addTestSuiteFor$TestAdd (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("add"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("add", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"add\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("add", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"add\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("add", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"add\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType arg2 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestAdd(receiver$, arg1, arg2)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the add method. */ protected static class TestAdd extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Argument arg2 */ private org.jmlspecs.models.JMLType arg2; /** Initialize this instance. */ public TestAdd(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1, org.jmlspecs.models.JMLType arg2) { super("add"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.add(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'add' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the insert method * to the overall test suite. */ private void addTestSuiteFor$TestInsert (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("insert"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("insert", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"insert\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePair$1$iter = this.vorg_jmlspecs_models_JMLValueValuePairIter("insert", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueValuePair$1$iter, "this.vorg_jmlspecs_models_JMLValueValuePairIter(\"insert\", 0)"); while (!vorg_jmlspecs_models_JMLValueValuePair$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueValuePair arg1 = (org.jmlspecs.models.JMLValueValuePair) vorg_jmlspecs_models_JMLValueValuePair$1$iter.get(); methodTests$.addTest (new TestInsert(receiver$, arg1)); vorg_jmlspecs_models_JMLValueValuePair$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the insert method. */ protected static class TestInsert extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueValuePair arg1; /** Initialize this instance. */ public TestInsert(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueValuePair arg1) { super("insert"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueValuePair}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.insert(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'insert' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the removeFromDomain method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveFromDomain (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeFromDomain"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("removeFromDomain", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"removeFromDomain\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("removeFromDomain", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"removeFromDomain\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestRemoveFromDomain(receiver$, arg1)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeFromDomain method. */ protected static class TestRemoveFromDomain extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Initialize this instance. */ public TestRemoveFromDomain(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1) { super("removeFromDomain"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.removeFromDomain(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeFromDomain' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the remove method * to the overall test suite. */ private void addTestSuiteFor$TestRemove (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("remove"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("remove", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"remove\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("remove", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"remove\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("remove", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"remove\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLType arg1 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLType arg2 = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestRemove(receiver$, arg1, arg2)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the remove method. */ protected static class TestRemove extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLType arg1; /** Argument arg2 */ private org.jmlspecs.models.JMLType arg2; /** Initialize this instance. */ public TestRemove(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLType arg1, org.jmlspecs.models.JMLType arg2) { super("remove"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.remove(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'remove' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the remove method * to the overall test suite. */ private void addTestSuiteFor$TestRemove$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("remove"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("remove", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"remove\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueValuePair$1$iter = this.vorg_jmlspecs_models_JMLValueValuePairIter("remove", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueValuePair$1$iter, "this.vorg_jmlspecs_models_JMLValueValuePairIter(\"remove\", 0)"); while (!vorg_jmlspecs_models_JMLValueValuePair$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueValuePair arg1 = (org.jmlspecs.models.JMLValueValuePair) vorg_jmlspecs_models_JMLValueValuePair$1$iter.get(); methodTests$.addTest (new TestRemove$1(receiver$, arg1)); vorg_jmlspecs_models_JMLValueValuePair$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the remove method. */ protected static class TestRemove$1 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueValuePair arg1; /** Initialize this instance. */ public TestRemove$1(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueValuePair arg1) { super("remove"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueValuePair}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.remove(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'remove' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the compose method * to the overall test suite. */ private void addTestSuiteFor$TestCompose$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compose"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueRelation$1$iter = this.vorg_jmlspecs_models_JMLValueToValueRelationIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueRelation$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueRelationIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueRelation arg1 = (org.jmlspecs.models.JMLValueToValueRelation) vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.get(); methodTests$.addTest (new TestCompose$2(receiver$, arg1)); vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compose method. */ protected static class TestCompose$2 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueToValueRelation arg1; /** Initialize this instance. */ public TestCompose$2(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueRelation arg1) { super("compose"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueToValueRelation}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.compose(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compose' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the compose method * to the overall test suite. */ private void addTestSuiteFor$TestCompose$3 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compose"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToValueRelation$1$iter = this.vorg_jmlspecs_models_JMLObjectToValueRelationIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToValueRelation$1$iter, "this.vorg_jmlspecs_models_JMLObjectToValueRelationIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToValueRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToValueRelation arg1 = (org.jmlspecs.models.JMLObjectToValueRelation) vorg_jmlspecs_models_JMLObjectToValueRelation$1$iter.get(); methodTests$.addTest (new TestCompose$3(receiver$, arg1)); vorg_jmlspecs_models_JMLObjectToValueRelation$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compose method. */ protected static class TestCompose$3 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLObjectToValueRelation arg1; /** Initialize this instance. */ public TestCompose$3(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLObjectToValueRelation arg1) { super("compose"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLObjectToValueRelation}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.compose(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compose' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the union method * to the overall test suite. */ private void addTestSuiteFor$TestUnion (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("union"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("union", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"union\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueRelation$1$iter = this.vorg_jmlspecs_models_JMLValueToValueRelationIter("union", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueRelation$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueRelationIter(\"union\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueRelation arg1 = (org.jmlspecs.models.JMLValueToValueRelation) vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.get(); methodTests$.addTest (new TestUnion(receiver$, arg1)); vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the union method. */ protected static class TestUnion extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueToValueRelation arg1; /** Initialize this instance. */ public TestUnion(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueRelation arg1) { super("union"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueToValueRelation}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.union(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'union' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the intersection method * to the overall test suite. */ private void addTestSuiteFor$TestIntersection (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("intersection"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("intersection", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"intersection\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueRelation$1$iter = this.vorg_jmlspecs_models_JMLValueToValueRelationIter("intersection", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueRelation$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueRelationIter(\"intersection\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueRelation arg1 = (org.jmlspecs.models.JMLValueToValueRelation) vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.get(); methodTests$.addTest (new TestIntersection(receiver$, arg1)); vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the intersection method. */ protected static class TestIntersection extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueToValueRelation arg1; /** Initialize this instance. */ public TestIntersection(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueRelation arg1) { super("intersection"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueToValueRelation}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.intersection(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'intersection' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the difference method * to the overall test suite. */ private void addTestSuiteFor$TestDifference (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("difference"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("difference", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"difference\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToValueRelation$1$iter = this.vorg_jmlspecs_models_JMLValueToValueRelationIter("difference", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToValueRelation$1$iter, "this.vorg_jmlspecs_models_JMLValueToValueRelationIter(\"difference\", 0)"); while (!vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueToValueRelation arg1 = (org.jmlspecs.models.JMLValueToValueRelation) vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.get(); methodTests$.addTest (new TestDifference(receiver$, arg1)); vorg_jmlspecs_models_JMLValueToValueRelation$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the difference method. */ protected static class TestDifference extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueToValueRelation arg1; /** Initialize this instance. */ public TestDifference(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueToValueRelation arg1) { super("difference"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueToValueRelation}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.difference(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'difference' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the restrictDomainTo method * to the overall test suite. */ private void addTestSuiteFor$TestRestrictDomainTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("restrictDomainTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("restrictDomainTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"restrictDomainTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("restrictDomainTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"restrictDomainTo\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet arg1 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestRestrictDomainTo(receiver$, arg1)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the restrictDomainTo method. */ protected static class TestRestrictDomainTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueSet arg1; /** Initialize this instance. */ public TestRestrictDomainTo(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet arg1) { super("restrictDomainTo"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.restrictDomainTo(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'restrictDomainTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the restrictRangeTo method * to the overall test suite. */ private void addTestSuiteFor$TestRestrictRangeTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("restrictRangeTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("restrictRangeTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"restrictRangeTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueSet$1$iter = this.vorg_jmlspecs_models_JMLValueSetIter("restrictRangeTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueSet$1$iter, "this.vorg_jmlspecs_models_JMLValueSetIter(\"restrictRangeTo\", 0)"); while (!vorg_jmlspecs_models_JMLValueSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); final org.jmlspecs.models.JMLValueSet arg1 = (org.jmlspecs.models.JMLValueSet) vorg_jmlspecs_models_JMLValueSet$1$iter.get(); methodTests$.addTest (new TestRestrictRangeTo(receiver$, arg1)); vorg_jmlspecs_models_JMLValueSet$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the restrictRangeTo method. */ protected static class TestRestrictRangeTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Argument arg1 */ private org.jmlspecs.models.JMLValueSet arg1; /** Initialize this instance. */ public TestRestrictRangeTo(org.jmlspecs.models.JMLValueToValueMap receiver$, org.jmlspecs.models.JMLValueSet arg1) { super("restrictRangeTo"+ ":" + (arg1==null? "null" :"{org.jmlspecs.models.JMLValueSet}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.restrictRangeTo(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'restrictRangeTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the toString method * to the overall test suite. */ private void addTestSuiteFor$TestToString (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toString"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestToString(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toString method. */ protected static class TestToString extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("toString"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toString(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toString' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the associations method * to the overall test suite. */ private void addTestSuiteFor$TestAssociations (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("associations"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("associations", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"associations\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestAssociations(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the associations method. */ protected static class TestAssociations extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestAssociations(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("associations"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.associations(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'associations' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the elements method * to the overall test suite. */ private void addTestSuiteFor$TestElements (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("elements"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("elements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"elements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestElements(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the elements method. */ protected static class TestElements extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestElements(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("elements"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.elements(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'elements' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the iterator method * to the overall test suite. */ private void addTestSuiteFor$TestIterator (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("iterator"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("iterator", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"iterator\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestIterator(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the iterator method. */ protected static class TestIterator extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestIterator(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("iterator"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.iterator(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'iterator' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the toSet method * to the overall test suite. */ private void addTestSuiteFor$TestToSet (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toSet"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("toSet", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"toSet\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestToSet(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toSet method. */ protected static class TestToSet extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestToSet(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("toSet"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toSet(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toSet' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the toBag method * to the overall test suite. */ private void addTestSuiteFor$TestToBag (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toBag"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("toBag", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"toBag\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestToBag(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toBag method. */ protected static class TestToBag extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestToBag(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("toBag"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toBag(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toBag' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the toSequence method * to the overall test suite. */ private void addTestSuiteFor$TestToSequence (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toSequence"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("toSequence", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"toSequence\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestToSequence(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toSequence method. */ protected static class TestToSequence extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestToSequence(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("toSequence"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toSequence(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toSequence' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the imagePairSet method * to the overall test suite. */ private void addTestSuiteFor$TestImagePairSet (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("imagePairSet"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("imagePairSet", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"imagePairSet\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestImagePairSet(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the imagePairSet method. */ protected static class TestImagePairSet extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestImagePairSet(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("imagePairSet"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.imagePairSet(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'imagePairSet' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the imagePairs method * to the overall test suite. */ private void addTestSuiteFor$TestImagePairs (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("imagePairs"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("imagePairs", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"imagePairs\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestImagePairs(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the imagePairs method. */ protected static class TestImagePairs extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestImagePairs(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("imagePairs"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.imagePairs(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'imagePairs' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the domainElements method * to the overall test suite. */ private void addTestSuiteFor$TestDomainElements (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("domainElements"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("domainElements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"domainElements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestDomainElements(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the domainElements method. */ protected static class TestDomainElements extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestDomainElements(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("domainElements"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.domainElements(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'domainElements' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the rangeElements method * to the overall test suite. */ private void addTestSuiteFor$TestRangeElements (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("rangeElements"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("rangeElements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"rangeElements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestRangeElements(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the rangeElements method. */ protected static class TestRangeElements extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestRangeElements(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("rangeElements"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.rangeElements(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'rangeElements' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the int_size method * to the overall test suite. */ private void addTestSuiteFor$TestInt_size (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("int_size"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("int_size", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"int_size\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestInt_size(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the int_size method. */ protected static class TestInt_size extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestInt_size(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("int_size"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.int_size(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'int_size' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the toFunction method * to the overall test suite. */ private void addTestSuiteFor$TestToFunction (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toFunction"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLValueToValueMapIter("toFunction", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLValueToValueMapIter(\"toFunction\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLValueToValueMap receiver$ = (org.jmlspecs.models.JMLValueToValueMap) receivers$iter.get(); methodTests$.addTest (new TestToFunction(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toFunction method. */ protected static class TestToFunction extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLValueToValueMap receiver$; /** Initialize this instance. */ public TestToFunction(org.jmlspecs.models.JMLValueToValueMap receiver$) { super("toFunction"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toFunction(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toFunction' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Check that the iterator is non-null and not empty. */ private void check_has_data(org.jmlspecs.jmlunit.strategies.IndefiniteIterator iter, String call) { if (iter == null) { junit.framework.Assert.fail(call + " returned null"); } if (iter.atEnd()) { junit.framework.Assert.fail(call + " returned an empty iterator"); } } /** Converts a char to a printable String for display */ public static String charToString(char c) { if (c == '\n') { return "NL"; } else if (c == '\r') { return "CR"; } else if (c == '\t') { return "TAB"; } else if (Character.isISOControl(c)) { int i = (int)c; return "\\u" + Character.forDigit((i/2048)%16,16) + Character.forDigit((i/256)%16,16) + Character.forDigit((i/16)%16,16) + Character.forDigit((i)%16,16); } return Character.toString(c); } }