// This file was generated by jmlunit on Mon Mar 16 13:11:57 EDT 2009. package org.jmlspecs.models; /** Automatically-generated test driver for JML and JUnit based * testing of JMLChar. 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 JMLChar.java
 *
* to regenerate this class whenever JMLChar.java changes. */ public class JMLChar_JML_Test extends JMLChar_JML_TestData { /** Initialize this class. */ public JMLChar_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 JMLChar * 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 JMLChar" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLChar.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() { JMLChar_JML_Test testobj = new JMLChar_JML_Test("JMLChar_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(JMLChar_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 JMLChar_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 * JMLChar. 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$TestJMLChar(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLChar$1(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestJMLChar$2(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$TestCharValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGetChar(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$TestCompareTo(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$TestToString(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIntValue(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestPlus(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestMinus(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestTimes(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDividedBy(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemainderBy(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGreaterThan(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestLessThan(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGreaterThanOrEqualTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestLessThanOrEqualTo(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } } /** Add tests for the JMLChar contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLChar (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLChar"); try { methodTests$.addTest (new TestJMLChar()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLChar contructor. */ protected static class TestJMLChar extends OneTest { /** Initialize this instance. */ public TestJMLChar() { super("JMLChar"); } protected void doCall() throws java.lang.Throwable { new JMLChar(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLChar'"; return msg; } } /** Add tests for the JMLChar contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLChar$1 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLChar"); try { org.jmlspecs.jmlunit.strategies.CharIterator vchar$1$iter = this.vcharIter("JMLChar", 0); this.check_has_data (vchar$1$iter, "this.vcharIter(\"JMLChar\", 0)"); while (!vchar$1$iter.atEnd()) { final char c = vchar$1$iter.getChar(); methodTests$.addTest (new TestJMLChar$1(c)); vchar$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLChar contructor. */ protected static class TestJMLChar$1 extends OneTest { /** Argument c */ private char c; /** Initialize this instance. */ public TestJMLChar$1(char c) { super("JMLChar"+ ":" + "\'"+charToString(c)+"\'"); this.c = c; } protected void doCall() throws java.lang.Throwable { new JMLChar(c); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLChar' applied to"; msg += "\n\tArgument c: " + this.c; return msg; } } /** Add tests for the JMLChar contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLChar$2 (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLChar"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Character$1$iter = this.vjava_lang_CharacterIter("JMLChar", 0); this.check_has_data (vjava_lang_Character$1$iter, "this.vjava_lang_CharacterIter(\"JMLChar\", 0)"); while (!vjava_lang_Character$1$iter.atEnd()) { final java.lang.Character inChar = (java.lang.Character) vjava_lang_Character$1$iter.get(); methodTests$.addTest (new TestJMLChar$2(inChar)); vjava_lang_Character$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLChar contructor. */ protected static class TestJMLChar$2 extends OneTest { /** Argument inChar */ private java.lang.Character inChar; /** Initialize this instance. */ public TestJMLChar$2(java.lang.Character inChar) { super("JMLChar"+ ":" + (inChar==null? "null" :"{java.lang.Character}")); this.inChar = inChar; } protected void doCall() throws java.lang.Throwable { new JMLChar(inChar); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLChar' applied to"; msg += "\n\tArgument inChar: " + this.inChar; 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_JMLCharIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) 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.JMLChar receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.models.JMLChar 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 charValue method * to the overall test suite. */ private void addTestSuiteFor$TestCharValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("charValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("charValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"charValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); methodTests$.addTest (new TestCharValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the charValue method. */ protected static class TestCharValue extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Initialize this instance. */ public TestCharValue(org.jmlspecs.models.JMLChar receiver$) { super("charValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.charValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'charValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the getChar method * to the overall test suite. */ private void addTestSuiteFor$TestGetChar (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("getChar"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("getChar", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"getChar\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); methodTests$.addTest (new TestGetChar(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the getChar method. */ protected static class TestGetChar extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Initialize this instance. */ public TestGetChar(org.jmlspecs.models.JMLChar receiver$) { super("getChar"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.getChar(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'getChar' applied to"; msg += "\n\tReceiver: " + this.receiver$; 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_JMLCharIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) 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.JMLChar receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.models.JMLChar 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 compareTo method * to the overall test suite. */ private void addTestSuiteFor$TestCompareTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("compareTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("compareTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"compareTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("compareTo", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"compareTo\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final java.lang.Object op2 = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestCompareTo(receiver$, op2)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the compareTo method. */ protected static class TestCompareTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument op2 */ private java.lang.Object op2; /** Initialize this instance. */ public TestCompareTo(org.jmlspecs.models.JMLChar receiver$, java.lang.Object op2) { super("compareTo"+ ":" + (op2==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.op2 = op2; } protected void doCall() throws java.lang.Throwable { receiver$.compareTo(op2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'compareTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument op2: " + this.op2; 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_JMLCharIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"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.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) 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.JMLChar receiver$; /** Argument obj */ private java.lang.Object obj; /** Initialize this instance. */ public TestEquals(org.jmlspecs.models.JMLChar 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 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_JMLCharIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) 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.JMLChar receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.models.JMLChar 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 intValue method * to the overall test suite. */ private void addTestSuiteFor$TestIntValue (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("intValue"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("intValue", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"intValue\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); methodTests$.addTest (new TestIntValue(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the intValue method. */ protected static class TestIntValue extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Initialize this instance. */ public TestIntValue(org.jmlspecs.models.JMLChar receiver$) { super("intValue"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.intValue(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'intValue' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the plus method * to the overall test suite. */ private void addTestSuiteFor$TestPlus (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("plus"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("plus", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"plus\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("plus", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"plus\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestPlus(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 plus method. */ protected static class TestPlus extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestPlus(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("plus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.plus(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'plus' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the minus method * to the overall test suite. */ private void addTestSuiteFor$TestMinus (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("minus"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("minus", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"minus\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("minus", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"minus\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestMinus(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 minus method. */ protected static class TestMinus extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestMinus(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("minus"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.minus(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'minus' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the times method * to the overall test suite. */ private void addTestSuiteFor$TestTimes (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("times"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("times", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"times\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("times", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"times\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestTimes(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 times method. */ protected static class TestTimes extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestTimes(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("times"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.times(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'times' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the dividedBy method * to the overall test suite. */ private void addTestSuiteFor$TestDividedBy (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("dividedBy"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("dividedBy", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"dividedBy\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("dividedBy", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"dividedBy\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestDividedBy(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 dividedBy method. */ protected static class TestDividedBy extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestDividedBy(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("dividedBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.dividedBy(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'dividedBy' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the remainderBy method * to the overall test suite. */ private void addTestSuiteFor$TestRemainderBy (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("remainderBy"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("remainderBy", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"remainderBy\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("remainderBy", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"remainderBy\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestRemainderBy(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 remainderBy method. */ protected static class TestRemainderBy extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestRemainderBy(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("remainderBy"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.remainderBy(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'remainderBy' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the greaterThan method * to the overall test suite. */ private void addTestSuiteFor$TestGreaterThan (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("greaterThan"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("greaterThan", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"greaterThan\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("greaterThan", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"greaterThan\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestGreaterThan(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 greaterThan method. */ protected static class TestGreaterThan extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestGreaterThan(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("greaterThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.greaterThan(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'greaterThan' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the lessThan method * to the overall test suite. */ private void addTestSuiteFor$TestLessThan (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("lessThan"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("lessThan", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"lessThan\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("lessThan", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"lessThan\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestLessThan(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 lessThan method. */ protected static class TestLessThan extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestLessThan(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("lessThan"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.lessThan(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'lessThan' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the greaterThanOrEqualTo method * to the overall test suite. */ private void addTestSuiteFor$TestGreaterThanOrEqualTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("greaterThanOrEqualTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("greaterThanOrEqualTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"greaterThanOrEqualTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("greaterThanOrEqualTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"greaterThanOrEqualTo\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestGreaterThanOrEqualTo(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 greaterThanOrEqualTo method. */ protected static class TestGreaterThanOrEqualTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestGreaterThanOrEqualTo(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("greaterThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.greaterThanOrEqualTo(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'greaterThanOrEqualTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; return msg; } } /** Add tests for the lessThanOrEqualTo method * to the overall test suite. */ private void addTestSuiteFor$TestLessThanOrEqualTo (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("lessThanOrEqualTo"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLCharIter("lessThanOrEqualTo", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLCharIter(\"lessThanOrEqualTo\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLChar$1$iter = this.vorg_jmlspecs_models_JMLCharIter("lessThanOrEqualTo", 0); this.check_has_data (vorg_jmlspecs_models_JMLChar$1$iter, "this.vorg_jmlspecs_models_JMLCharIter(\"lessThanOrEqualTo\", 0)"); while (!vorg_jmlspecs_models_JMLChar$1$iter.atEnd()) { final org.jmlspecs.models.JMLChar receiver$ = (org.jmlspecs.models.JMLChar) receivers$iter.get(); final org.jmlspecs.models.JMLChar i2 = (org.jmlspecs.models.JMLChar) vorg_jmlspecs_models_JMLChar$1$iter.get(); methodTests$.addTest (new TestLessThanOrEqualTo(receiver$, i2)); vorg_jmlspecs_models_JMLChar$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 lessThanOrEqualTo method. */ protected static class TestLessThanOrEqualTo extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLChar receiver$; /** Argument i2 */ private org.jmlspecs.models.JMLChar i2; /** Initialize this instance. */ public TestLessThanOrEqualTo(org.jmlspecs.models.JMLChar receiver$, org.jmlspecs.models.JMLChar i2) { super("lessThanOrEqualTo"+ ":" + (i2==null? "null" :"{org.jmlspecs.models.JMLChar}")); this.receiver$ = receiver$; this.i2 = i2; } protected void doCall() throws java.lang.Throwable { receiver$.lessThanOrEqualTo(i2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'lessThanOrEqualTo' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i2: " + this.i2; 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); } }