// 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 JMLListValueNode. 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 JMLListValueNode.java ** to regenerate this class whenever JMLListValueNode.java changes. */ public class JMLListValueNode_JML_Test extends JMLListValueNode_JML_TestData { /** Initialize this class. */ public JMLListValueNode_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 JMLListValueNode * 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 JMLListValueNode" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(JMLListValueNode.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() { JMLListValueNode_JML_Test testobj = new JMLListValueNode_JML_Test("JMLListValueNode_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(JMLListValueNode_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 JMLListValueNode_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 * JMLListValueNode. 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$TestJMLListValueNode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestCons(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHead(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHeadEquals(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestItemAt(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$TestInt_length(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$TestIsPrefixOf(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$TestIndexOf(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestLast(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGetItem(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$TestPrefix(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemovePrefix(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveItemAt(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestReplaceItemAt(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveLast(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestConcat(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestPrepend(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAppend(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestReverse(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInsertBefore(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$TestToString(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } } /** Add tests for the JMLListValueNode contructor * to the overall test suite. */ private void addTestSuiteFor$TestJMLListValueNode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("JMLListValueNode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("JMLListValueNode", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"JMLListValueNode\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLListValueNode$2$iter = this.vorg_jmlspecs_models_JMLListValueNodeIter("JMLListValueNode", 0); this.check_has_data (vorg_jmlspecs_models_JMLListValueNode$2$iter, "this.vorg_jmlspecs_models_JMLListValueNodeIter(\"JMLListValueNode\", 0)"); while (!vorg_jmlspecs_models_JMLListValueNode$2$iter.atEnd()) { final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLListValueNode nxt = (org.jmlspecs.models.JMLListValueNode) vorg_jmlspecs_models_JMLListValueNode$2$iter.get(); methodTests$.addTest (new TestJMLListValueNode(item, nxt)); vorg_jmlspecs_models_JMLListValueNode$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the JMLListValueNode contructor. */ protected static class TestJMLListValueNode extends OneTest { /** Argument item */ private org.jmlspecs.models.JMLType item; /** Argument nxt */ private org.jmlspecs.models.JMLListValueNode nxt; /** Initialize this instance. */ public TestJMLListValueNode(org.jmlspecs.models.JMLType item, org.jmlspecs.models.JMLListValueNode nxt) { super("JMLListValueNode"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(nxt==null? "null" :"{org.jmlspecs.models.JMLListValueNode}")); this.item = item; this.nxt = nxt; } protected void doCall() throws java.lang.Throwable { new JMLListValueNode(item, nxt); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'JMLListValueNode' applied to"; msg += "\n\tArgument item: " + this.item; msg += "\n\tArgument nxt: " + this.nxt; return msg; } } /** Add tests for the cons method * to the overall test suite. */ private void addTestSuiteFor$TestCons (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("cons"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("cons", 1); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"cons\", 1)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLListValueNode$2$iter = this.vorg_jmlspecs_models_JMLListValueNodeIter("cons", 0); this.check_has_data (vorg_jmlspecs_models_JMLListValueNode$2$iter, "this.vorg_jmlspecs_models_JMLListValueNodeIter(\"cons\", 0)"); while (!vorg_jmlspecs_models_JMLListValueNode$2$iter.atEnd()) { final org.jmlspecs.models.JMLType hd = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); final org.jmlspecs.models.JMLListValueNode tl = (org.jmlspecs.models.JMLListValueNode) vorg_jmlspecs_models_JMLListValueNode$2$iter.get(); methodTests$.addTest (new TestCons(hd, tl)); vorg_jmlspecs_models_JMLListValueNode$2$iter.advance(); } vorg_jmlspecs_models_JMLType$1$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the cons method. */ protected static class TestCons extends OneTest { /** Argument hd */ private org.jmlspecs.models.JMLType hd; /** Argument tl */ private org.jmlspecs.models.JMLListValueNode tl; /** Initialize this instance. */ public TestCons(org.jmlspecs.models.JMLType hd, org.jmlspecs.models.JMLListValueNode tl) { super("cons"+ ":" + (hd==null? "null" :"{org.jmlspecs.models.JMLType}")+ "," +(tl==null? "null" :"{org.jmlspecs.models.JMLListValueNode}")); this.hd = hd; this.tl = tl; } protected void doCall() throws java.lang.Throwable { JMLListValueNode.cons(hd, tl); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'cons' applied to"; msg += "\n\tReceiver class JMLListValueNode"; msg += "\n\tArgument hd: " + this.hd; msg += "\n\tArgument tl: " + this.tl; return msg; } } /** Add tests for the head method * to the overall test suite. */ private void addTestSuiteFor$TestHead (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("head"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("head", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"head\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); methodTests$.addTest (new TestHead(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the head method. */ protected static class TestHead extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Initialize this instance. */ public TestHead(org.jmlspecs.models.JMLListValueNode receiver$) { super("head"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.head(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'head' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the headEquals method * to the overall test suite. */ private void addTestSuiteFor$TestHeadEquals (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("headEquals"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("headEquals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"headEquals\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("headEquals", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"headEquals\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestHeadEquals(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the headEquals method. */ protected static class TestHeadEquals extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestHeadEquals(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("headEquals"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.headEquals(item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'headEquals' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument item: " + this.item; return msg; } } /** Add tests for the itemAt method * to the overall test suite. */ private void addTestSuiteFor$TestItemAt (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("itemAt"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("itemAt", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"itemAt\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("itemAt", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"itemAt\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int i = vint$1$iter.getInt(); methodTests$.addTest (new TestItemAt(receiver$, i)); vint$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 itemAt method. */ protected static class TestItemAt extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument i */ private int i; /** Initialize this instance. */ public TestItemAt(org.jmlspecs.models.JMLListValueNode receiver$, int i) { super("itemAt"+ ":" + i); this.receiver$ = receiver$; this.i = i; } protected void doCall() throws java.lang.Throwable { receiver$.itemAt(i); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'itemAt' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument i: " + this.i; 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_JMLListValueNodeIter("int_size", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"int_size\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) 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.JMLListValueNode receiver$; /** Initialize this instance. */ public TestInt_size(org.jmlspecs.models.JMLListValueNode 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 int_length method * to the overall test suite. */ private void addTestSuiteFor$TestInt_length (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("int_length"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("int_length", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"int_length\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); methodTests$.addTest (new TestInt_length(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the int_length method. */ protected static class TestInt_length extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Initialize this instance. */ public TestInt_length(org.jmlspecs.models.JMLListValueNode receiver$) { super("int_length"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.int_length(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'int_length' applied to"; msg += "\n\tReceiver: " + this.receiver$; 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_JMLListValueNodeIter("has", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"has\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("has", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"has\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestHas(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the has method. */ protected static class TestHas extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestHas(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("has"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.has(item); } 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 item: " + this.item; return msg; } } /** Add tests for the isPrefixOf method * to the overall test suite. */ private void addTestSuiteFor$TestIsPrefixOf (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isPrefixOf"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("isPrefixOf", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"isPrefixOf\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLListValueNode$1$iter = this.vorg_jmlspecs_models_JMLListValueNodeIter("isPrefixOf", 0); this.check_has_data (vorg_jmlspecs_models_JMLListValueNode$1$iter, "this.vorg_jmlspecs_models_JMLListValueNodeIter(\"isPrefixOf\", 0)"); while (!vorg_jmlspecs_models_JMLListValueNode$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLListValueNode ls2 = (org.jmlspecs.models.JMLListValueNode) vorg_jmlspecs_models_JMLListValueNode$1$iter.get(); methodTests$.addTest (new TestIsPrefixOf(receiver$, ls2)); vorg_jmlspecs_models_JMLListValueNode$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 isPrefixOf method. */ protected static class TestIsPrefixOf extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument ls2 */ private org.jmlspecs.models.JMLListValueNode ls2; /** Initialize this instance. */ public TestIsPrefixOf(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLListValueNode ls2) { super("isPrefixOf"+ ":" + (ls2==null? "null" :"{org.jmlspecs.models.JMLListValueNode}")); this.receiver$ = receiver$; this.ls2 = ls2; } protected void doCall() throws java.lang.Throwable { receiver$.isPrefixOf(ls2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isPrefixOf' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument ls2: " + this.ls2; 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_JMLListValueNodeIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"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.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final java.lang.Object ls2 = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestEquals(receiver$, ls2)); 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.JMLListValueNode receiver$; /** Argument ls2 */ private java.lang.Object ls2; /** Initialize this instance. */ public TestEquals(org.jmlspecs.models.JMLListValueNode receiver$, java.lang.Object ls2) { super("equals"+ ":" + (ls2==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.ls2 = ls2; } protected void doCall() throws java.lang.Throwable { receiver$.equals(ls2); } 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 ls2: " + this.ls2; 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_JMLListValueNodeIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) 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.JMLListValueNode receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.models.JMLListValueNode 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 indexOf method * to the overall test suite. */ private void addTestSuiteFor$TestIndexOf (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("indexOf"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("indexOf", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"indexOf\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("indexOf", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"indexOf\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestIndexOf(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the indexOf method. */ protected static class TestIndexOf extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestIndexOf(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("indexOf"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.indexOf(item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'indexOf' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument item: " + this.item; return msg; } } /** Add tests for the last method * to the overall test suite. */ private void addTestSuiteFor$TestLast (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("last"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("last", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"last\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); methodTests$.addTest (new TestLast(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the last method. */ protected static class TestLast extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Initialize this instance. */ public TestLast(org.jmlspecs.models.JMLListValueNode receiver$) { super("last"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.last(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'last' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the getItem method * to the overall test suite. */ private void addTestSuiteFor$TestGetItem (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("getItem"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("getItem", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"getItem\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("getItem", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"getItem\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestGetItem(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the getItem method. */ protected static class TestGetItem extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestGetItem(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("getItem"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.getItem(item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'getItem' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument item: " + this.item; 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_JMLListValueNodeIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) 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.JMLListValueNode receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.models.JMLListValueNode 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 prefix method * to the overall test suite. */ private void addTestSuiteFor$TestPrefix (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("prefix"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("prefix", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"prefix\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("prefix", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"prefix\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int n = vint$1$iter.getInt(); methodTests$.addTest (new TestPrefix(receiver$, n)); vint$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 prefix method. */ protected static class TestPrefix extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument n */ private int n; /** Initialize this instance. */ public TestPrefix(org.jmlspecs.models.JMLListValueNode receiver$, int n) { super("prefix"+ ":" + n); this.receiver$ = receiver$; this.n = n; } protected void doCall() throws java.lang.Throwable { receiver$.prefix(n); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'prefix' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; return msg; } } /** Add tests for the removePrefix method * to the overall test suite. */ private void addTestSuiteFor$TestRemovePrefix (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removePrefix"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("removePrefix", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"removePrefix\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("removePrefix", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"removePrefix\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int n = vint$1$iter.getInt(); methodTests$.addTest (new TestRemovePrefix(receiver$, n)); vint$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 removePrefix method. */ protected static class TestRemovePrefix extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument n */ private int n; /** Initialize this instance. */ public TestRemovePrefix(org.jmlspecs.models.JMLListValueNode receiver$, int n) { super("removePrefix"+ ":" + n); this.receiver$ = receiver$; this.n = n; } protected void doCall() throws java.lang.Throwable { receiver$.removePrefix(n); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removePrefix' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; return msg; } } /** Add tests for the removeItemAt method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveItemAt (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeItemAt"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("removeItemAt", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"removeItemAt\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("removeItemAt", 0); this.check_has_data (vint$1$iter, "this.vintIter(\"removeItemAt\", 0)"); while (!vint$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int n = vint$1$iter.getInt(); methodTests$.addTest (new TestRemoveItemAt(receiver$, n)); vint$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 removeItemAt method. */ protected static class TestRemoveItemAt extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument n */ private int n; /** Initialize this instance. */ public TestRemoveItemAt(org.jmlspecs.models.JMLListValueNode receiver$, int n) { super("removeItemAt"+ ":" + n); this.receiver$ = receiver$; this.n = n; } protected void doCall() throws java.lang.Throwable { receiver$.removeItemAt(n); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeItemAt' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; return msg; } } /** Add tests for the replaceItemAt method * to the overall test suite. */ private void addTestSuiteFor$TestReplaceItemAt (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("replaceItemAt"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("replaceItemAt", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"replaceItemAt\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("replaceItemAt", 1); this.check_has_data (vint$1$iter, "this.vintIter(\"replaceItemAt\", 1)"); while (!vint$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("replaceItemAt", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"replaceItemAt\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int n = vint$1$iter.getInt(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestReplaceItemAt(receiver$, n, item)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vint$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 replaceItemAt method. */ protected static class TestReplaceItemAt extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument n */ private int n; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestReplaceItemAt(org.jmlspecs.models.JMLListValueNode receiver$, int n, org.jmlspecs.models.JMLType item) { super("replaceItemAt"+ ":" + n+ "," +(item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.n = n; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.replaceItemAt(n, item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'replaceItemAt' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; msg += "\n\tArgument item: " + this.item; return msg; } } /** Add tests for the removeLast method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveLast (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeLast"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("removeLast", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"removeLast\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); methodTests$.addTest (new TestRemoveLast(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeLast method. */ protected static class TestRemoveLast extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Initialize this instance. */ public TestRemoveLast(org.jmlspecs.models.JMLListValueNode receiver$) { super("removeLast"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.removeLast(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeLast' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the concat method * to the overall test suite. */ private void addTestSuiteFor$TestConcat (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("concat"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("concat", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"concat\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLListValueNode$1$iter = this.vorg_jmlspecs_models_JMLListValueNodeIter("concat", 0); this.check_has_data (vorg_jmlspecs_models_JMLListValueNode$1$iter, "this.vorg_jmlspecs_models_JMLListValueNodeIter(\"concat\", 0)"); while (!vorg_jmlspecs_models_JMLListValueNode$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLListValueNode ls2 = (org.jmlspecs.models.JMLListValueNode) vorg_jmlspecs_models_JMLListValueNode$1$iter.get(); methodTests$.addTest (new TestConcat(receiver$, ls2)); vorg_jmlspecs_models_JMLListValueNode$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 concat method. */ protected static class TestConcat extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument ls2 */ private org.jmlspecs.models.JMLListValueNode ls2; /** Initialize this instance. */ public TestConcat(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLListValueNode ls2) { super("concat"+ ":" + (ls2==null? "null" :"{org.jmlspecs.models.JMLListValueNode}")); this.receiver$ = receiver$; this.ls2 = ls2; } protected void doCall() throws java.lang.Throwable { receiver$.concat(ls2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'concat' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument ls2: " + this.ls2; return msg; } } /** Add tests for the prepend method * to the overall test suite. */ private void addTestSuiteFor$TestPrepend (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("prepend"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("prepend", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"prepend\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("prepend", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"prepend\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestPrepend(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the prepend method. */ protected static class TestPrepend extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestPrepend(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("prepend"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.prepend(item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'prepend' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument item: " + this.item; return msg; } } /** Add tests for the append method * to the overall test suite. */ private void addTestSuiteFor$TestAppend (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("append"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("append", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"append\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("append", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"append\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestAppend(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the append method. */ protected static class TestAppend extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestAppend(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("append"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.append(item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'append' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument item: " + this.item; return msg; } } /** Add tests for the reverse method * to the overall test suite. */ private void addTestSuiteFor$TestReverse (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("reverse"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("reverse", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"reverse\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); methodTests$.addTest (new TestReverse(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the reverse method. */ protected static class TestReverse extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Initialize this instance. */ public TestReverse(org.jmlspecs.models.JMLListValueNode receiver$) { super("reverse"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.reverse(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'reverse' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the insertBefore method * to the overall test suite. */ private void addTestSuiteFor$TestInsertBefore (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("insertBefore"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_models_JMLListValueNodeIter("insertBefore", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"insertBefore\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IntIterator vint$1$iter = this.vintIter("insertBefore", 1); this.check_has_data (vint$1$iter, "this.vintIter(\"insertBefore\", 1)"); while (!vint$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$2$iter = this.vorg_jmlspecs_models_JMLTypeIter("insertBefore", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$2$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"insertBefore\", 0)"); while (!vorg_jmlspecs_models_JMLType$2$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final int n = vint$1$iter.getInt(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$2$iter.get(); methodTests$.addTest (new TestInsertBefore(receiver$, n, item)); vorg_jmlspecs_models_JMLType$2$iter.advance(); } vint$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 insertBefore method. */ protected static class TestInsertBefore extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument n */ private int n; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestInsertBefore(org.jmlspecs.models.JMLListValueNode receiver$, int n, org.jmlspecs.models.JMLType item) { super("insertBefore"+ ":" + n+ "," +(item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.n = n; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.insertBefore(n, item); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'insertBefore' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument n: " + this.n; msg += "\n\tArgument item: " + this.item; 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_JMLListValueNodeIter("remove", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"remove\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_models_JMLType$1$iter = this.vorg_jmlspecs_models_JMLTypeIter("remove", 0); this.check_has_data (vorg_jmlspecs_models_JMLType$1$iter, "this.vorg_jmlspecs_models_JMLTypeIter(\"remove\", 0)"); while (!vorg_jmlspecs_models_JMLType$1$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) receivers$iter.get(); final org.jmlspecs.models.JMLType item = (org.jmlspecs.models.JMLType) vorg_jmlspecs_models_JMLType$1$iter.get(); methodTests$.addTest (new TestRemove(receiver$, item)); vorg_jmlspecs_models_JMLType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the remove method. */ protected static class TestRemove extends OneTest { /** The receiver */ private org.jmlspecs.models.JMLListValueNode receiver$; /** Argument item */ private org.jmlspecs.models.JMLType item; /** Initialize this instance. */ public TestRemove(org.jmlspecs.models.JMLListValueNode receiver$, org.jmlspecs.models.JMLType item) { super("remove"+ ":" + (item==null? "null" :"{org.jmlspecs.models.JMLType}")); this.receiver$ = receiver$; this.item = item; } protected void doCall() throws java.lang.Throwable { receiver$.remove(item); } 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 item: " + this.item; 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_JMLListValueNodeIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_models_JMLListValueNodeIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.models.JMLListValueNode receiver$ = (org.jmlspecs.models.JMLListValueNode) 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.JMLListValueNode receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.models.JMLListValueNode 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; } } /** 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); } }