// This file was generated by jmlunit on Mon Mar 16 13:16:47 EDT 2009. package org.jmlspecs.samples.list.list3; import org.jmlspecs.samples.list.node.OneWayNode; /** Automatically-generated test driver for JML and JUnit based * testing of E_OneWayList. 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 E_OneWayList.java
 *
* to regenerate this class whenever E_OneWayList.java changes. */ public class E_OneWayList_JML_Test extends E_OneWayList_JML_TestData { /** Initialize this class. */ public E_OneWayList_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 E_OneWayList * 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 E_OneWayList" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(E_OneWayList.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() { E_OneWayList_JML_Test testobj = new E_OneWayList_JML_Test("E_OneWayList_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(E_OneWayList_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 E_OneWayList_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 * E_OneWayList. 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$TestE_OneWayList(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestLength(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsEmpty(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestEquals(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestHashCode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveEntry(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInsertAfterCursor(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestInsertBeforeCursor(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$TestRemoveAllEntries(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$TestFirstEntry(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIncrementCursor(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsOffEnd(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsOffFront(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestGetEntry(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestReplaceEntry(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 E_OneWayList contructor * to the overall test suite. */ private void addTestSuiteFor$TestE_OneWayList (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("E_OneWayList"); try { methodTests$.addTest (new TestE_OneWayList()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the E_OneWayList contructor. */ protected static class TestE_OneWayList extends OneTest { /** Initialize this instance. */ public TestE_OneWayList() { super("E_OneWayList"); } protected void doCall() throws java.lang.Throwable { new E_OneWayList(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'E_OneWayList'"; return msg; } } /** Add tests for the length method * to the overall test suite. */ private void addTestSuiteFor$TestLength (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("length"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("length", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"length\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestLength(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the length method. */ protected static class TestLength extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestLength(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("length"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.length(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'length' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the isEmpty method * to the overall test suite. */ private void addTestSuiteFor$TestIsEmpty (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isEmpty"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("isEmpty", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"isEmpty\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestIsEmpty(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isEmpty method. */ protected static class TestIsEmpty extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestIsEmpty(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("isEmpty"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isEmpty(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isEmpty' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the equals method * to the overall test suite. */ private void addTestSuiteFor$TestEquals (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("equals"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("equals", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"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.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) 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.samples.list.list3.E_OneWayList receiver$; /** Argument obj */ private java.lang.Object obj; /** Initialize this instance. */ public TestEquals(org.jmlspecs.samples.list.list3.E_OneWayList receiver$, java.lang.Object obj) { super("equals"+ ":" + (obj==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.obj = obj; } protected void doCall() throws java.lang.Throwable { receiver$.equals(obj); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'equals' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument obj: " + this.obj; return msg; } } /** Add tests for the hashCode method * to the overall test suite. */ private void addTestSuiteFor$TestHashCode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("hashCode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("hashCode", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"hashCode\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) 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.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestHashCode(org.jmlspecs.samples.list.list3.E_OneWayList 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 removeEntry method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveEntry (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeEntry"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("removeEntry", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"removeEntry\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestRemoveEntry(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeEntry method. */ protected static class TestRemoveEntry extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestRemoveEntry(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("removeEntry"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.removeEntry(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeEntry' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the insertAfterCursor method * to the overall test suite. */ private void addTestSuiteFor$TestInsertAfterCursor (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("insertAfterCursor"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("insertAfterCursor", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"insertAfterCursor\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("insertAfterCursor", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"insertAfterCursor\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); final java.lang.Object newEntry = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestInsertAfterCursor(receiver$, newEntry)); 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 insertAfterCursor method. */ protected static class TestInsertAfterCursor extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Argument newEntry */ private java.lang.Object newEntry; /** Initialize this instance. */ public TestInsertAfterCursor(org.jmlspecs.samples.list.list3.E_OneWayList receiver$, java.lang.Object newEntry) { super("insertAfterCursor"+ ":" + (newEntry==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.newEntry = newEntry; } protected void doCall() throws java.lang.Throwable { receiver$.insertAfterCursor(newEntry); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'insertAfterCursor' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument newEntry: " + this.newEntry; return msg; } } /** Add tests for the insertBeforeCursor method * to the overall test suite. */ private void addTestSuiteFor$TestInsertBeforeCursor (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("insertBeforeCursor"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("insertBeforeCursor", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"insertBeforeCursor\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("insertBeforeCursor", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"insertBeforeCursor\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); final java.lang.Object newEntry = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestInsertBeforeCursor(receiver$, newEntry)); 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 insertBeforeCursor method. */ protected static class TestInsertBeforeCursor extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Argument newEntry */ private java.lang.Object newEntry; /** Initialize this instance. */ public TestInsertBeforeCursor(org.jmlspecs.samples.list.list3.E_OneWayList receiver$, java.lang.Object newEntry) { super("insertBeforeCursor"+ ":" + (newEntry==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.newEntry = newEntry; } protected void doCall() throws java.lang.Throwable { receiver$.insertBeforeCursor(newEntry); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'insertBeforeCursor' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument newEntry: " + this.newEntry; 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_samples_list_list3_E_OneWayListIter("append", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"append\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("append", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"append\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); final java.lang.Object newEntry = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestAppend(receiver$, newEntry)); 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 append method. */ protected static class TestAppend extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Argument newEntry */ private java.lang.Object newEntry; /** Initialize this instance. */ public TestAppend(org.jmlspecs.samples.list.list3.E_OneWayList receiver$, java.lang.Object newEntry) { super("append"+ ":" + (newEntry==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.newEntry = newEntry; } protected void doCall() throws java.lang.Throwable { receiver$.append(newEntry); } 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 newEntry: " + this.newEntry; return msg; } } /** Add tests for the removeAllEntries method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveAllEntries (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeAllEntries"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("removeAllEntries", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"removeAllEntries\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestRemoveAllEntries(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeAllEntries method. */ protected static class TestRemoveAllEntries extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestRemoveAllEntries(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("removeAllEntries"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.removeAllEntries(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeAllEntries' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the clone method * to the overall test suite. */ private void addTestSuiteFor$TestClone (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("clone"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("clone", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"clone\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) 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.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestClone(org.jmlspecs.samples.list.list3.E_OneWayList 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 firstEntry method * to the overall test suite. */ private void addTestSuiteFor$TestFirstEntry (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("firstEntry"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("firstEntry", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"firstEntry\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestFirstEntry(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the firstEntry method. */ protected static class TestFirstEntry extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestFirstEntry(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("firstEntry"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.firstEntry(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'firstEntry' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the incrementCursor method * to the overall test suite. */ private void addTestSuiteFor$TestIncrementCursor (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("incrementCursor"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("incrementCursor", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"incrementCursor\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestIncrementCursor(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the incrementCursor method. */ protected static class TestIncrementCursor extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestIncrementCursor(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("incrementCursor"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.incrementCursor(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'incrementCursor' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the isOffEnd method * to the overall test suite. */ private void addTestSuiteFor$TestIsOffEnd (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isOffEnd"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("isOffEnd", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"isOffEnd\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestIsOffEnd(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isOffEnd method. */ protected static class TestIsOffEnd extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestIsOffEnd(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("isOffEnd"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isOffEnd(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isOffEnd' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the isOffFront method * to the overall test suite. */ private void addTestSuiteFor$TestIsOffFront (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isOffFront"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("isOffFront", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"isOffFront\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestIsOffFront(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isOffFront method. */ protected static class TestIsOffFront extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestIsOffFront(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("isOffFront"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.isOffFront(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isOffFront' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the getEntry method * to the overall test suite. */ private void addTestSuiteFor$TestGetEntry (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("getEntry"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("getEntry", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"getEntry\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); methodTests$.addTest (new TestGetEntry(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the getEntry method. */ protected static class TestGetEntry extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestGetEntry(org.jmlspecs.samples.list.list3.E_OneWayList receiver$) { super("getEntry"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.getEntry(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'getEntry' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the replaceEntry method * to the overall test suite. */ private void addTestSuiteFor$TestReplaceEntry (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("replaceEntry"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("replaceEntry", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"replaceEntry\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vjava_lang_Object$1$iter = this.vjava_lang_ObjectIter("replaceEntry", 0); this.check_has_data (vjava_lang_Object$1$iter, "this.vjava_lang_ObjectIter(\"replaceEntry\", 0)"); while (!vjava_lang_Object$1$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) receivers$iter.get(); final java.lang.Object arg1 = (java.lang.Object) vjava_lang_Object$1$iter.get(); methodTests$.addTest (new TestReplaceEntry(receiver$, arg1)); vjava_lang_Object$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the replaceEntry method. */ protected static class TestReplaceEntry extends OneTest { /** The receiver */ private org.jmlspecs.samples.list.list3.E_OneWayList receiver$; /** Argument arg1 */ private java.lang.Object arg1; /** Initialize this instance. */ public TestReplaceEntry(org.jmlspecs.samples.list.list3.E_OneWayList receiver$, java.lang.Object arg1) { super("replaceEntry"+ ":" + (arg1==null? "null" :"{java.lang.Object}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.replaceEntry(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'replaceEntry' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the toString method * to the overall test suite. */ private void addTestSuiteFor$TestToString (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toString"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_list_list3_E_OneWayListIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.list.list3.E_OneWayList receiver$ = (org.jmlspecs.samples.list.list3.E_OneWayList) 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.samples.list.list3.E_OneWayList receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.samples.list.list3.E_OneWayList 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); } }