// 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 JMLObjectToObjectRelation. 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 JMLObjectToObjectRelation.java ** to regenerate this class whenever JMLObjectToObjectRelation.java changes. */ public class JMLObjectToObjectRelation_JML_Test extends JMLObjectToObjectRelation_JML_TestData { /** Initialize this class. */ public JMLObjectToObjectRelation_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 JMLObjectToObjectRelation * 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 JMLObjectToObjectRelation" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLObjectToObjectRelation.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() { JMLObjectToObjectRelation_JML_Test testobj = new JMLObjectToObjectRelation_JML_Test("JMLObjectToObjectRelation_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(JMLObjectToObjectRelation_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 JMLObjectToObjectRelation_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 * JMLObjectToObjectRelation. 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$TestJMLObjectToObjectRelation(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLObjectToObjectRelation$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLObjectToObjectRelation$2(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSingleton(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestSingleton$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$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$TestClone(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(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$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 JMLObjectToObjectRelation contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLObjectToObjectRelation (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLObjectToObjectRelation"); try { methodTests$.addTest (new TestJMLObjectToObjectRelation()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLObjectToObjectRelation contructor. */ protected static class TestJMLObjectToObjectRelation extends OneTest { /** Initialize this instance. */ public TestJMLObjectToObjectRelation() { super("JMLObjectToObjectRelation"); } protected void doCall() throws java.lang.Throwable { new JMLObjectToObjectRelation(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLObjectToObjectRelation'"; return msg; } } /** Add tests for the JMLObjectToObjectRelation contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLObjectToObjectRelation$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLObjectToObjectRelation"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("JMLObjectToObjectRelation", 1); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"JMLObjectToObjectRelation\", 1)"); while (!vjava_lang_Object$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$2$iter = this.vjava_lang_ObjectIter("JMLObjectToObjectRelation", 0); this.check_has_data (vjava_lang_Object$2$iter, "this.vjava_lang_ObjectIter(\"JMLObjectToObjectRelation\", 0)"); while (!vjava_lang_Object$2$iter.atEnd()) { final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$2$iter.get(); methodTests$.addTest (new TestJMLObjectToObjectRelation$1(dv, rv)); vjava_lang_Object$2$iter.advance(); } vjava_lang_Object$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLObjectToObjectRelation contructor. */ protected static class TestJMLObjectToObjectRelation$1 extends OneTest { /** Argument dv */ private java.lang.Object dv; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestJMLObjectToObjectRelation$1(java.lang.Object dv, java.lang.Object rv) { super("JMLObjectToObjectRelation"+ ":" + (dv==null? "null" :"{java.lang.Object}")+ "," +(rv==null? "null" :"{java.lang.Object}")); this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { new JMLObjectToObjectRelation(dv, rv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLObjectToObjectRelation' applied to"; msg += "\n\tArgument dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; return msg; } } /** Add tests for the JMLObjectToObjectRelation contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLObjectToObjectRelation$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLObjectToObjectRelation"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPair$1$iter = this.vorg_jmlspecs_models_JMLObjectObjectPairIter("JMLObjectToObjectRelation", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectObjectPair$1$iter, "this.vorg_jmlspecs_models_JMLObjectObjectPairIter(\"JMLObjectToObjectRelation\", 0)"); while (!vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectObjectPair pair = (org.jmlspecs.models.JMLObjectObjectPair) vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.get(); methodTests$.addTest (new TestJMLObjectToObjectRelation$2(pair)); vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLObjectToObjectRelation contructor. */ protected static class TestJMLObjectToObjectRelation$2 extends OneTest { /** Argument pair */ private org.jmlspecs.models.JMLObjectObjectPair pair; /** Initialize this instance. */ public TestJMLObjectToObjectRelation$2(org.jmlspecs.models.JMLObjectObjectPair pair) { super("JMLObjectToObjectRelation"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLObjectObjectPair}")); this.pair = pair; } protected void doCall() throws java.lang.Throwable { new JMLObjectToObjectRelation(pair); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLObjectToObjectRelation' applied to"; msg += "\n\tArgument pair: " + this.pair; return msg; } } /** Add tests for the singleton method * to the overall test suite. */ private void addTestSuiteFor$TestSingleton (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("singleton"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("singleton", 1); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"singleton\", 1)"); while (!vjava_lang_Object$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$2$iter = this.vjava_lang_ObjectIter("singleton", 0); this.check_has_data (vjava_lang_Object$2$iter, "this.vjava_lang_ObjectIter(\"singleton\", 0)"); while (!vjava_lang_Object$2$iter.atEnd()) { final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$2$iter.get(); methodTests$.addTest (new TestSingleton(dv, rv)); vjava_lang_Object$2$iter.advance(); } vjava_lang_Object$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the singleton method. */ protected static class TestSingleton extends OneTest { /** Argument dv */ private java.lang.Object dv; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestSingleton(java.lang.Object dv, java.lang.Object rv) { super("singleton"+ ":" + (dv==null? "null" :"{java.lang.Object}")+ "," +(rv==null? "null" :"{java.lang.Object}")); this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { JMLObjectToObjectRelation.singleton(dv, rv); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'singleton' applied to"; msg += "\n\tReceiver class JMLObjectToObjectRelation"; msg += "\n\tArgument dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; return msg; } } /** Add tests for the singleton method * to the overall test suite. */ private void addTestSuiteFor$TestSingleton$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("singleton"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPair$1$iter = this.vorg_jmlspecs_models_JMLObjectObjectPairIter("singleton", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectObjectPair$1$iter, "this.vorg_jmlspecs_models_JMLObjectObjectPairIter(\"singleton\", 0)"); while (!vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectObjectPair pair = (org.jmlspecs.models.JMLObjectObjectPair) vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.get(); methodTests$.addTest (new TestSingleton$1(pair)); vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the singleton method. */ protected static class TestSingleton$1 extends OneTest { /** Argument pair */ private org.jmlspecs.models.JMLObjectObjectPair pair; /** Initialize this instance. */ public TestSingleton$1(org.jmlspecs.models.JMLObjectObjectPair pair) { super("singleton"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLObjectObjectPair}")); this.pair = pair; } protected void doCall() throws java.lang.Throwable { JMLObjectToObjectRelation.singleton(pair); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'singleton' applied to"; msg += "\n\tReceiver class JMLObjectToObjectRelation"; 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_JMLObjectToObjectRelationIter("isaFunction", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"isaFunction\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestIsaFunction(org.jmlspecs.models.JMLObjectToObjectRelation 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 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_JMLObjectToObjectRelationIter("elementImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"elementImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("elementImage", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"elementImage\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestElementImage(receiver$, dv)); 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 elementImage method. */ protected static class TestElementImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Initialize this instance. */ public TestElementImage(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv) { super("elementImage"+ ":" + (dv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; } protected void doCall() throws java.lang.Throwable { receiver$.elementImage(dv); } 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 dv: " + this.dv; 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_JMLObjectToObjectRelationIter("image", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"image\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectSet$1$iter = this.vorg_jmlspecs_models_JMLObjectSetIter("image", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectSet$1$iter, "this.vorg_jmlspecs_models_JMLObjectSetIter(\"image\", 0)"); while (!vorg_jmlspecs_models_JMLObjectSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectSet dom = (org.jmlspecs.models.JMLObjectSet) vorg_jmlspecs_models_JMLObjectSet$1$iter.get(); methodTests$.addTest (new TestImage(receiver$, dom)); vorg_jmlspecs_models_JMLObjectSet$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.JMLObjectToObjectRelation receiver$; /** Argument dom */ private org.jmlspecs.models.JMLObjectSet dom; /** Initialize this instance. */ public TestImage(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectSet dom) { super("image"+ ":" + (dom==null? "null" :"{org.jmlspecs.models.JMLObjectSet}")); this.receiver$ = receiver$; this.dom = dom; } protected void doCall() throws java.lang.Throwable { receiver$.image(dom); } 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 dom: " + this.dom; 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_JMLObjectToObjectRelationIter("inverse", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"inverse\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestInverse(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("inverseElementImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"inverseElementImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("inverseElementImage", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"inverseElementImage\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestInverseElementImage(receiver$, rv)); 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 inverseElementImage method. */ protected static class TestInverseElementImage extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestInverseElementImage(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object rv) { super("inverseElementImage"+ ":" + (rv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.rv = rv; } protected void doCall() throws java.lang.Throwable { receiver$.inverseElementImage(rv); } 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 rv: " + this.rv; 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_JMLObjectToObjectRelationIter("inverseImage", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"inverseImage\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectSet$1$iter = this.vorg_jmlspecs_models_JMLObjectSetIter("inverseImage", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectSet$1$iter, "this.vorg_jmlspecs_models_JMLObjectSetIter(\"inverseImage\", 0)"); while (!vorg_jmlspecs_models_JMLObjectSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectSet rng = (org.jmlspecs.models.JMLObjectSet) vorg_jmlspecs_models_JMLObjectSet$1$iter.get(); methodTests$.addTest (new TestInverseImage(receiver$, rng)); vorg_jmlspecs_models_JMLObjectSet$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.JMLObjectToObjectRelation receiver$; /** Argument rng */ private org.jmlspecs.models.JMLObjectSet rng; /** Initialize this instance. */ public TestInverseImage(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectSet rng) { super("inverseImage"+ ":" + (rng==null? "null" :"{org.jmlspecs.models.JMLObjectSet}")); this.receiver$ = receiver$; this.rng = rng; } protected void doCall() throws java.lang.Throwable { receiver$.inverseImage(rng); } 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 rng: " + this.rng; 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_JMLObjectToObjectRelationIter("isDefinedAt", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"isDefinedAt\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("isDefinedAt", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"isDefinedAt\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestIsDefinedAt(receiver$, dv)); 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 isDefinedAt method. */ protected static class TestIsDefinedAt extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Initialize this instance. */ public TestIsDefinedAt(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv) { super("isDefinedAt"+ ":" + (dv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; } protected void doCall() throws java.lang.Throwable { receiver$.isDefinedAt(dv); } 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 dv: " + this.dv; 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_JMLObjectToObjectRelationIter("has", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"has\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("has", 1); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"has\", 1)"); while (!vjava_lang_Object$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$2$iter = this.vjava_lang_ObjectIter("has", 0); this.check_has_data (vjava_lang_Object$2$iter, "this.vjava_lang_ObjectIter(\"has\", 0)"); while (!vjava_lang_Object$2$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$2$iter.get(); methodTests$.addTest (new TestHas(receiver$, dv, rv)); vjava_lang_Object$2$iter.advance(); } 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 extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestHas(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv, java.lang.Object rv) { super("has"+ ":" + (dv==null? "null" :"{java.lang.Object}")+ "," +(rv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { receiver$.has(dv, rv); } 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 dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; 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_JMLObjectToObjectRelationIter("has", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"has\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPair$1$iter = this.vorg_jmlspecs_models_JMLObjectObjectPairIter("has", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectObjectPair$1$iter, "this.vorg_jmlspecs_models_JMLObjectObjectPairIter(\"has\", 0)"); while (!vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectObjectPair pair = (org.jmlspecs.models.JMLObjectObjectPair) vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.get(); methodTests$.addTest (new TestHas$1(receiver$, pair)); vorg_jmlspecs_models_JMLObjectObjectPair$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.JMLObjectToObjectRelation receiver$; /** Argument pair */ private org.jmlspecs.models.JMLObjectObjectPair pair; /** Initialize this instance. */ public TestHas$1(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectObjectPair pair) { super("has"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLObjectObjectPair}")); this.receiver$ = receiver$; this.pair = pair; } protected void doCall() throws java.lang.Throwable { receiver$.has(pair); } 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 pair: " + this.pair; 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_JMLObjectToObjectRelationIter("has", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"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.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object obj = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestHas$2(receiver$, obj)); 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.JMLObjectToObjectRelation receiver$; /** Argument obj */ private java.lang.Object obj; /** Initialize this instance. */ public TestHas$2(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object obj) { super("has"+ ":" + (obj==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.obj = obj; } protected void doCall() throws java.lang.Throwable { receiver$.has(obj); } 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 obj: " + this.obj; 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_JMLObjectToObjectRelationIter("isEmpty", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"isEmpty\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestIsEmpty(org.jmlspecs.models.JMLObjectToObjectRelation 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 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_JMLObjectToObjectRelationIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.models.JMLObjectToObjectRelation 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 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_JMLObjectToObjectRelationIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"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.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object obj = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestEquals(receiver$, obj)); 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.JMLObjectToObjectRelation receiver$; /** Argument obj */ private java.lang.Object obj; /** Initialize this instance. */ public TestEquals(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object obj) { super("equals"+ ":" + (obj==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.obj = obj; } protected void doCall() throws java.lang.Throwable { receiver$.equals(obj); } 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 obj: " + this.obj; 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_JMLObjectToObjectRelationIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("domain", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"domain\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestDomain(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("range", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"range\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestRange(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("add", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"add\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("add", 1); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"add\", 1)"); while (!vjava_lang_Object$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$2$iter = this.vjava_lang_ObjectIter("add", 0); this.check_has_data (vjava_lang_Object$2$iter, "this.vjava_lang_ObjectIter(\"add\", 0)"); while (!vjava_lang_Object$2$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$2$iter.get(); methodTests$.addTest (new TestAdd(receiver$, dv, rv)); vjava_lang_Object$2$iter.advance(); } 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 add method. */ protected static class TestAdd extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestAdd(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv, java.lang.Object rv) { super("add"+ ":" + (dv==null? "null" :"{java.lang.Object}")+ "," +(rv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { receiver$.add(dv, rv); } 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 dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; 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_JMLObjectToObjectRelationIter("insert", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"insert\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPair$1$iter = this.vorg_jmlspecs_models_JMLObjectObjectPairIter("insert", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectObjectPair$1$iter, "this.vorg_jmlspecs_models_JMLObjectObjectPairIter(\"insert\", 0)"); while (!vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectObjectPair pair = (org.jmlspecs.models.JMLObjectObjectPair) vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.get(); methodTests$.addTest (new TestInsert(receiver$, pair)); vorg_jmlspecs_models_JMLObjectObjectPair$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.JMLObjectToObjectRelation receiver$; /** Argument pair */ private org.jmlspecs.models.JMLObjectObjectPair pair; /** Initialize this instance. */ public TestInsert(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectObjectPair pair) { super("insert"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLObjectObjectPair}")); this.receiver$ = receiver$; this.pair = pair; } protected void doCall() throws java.lang.Throwable { receiver$.insert(pair); } 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 pair: " + this.pair; 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_JMLObjectToObjectRelationIter("removeFromDomain", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"removeFromDomain\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("removeFromDomain", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"removeFromDomain\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestRemoveFromDomain(receiver$, dv)); 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 removeFromDomain method. */ protected static class TestRemoveFromDomain extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Initialize this instance. */ public TestRemoveFromDomain(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv) { super("removeFromDomain"+ ":" + (dv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; } protected void doCall() throws java.lang.Throwable { receiver$.removeFromDomain(dv); } 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 dv: " + this.dv; 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_JMLObjectToObjectRelationIter("remove", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"remove\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("remove", 1); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"remove\", 1)"); while (!vjava_lang_Object$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$2$iter = this.vjava_lang_ObjectIter("remove", 0); this.check_has_data (vjava_lang_Object$2$iter, "this.vjava_lang_ObjectIter(\"remove\", 0)"); while (!vjava_lang_Object$2$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final java.lang.Object dv = (java.lang.Object) vjava_lang_Object$1$iter.get(); final java.lang.Object rv = (java.lang.Object) vjava_lang_Object$2$iter.get(); methodTests$.addTest (new TestRemove(receiver$, dv, rv)); vjava_lang_Object$2$iter.advance(); } 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 remove method. */ protected static class TestRemove extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLObjectToObjectRelation receiver$; /** Argument dv */ private java.lang.Object dv; /** Argument rv */ private java.lang.Object rv; /** Initialize this instance. */ public TestRemove(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, java.lang.Object dv, java.lang.Object rv) { super("remove"+ ":" + (dv==null? "null" :"{java.lang.Object}")+ "," +(rv==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.dv = dv; this.rv = rv; } protected void doCall() throws java.lang.Throwable { receiver$.remove(dv, rv); } 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 dv: " + this.dv; msg += "\n\tArgument rv: " + this.rv; 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_JMLObjectToObjectRelationIter("remove", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"remove\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectObjectPair$1$iter = this.vorg_jmlspecs_models_JMLObjectObjectPairIter("remove", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectObjectPair$1$iter, "this.vorg_jmlspecs_models_JMLObjectObjectPairIter(\"remove\", 0)"); while (!vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectObjectPair pair = (org.jmlspecs.models.JMLObjectObjectPair) vorg_jmlspecs_models_JMLObjectObjectPair$1$iter.get(); methodTests$.addTest (new TestRemove$1(receiver$, pair)); vorg_jmlspecs_models_JMLObjectObjectPair$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.JMLObjectToObjectRelation receiver$; /** Argument pair */ private org.jmlspecs.models.JMLObjectObjectPair pair; /** Initialize this instance. */ public TestRemove$1(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectObjectPair pair) { super("remove"+ ":" + (pair==null? "null" :"{org.jmlspecs.models.JMLObjectObjectPair}")); this.receiver$ = receiver$; this.pair = pair; } protected void doCall() throws java.lang.Throwable { receiver$.remove(pair); } 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 pair: " + this.pair; 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_JMLObjectToObjectRelationIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLValueToObjectRelation$1$iter = this.vorg_jmlspecs_models_JMLValueToObjectRelationIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLValueToObjectRelation$1$iter, "this.vorg_jmlspecs_models_JMLValueToObjectRelationIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLValueToObjectRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLValueToObjectRelation othRel = (org.jmlspecs.models.JMLValueToObjectRelation) vorg_jmlspecs_models_JMLValueToObjectRelation$1$iter.get(); methodTests$.addTest (new TestCompose(receiver$, othRel)); vorg_jmlspecs_models_JMLValueToObjectRelation$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.JMLObjectToObjectRelation receiver$; /** Argument othRel */ private org.jmlspecs.models.JMLValueToObjectRelation othRel; /** Initialize this instance. */ public TestCompose(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLValueToObjectRelation othRel) { super("compose"+ ":" + (othRel==null? "null" :"{org.jmlspecs.models.JMLValueToObjectRelation}")); this.receiver$ = receiver$; this.othRel = othRel; } protected void doCall() throws java.lang.Throwable { receiver$.compose(othRel); } 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 othRel: " + this.othRel; 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_JMLObjectToObjectRelationIter("compose", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"compose\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter = this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter("compose", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter, "this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"compose\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToObjectRelation othRel = (org.jmlspecs.models.JMLObjectToObjectRelation) vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.get(); methodTests$.addTest (new TestCompose$1(receiver$, othRel)); vorg_jmlspecs_models_JMLObjectToObjectRelation$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.JMLObjectToObjectRelation receiver$; /** Argument othRel */ private org.jmlspecs.models.JMLObjectToObjectRelation othRel; /** Initialize this instance. */ public TestCompose$1(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectToObjectRelation othRel) { super("compose"+ ":" + (othRel==null? "null" :"{org.jmlspecs.models.JMLObjectToObjectRelation}")); this.receiver$ = receiver$; this.othRel = othRel; } protected void doCall() throws java.lang.Throwable { receiver$.compose(othRel); } 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 othRel: " + this.othRel; 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_JMLObjectToObjectRelationIter("union", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"union\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter = this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter("union", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter, "this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"union\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToObjectRelation othRel = (org.jmlspecs.models.JMLObjectToObjectRelation) vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.get(); methodTests$.addTest (new TestUnion(receiver$, othRel)); vorg_jmlspecs_models_JMLObjectToObjectRelation$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.JMLObjectToObjectRelation receiver$; /** Argument othRel */ private org.jmlspecs.models.JMLObjectToObjectRelation othRel; /** Initialize this instance. */ public TestUnion(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectToObjectRelation othRel) { super("union"+ ":" + (othRel==null? "null" :"{org.jmlspecs.models.JMLObjectToObjectRelation}")); this.receiver$ = receiver$; this.othRel = othRel; } protected void doCall() throws java.lang.Throwable { receiver$.union(othRel); } 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 othRel: " + this.othRel; 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_JMLObjectToObjectRelationIter("intersection", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"intersection\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter = this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter("intersection", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter, "this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"intersection\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToObjectRelation othRel = (org.jmlspecs.models.JMLObjectToObjectRelation) vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.get(); methodTests$.addTest (new TestIntersection(receiver$, othRel)); vorg_jmlspecs_models_JMLObjectToObjectRelation$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.JMLObjectToObjectRelation receiver$; /** Argument othRel */ private org.jmlspecs.models.JMLObjectToObjectRelation othRel; /** Initialize this instance. */ public TestIntersection(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectToObjectRelation othRel) { super("intersection"+ ":" + (othRel==null? "null" :"{org.jmlspecs.models.JMLObjectToObjectRelation}")); this.receiver$ = receiver$; this.othRel = othRel; } protected void doCall() throws java.lang.Throwable { receiver$.intersection(othRel); } 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 othRel: " + this.othRel; 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_JMLObjectToObjectRelationIter("difference", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"difference\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter = this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter("difference", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter, "this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"difference\", 0)"); while (!vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectToObjectRelation othRel = (org.jmlspecs.models.JMLObjectToObjectRelation) vorg_jmlspecs_models_JMLObjectToObjectRelation$1$iter.get(); methodTests$.addTest (new TestDifference(receiver$, othRel)); vorg_jmlspecs_models_JMLObjectToObjectRelation$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.JMLObjectToObjectRelation receiver$; /** Argument othRel */ private org.jmlspecs.models.JMLObjectToObjectRelation othRel; /** Initialize this instance. */ public TestDifference(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectToObjectRelation othRel) { super("difference"+ ":" + (othRel==null? "null" :"{org.jmlspecs.models.JMLObjectToObjectRelation}")); this.receiver$ = receiver$; this.othRel = othRel; } protected void doCall() throws java.lang.Throwable { receiver$.difference(othRel); } 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 othRel: " + this.othRel; 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_JMLObjectToObjectRelationIter("restrictDomainTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"restrictDomainTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectSet$1$iter = this.vorg_jmlspecs_models_JMLObjectSetIter("restrictDomainTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectSet$1$iter, "this.vorg_jmlspecs_models_JMLObjectSetIter(\"restrictDomainTo\", 0)"); while (!vorg_jmlspecs_models_JMLObjectSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectSet dom = (org.jmlspecs.models.JMLObjectSet) vorg_jmlspecs_models_JMLObjectSet$1$iter.get(); methodTests$.addTest (new TestRestrictDomainTo(receiver$, dom)); vorg_jmlspecs_models_JMLObjectSet$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.JMLObjectToObjectRelation receiver$; /** Argument dom */ private org.jmlspecs.models.JMLObjectSet dom; /** Initialize this instance. */ public TestRestrictDomainTo(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectSet dom) { super("restrictDomainTo"+ ":" + (dom==null? "null" :"{org.jmlspecs.models.JMLObjectSet}")); this.receiver$ = receiver$; this.dom = dom; } protected void doCall() throws java.lang.Throwable { receiver$.restrictDomainTo(dom); } 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 dom: " + this.dom; 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_JMLObjectToObjectRelationIter("restrictRangeTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"restrictRangeTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLObjectSet$1$iter = this.vorg_jmlspecs_models_JMLObjectSetIter("restrictRangeTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLObjectSet$1$iter, "this.vorg_jmlspecs_models_JMLObjectSetIter(\"restrictRangeTo\", 0)"); while (!vorg_jmlspecs_models_JMLObjectSet$1$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) receivers$iter.get(); final org.jmlspecs.models.JMLObjectSet rng = (org.jmlspecs.models.JMLObjectSet) vorg_jmlspecs_models_JMLObjectSet$1$iter.get(); methodTests$.addTest (new TestRestrictRangeTo(receiver$, rng)); vorg_jmlspecs_models_JMLObjectSet$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.JMLObjectToObjectRelation receiver$; /** Argument rng */ private org.jmlspecs.models.JMLObjectSet rng; /** Initialize this instance. */ public TestRestrictRangeTo(org.jmlspecs.models.JMLObjectToObjectRelation receiver$, org.jmlspecs.models.JMLObjectSet rng) { super("restrictRangeTo"+ ":" + (rng==null? "null" :"{org.jmlspecs.models.JMLObjectSet}")); this.receiver$ = receiver$; this.rng = rng; } protected void doCall() throws java.lang.Throwable { receiver$.restrictRangeTo(rng); } 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 rng: " + this.rng; 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_JMLObjectToObjectRelationIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("associations", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"associations\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestAssociations(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("elements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"elements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestElements(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("iterator", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"iterator\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestIterator(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("toSet", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"toSet\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestToSet(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("toBag", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"toBag\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestToBag(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("toSequence", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"toSequence\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestToSequence(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("imagePairSet", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"imagePairSet\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestImagePairSet(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("imagePairs", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"imagePairs\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestImagePairs(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("domainElements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"domainElements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestDomainElements(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("rangeElements", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"rangeElements\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestRangeElements(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("int_size", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"int_size\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestInt_size(org.jmlspecs.models.JMLObjectToObjectRelation 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_JMLObjectToObjectRelationIter("toFunction", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLObjectToObjectRelationIter(\"toFunction\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLObjectToObjectRelation receiver$ = (org.jmlspecs.models.JMLObjectToObjectRelation) 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.JMLObjectToObjectRelation receiver$; /** Initialize this instance. */ public TestToFunction(org.jmlspecs.models.JMLObjectToObjectRelation 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); } }