Uses of Class org.jmlspecs.jmlrac.runtime.JMLAssertionError (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV NEXT

FRAMES NO FRAMES

Uses of Class
org.jmlspecs.jmlrac.runtime.JMLAssertionError

Packages that use JMLAssertionError
org.jmlspecs.jmlrac.runtime	Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc).
org.jmlspecs.jmlunit.strategies	The types in this package are used in providing test data for JML/JUnit testing.
org.jmlspecs.lang	This package is a collection of types used in the definition of the JML language.
org.jmlspecs.models	This package is a collection of types with immutable objects; it also enumerators (which have mutable objects) for the types of the immutable collections in the package.
org.jmlspecs.models.resolve	This package is a collection of types with immutable objects based on the RESOLVE specification language's mathematical models.
org.jmlspecs.samples.dbc	This package contains samples of JML specifications written in the style of design by contract.
org.jmlspecs.samples.digraph	This package contains samples of JML specifications for directed graphs.
org.jmlspecs.samples.jmlkluwer	This package contains samples of JML specifications from the paper "JML: a Notation for Detailed Design".
org.jmlspecs.samples.jmlrefman	This package contains samples of JML specifications from the JML Reference Manual.
org.jmlspecs.samples.jmltutorial	This package contains samples of JML specifications from the tutorials.
org.jmlspecs.samples.list.list1
org.jmlspecs.samples.list.list1.node
org.jmlspecs.samples.list.list2
org.jmlspecs.samples.list.list3
org.jmlspecs.samples.list.node
org.jmlspecs.samples.list.node2
org.jmlspecs.samples.misc	This package contains miscellaneous samples of JML specifications.
org.jmlspecs.samples.prelimdesign	This package contains samples of JML specifications from the paper Preliminary Design of JML.
org.jmlspecs.samples.reader	This package contains samples of JML specifications relating to some abstractions of input and output.
org.jmlspecs.samples.sets	This package contains samples of JML specifications relating to sets.
org.jmlspecs.samples.stacks	This package contains samples of JML specifications relating to stacks of various sorts.
org.jmlspecs.samples.table	This package contains samples of JML specifications relating to tables.
org.jmlspecs.util

Uses of JMLAssertionError in org.jmlspecs.jmlrac.runtime

Subclasses of JMLAssertionError in org.jmlspecs.jmlrac.runtime
`class`	`JMLAssertError` A JML error class to report violations of JML `assert` specification statements.
`class`	`JMLAssumeError` A JML error class to report violations of JML `assume` specification statements.
`class`	`JMLDebugError` A JML error class to report an error in the JML `debug` statement.
`class`	`JMLEntryPreconditionError` A JML error class to notify entry precondition violations.
`class`	`JMLEvaluationError`
`class`	`JMLExceptionalPostconditionError` A JML error class to notify exceptional postcondition violations.
`class`	`JMLExitExceptionalPostconditionError` A JML error class to notify exit exceptional postcondition violations.
`class`	`JMLExitNormalPostconditionError` A JML error class to notify exit normal postcondition violations.
`class`	`JMLHenceByError` A JML error class to report violations of `hence_by` specification statements.
`class`	`JMLHistoryConstraintError` A JML error class to notify history constraint violations.
`class`	`JMLInternalExceptionalPostconditionError` A JML error class to notify internal exceptional postcondition violations.
`class`	`JMLInternalNormalPostconditionError` A JML error class to notify internal normal postcondition violations.
`class`	`JMLInternalPreconditionError` A JML error class to notify internal precondition violations.
`class`	`JMLIntraconditionError` A JML exception class to signal intracondition violations.
`class`	`JMLInvariantError` A JML error class to notify invariant violations.
`class`	`JMLLoopInvariantError` A JML error class to report loop invariant violations.
`class`	`JMLLoopVariantError` A JML error class to report loop variant violations.
`class`	`JMLNormalPostconditionError` A JML error class to notify normal postcondition violations.
`class`	`JMLPostconditionError` A JML error class to notify postcondition violations.
`class`	`JMLPreconditionError` A JML exception class for notifying precondition violations.
`class`	`JMLUnreachableError` A JML error class to report violations of `unreachable` specification statements.

Methods in org.jmlspecs.jmlrac.runtime with parameters of type JMLAssertionError
`static boolean`	`JMLRacUtil.matchCause(Class c, JMLAssertionError e)`
`static boolean`	`JMLRacUtil.checkErr(Class c, JMLAssertionError e)` Under the old semantics, ensure that e is an instance of c.

Constructors in org.jmlspecs.jmlrac.runtime with parameters of type JMLAssertionError
`JMLEvaluationError(String message, JMLAssertionError cause)`
`JMLInternalExceptionalPostconditionError(JMLAssertionError e)` Creates a new instance from the given assertion error.
`JMLInternalNormalPostconditionError(JMLAssertionError e)` Creates a new instance from the given assertion error.
`JMLInternalPreconditionError(JMLAssertionError e)` Creates a new instance from the given assertion error.

Uses of JMLAssertionError in org.jmlspecs.jmlunit.strategies

Methods in org.jmlspecs.jmlunit.strategies with parameters of type JMLAssertionError
`protected abstract String`	`CharIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`CharIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`CharIterator_JML_Test.TestGetChar.failMessage(JMLAssertionError e$)`
`protected String`	`CharIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`CharIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`CharIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected abstract String`	`CloneableObjectArrayAbstractIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`CloneableObjectArrayAbstractIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`CloneableObjectArrayAbstractIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`CloneableObjectArrayAbstractIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`CloneableObjectArrayAbstractIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`CloneableObjectArrayAbstractIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`CompositeIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`CompositeIterator_JML_Test.TestCompositeIterator.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestCompositeIterator$1.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestCompositeIterator$2.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`CompositeIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestInitialize.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestApprove.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestGetDouble.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleAbstractFilteringIteratorDecorator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected abstract String`	`DoubleCompositeIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`DoubleCompositeIterator_JML_Test.TestDoubleCompositeIterator.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestDoubleCompositeIterator$1.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestDoubleCompositeIterator$2.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestGetDouble.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`DoubleCompositeIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected abstract String`	`ImmutableObjectArrayIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestImmutableObjectArrayIterator.failMessage(JMLAssertionError e$)`
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`ImmutableObjectArrayIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`IntArrayIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntArrayIterator_JML_Test.TestIntArrayIterator.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestGetInt.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`IntArrayIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected abstract String`	`NewObjectAbstractIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`NewObjectAbstractIterator_JML_Test.TestInitialize.failMessage(JMLAssertionError e$)`
`protected String`	`NewObjectAbstractIterator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`NewObjectAbstractIterator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`NewObjectAbstractIterator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`NewObjectAbstractIterator_JML_Test.TestMake.failMessage(JMLAssertionError e$)`
`protected String`	`NewObjectAbstractIterator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected abstract String`	`NonNullIteratorDecorator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`NonNullIteratorDecorator_JML_Test.TestNonNullIteratorDecorator.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestApprove.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestInitialize.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestAtEnd.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestAdvance.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`NonNullIteratorDecorator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.lang

Methods in org.jmlspecs.lang with parameters of type JMLAssertionError
`protected abstract String`	`JMLDataGroup_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLDataGroup_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLDataGroup_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLDataGroup_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLDataGroup_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.models

Methods in org.jmlspecs.models with parameters of type JMLAssertionError
`protected abstract String`	`JMLChar_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLChar_JML_Test.TestJMLChar.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestJMLChar$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestJMLChar$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestCharValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestGetChar.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestIntValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestPlus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestMinus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestTimes.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestDividedBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestRemainderBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestGreaterThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestLessThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestGreaterThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLChar_JML_Test.TestLessThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLFloat_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLFloat_JML_Test.TestJMLFloat.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestJMLFloat$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestJMLFloat$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestJMLFloat$3.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestJMLFloat$4.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestIsInfinite.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestIsNaN.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestIsZero.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestIsZero$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestFloatValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestGetFloat.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestNegated.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestPlus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestMinus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestTimes.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestDividedBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestRemainderBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestGreaterThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestLessThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestGreaterThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestLessThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$3.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$3.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$4.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$4.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$5.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$5.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestWithinEpsilonOf$6.failMessage(JMLAssertionError e$)`
`protected String`	`JMLFloat_JML_Test.TestApproximatelyEqualTo$6.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLInfiniteInteger_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLInfiniteInteger_JML_Test.TestSignum.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestIsFinite.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestFiniteValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestGreaterThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestLessThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestGreaterThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestLessThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestAbs.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestMax.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestMin.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestNegate.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestSubtract.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestMultiply.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestDivide.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestRemainder.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestMod.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestPow.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestDoubleValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestFloatValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestToString$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInfiniteInteger_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLInteger_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLInteger_JML_Test.TestJMLInteger.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestJMLInteger$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestJMLInteger$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestJMLInteger$3.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestIntValue.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestGetInteger.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestNegated.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestPlus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestMinus.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestTimes.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestDividedBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestRemainderBy.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestGreaterThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestLessThan.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestGreaterThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestLessThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLInteger_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLListValueNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLListValueNode_JML_Test.TestJMLListValueNode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestCons.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestHead.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestHeadEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestItemAt.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestInt_size.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestInt_length.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestHas.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestIsPrefixOf.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestIndexOf.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestLast.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestGetItem.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestPrefix.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestRemovePrefix.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestRemoveItemAt.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestReplaceItemAt.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestRemoveLast.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestConcat.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestPrepend.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestReverse.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestInsertBefore.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`JMLListValueNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLNullSafe_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLNullSafe_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLNullSafe_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLNullSafe_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLObjectToObjectRelation_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestJMLObjectToObjectRelation$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestSingleton.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestSingleton$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestIsaFunction.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestElementImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestInverse.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestInverseElementImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestInverseImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestIsDefinedAt.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestHas.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestHas$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestHas$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestDomain.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRange.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestInsert.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRemoveFromDomain.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRemove$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestCompose.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestCompose$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestIntersection.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestDifference.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRestrictDomainTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRestrictRangeTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestAssociations.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestIterator.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestToSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestToBag.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestToSequence.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestImagePairSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestImagePairs.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestDomainElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestRangeElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestInt_size.failMessage(JMLAssertionError e$)`
`protected String`	`JMLObjectToObjectRelation_JML_Test.TestToFunction.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLString_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLString_JML_Test.TestJMLString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestJMLString$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestCompareTo$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestEqualsIgnoreCase.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestEqualsIgnoreCase$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestConcat.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestConcat$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLString_JML_Test.TestConcat$2.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLValueObjectPair_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLValueObjectPair_JML_Test.TestJMLValueObjectPair.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestKeyEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestValueEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueObjectPair_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLValueSet_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLValueSet_JML_Test.TestJMLValueSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestJMLValueSet$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestSingleton.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestConvertFrom.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestConvertFrom$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestConvertFrom$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestHas.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestContainsAll.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestInt_size.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIsSubset.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIsProperSubset.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIsSuperset.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIsProperSuperset.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestChoose.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestInsert.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIntersection.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestDifference.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestPowerSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestToBag.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestToSequence.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestToArray.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestIterator.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueSet_JML_Test.TestHas$1.failMessage(JMLAssertionError e$)`
`protected abstract String`	`JMLValueToValueMap_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`JMLValueToValueMap_JML_Test.TestJMLValueToValueMap.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestJMLValueToValueMap$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestJMLValueToValueMap$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestSingletonMap.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestSingletonMap$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestIsaFunction.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestApply.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestExtend.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRemoveDomainElement.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestCompose.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestCompose$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRestrictedTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRangeRestrictedTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestExtendUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestClashReplaceUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestDisjointUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestElementImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestInverse.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestInverseElementImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestInverseImage.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestIsDefinedAt.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestHas.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestHas$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestHas$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestDomain.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRange.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestInsert.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRemoveFromDomain.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRemove$1.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestCompose$2.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestCompose$3.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestUnion.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestIntersection.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestDifference.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRestrictDomainTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRestrictRangeTo.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestAssociations.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestIterator.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestToSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestToBag.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestToSequence.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestImagePairSet.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestImagePairs.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestDomainElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestRangeElements.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestInt_size.failMessage(JMLAssertionError e$)`
`protected String`	`JMLValueToValueMap_JML_Test.TestToFunction.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.models.resolve

Methods in org.jmlspecs.models.resolve with parameters of type JMLAssertionError
`protected abstract String`	`NaturalNumber_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`NaturalNumber_JML_Test.TestNaturalNumber.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestNaturalNumber$1.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestNaturalNumber$2.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestValueOf.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestSuc.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestSuc$1.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestMultiply.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestDivide.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestRemainder.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestPow.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestPow$1.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestGcd.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestMod.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestShiftLeft.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestShiftRight.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestCompareTo.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestCompareTo$1.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestIsZero.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestDivides.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestMin.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestMax.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestBigIntegerValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestIntValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestLongValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestFloatValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestDoubleValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestByteValue.failMessage(JMLAssertionError e$)`
`protected String`	`NaturalNumber_JML_Test.TestShortValue.failMessage(JMLAssertionError e$)`
`protected abstract String`	`StringOfObject_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`StringOfObject_JML_Test.TestStringOfObject.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestStringOfObject$1.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestSingleton.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestExt.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestFrom.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestFrom$1.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestProduct.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestProductFrom.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestProductFromTo.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestGet.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestInt_size.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestExt$1.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAddFront.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAddAfterIndex.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAddBeforeIndex.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestConcat.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestComposedWith.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAddAll.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestAddAll$1.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestRev.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestReverse.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestPow.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestOccurs_ct.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestHas.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIterator.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestElements.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIsPrefix.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIsProperPrefix.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIsProperSuffix.failMessage(JMLAssertionError e$)`
`protected String`	`StringOfObject_JML_Test.TestIsSuffix.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.dbc

Methods in org.jmlspecs.samples.dbc with parameters of type JMLAssertionError
`protected abstract String`	`Complex_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Complex_JML_Test.TestRealPart.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestImaginaryPart.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestMagnitude.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestAngle.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestAdd.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestSub.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestMul.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestDiv.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`Complex_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.digraph

Methods in org.jmlspecs.samples.digraph with parameters of type JMLAssertionError
`protected abstract String`	`Arc_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Arc_JML_Test.TestArc.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestFlip.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestGetSource.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestSetSource.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestGetTarget.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestSetTarget.failMessage(JMLAssertionError e$)`
`protected String`	`Arc_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`NodeType_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`NodeType_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`NodeType_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`NodeType_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SearchableDigraph_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SearchableDigraph_JML_Test.TestSearchableDigraph.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestDFS.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestDFSVisit.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestTranspose.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestAddNode.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestRemoveNode.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestAddArc.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestRemoveArc.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestIsNode.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestIsArc.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestIsAPath.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableDigraph_JML_Test.TestUnconnected.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SearchableNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SearchableNode_JML_Test.TestSearchableNode.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestGetColor.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestGetPredecessor.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestGetFinishTime.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestGetDiscoverTime.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestSetValue.failMessage(JMLAssertionError e$)`
`protected String`	`SearchableNode_JML_Test.TestGetValue.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TransposableDigraph_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TransposableDigraph_JML_Test.TestTransposableDigraph.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestTranspose.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestAddNode.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestRemoveNode.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestAddArc.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestRemoveArc.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestIsNode.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestIsArc.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestIsAPath.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableDigraph_JML_Test.TestUnconnected.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TransposableNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TransposableNode_JML_Test.TestTransposableNode.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestSetValue.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestGetValue.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`TransposableNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.jmlkluwer

Methods in org.jmlspecs.samples.jmlkluwer with parameters of type JMLAssertionError
`protected abstract String`	`PriorityQueue_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`PriorityQueue_JML_Test.TestPriorityQueue.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestAddEntry.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestContains.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestNext.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`PriorityQueue_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`QueueEntry_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`QueueEntry_JML_Test.TestQueueEntry.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestGetLevel.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestGetObj.failMessage(JMLAssertionError e$)`
`protected String`	`QueueEntry_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.jmlrefman

Methods in org.jmlspecs.samples.jmlrefman with parameters of type JMLAssertionError
`protected abstract String`	`RefineDemo2_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected abstract String`	`RefineDemo_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`RefineDemo_JML_Test.TestRefineDemo.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SumArrayLoop_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SumArrayLoop_JML_Test.TestSumArray.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.jmltutorial

Methods in org.jmlspecs.samples.jmltutorial with parameters of type JMLAssertionError
`protected abstract String`	`Person_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Person_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`Person_JML_Test.TestGetWeight.failMessage(JMLAssertionError e$)`
`protected String`	`Person_JML_Test.TestAddKgs.failMessage(JMLAssertionError e$)`
`protected String`	`Person_JML_Test.TestPerson.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SqrtExample_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SqrtExample_JML_Test.TestSqrt.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.list1

Methods in org.jmlspecs.samples.list.list1 with parameters of type JMLAssertionError
`protected abstract String`	`DLList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`DLList_JML_Test.TestDLList.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestDecrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestLastEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestCreateIterator.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`DLList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected abstract String`	`E_SLList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`E_SLList_JML_Test.TestE_SLList.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestCreateIterator.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_SLList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`ListIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`ListIterator_JML_Test.TestListIterator.failMessage(JMLAssertionError e$)`
`protected String`	`ListIterator_JML_Test.TestFirst.failMessage(JMLAssertionError e$)`
`protected String`	`ListIterator_JML_Test.TestNext.failMessage(JMLAssertionError e$)`
`protected String`	`ListIterator_JML_Test.TestIsDone.failMessage(JMLAssertionError e$)`
`protected String`	`ListIterator_JML_Test.TestCurrentItem.failMessage(JMLAssertionError e$)`
`protected String`	`ListIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SLList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SLList_JML_Test.TestSLList.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`SLList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.list1.node

Methods in org.jmlspecs.samples.list.list1.node with parameters of type JMLAssertionError
`protected abstract String`	`DLNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`DLNode_JML_Test.TestDLNode.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestGetPrevNode.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestInsertBefore.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`DLNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`SLNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`SLNode_JML_Test.TestSLNode.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`SLNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.list2

Methods in org.jmlspecs.samples.list.list2 with parameters of type JMLAssertionError
`protected abstract String`	`E_OneWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`E_OneWayList_JML_Test.TestE_OneWayList.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`OneWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`OneWayList_JML_Test.TestOneWayList.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayIterator_JML_Test.TestTwoWayIterator.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestFirst.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestNext.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestIsDone.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestCurrentItem.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestLast.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestPrevious.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestIsAtFront.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayList_JML_Test.TestTwoWayList.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestDecrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestLastEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestCreateIterator.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.list3

Methods in org.jmlspecs.samples.list.list3 with parameters of type JMLAssertionError
`protected abstract String`	`E_OneWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`E_OneWayList_JML_Test.TestE_OneWayList.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`E_OneWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`OneWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`OneWayList_JML_Test.TestOneWayList.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayIterator_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayIterator_JML_Test.TestTwoWayIterator.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestFirst.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestNext.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestIsDone.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestCurrentItem.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestLast.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestPrevious.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestIsAtFront.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayIterator_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayList_JML_Test.TestTwoWayList.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestDecrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestLastEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestInsertAfterCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestInsertBeforeCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestCreateIterator.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestLength.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestAppend.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestRemoveAllEntries.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestFirstEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIncrementCursor.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsOffEnd.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestIsOffFront.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestReplaceEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.node

Methods in org.jmlspecs.samples.list.node with parameters of type JMLAssertionError
`protected abstract String`	`OneWayNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`OneWayNode_JML_Test.TestOneWayNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestOneWayNode$1.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestHasNext.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayNode_JML_Test.TestTwoWayNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestTwoWayNode$1.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetPrevNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestInsertBefore.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestHasNext.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.list.node2

Methods in org.jmlspecs.samples.list.node2 with parameters of type JMLAssertionError
`protected abstract String`	`OneWayNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`OneWayNode_JML_Test.TestOneWayNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestOneWayNode$1.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestGetNextLink.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestHasNext.failMessage(JMLAssertionError e$)`
`protected String`	`OneWayNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TwoWayNode_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TwoWayNode_JML_Test.TestTwoWayNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestInsertAfter.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestRemoveNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetPrevNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetPrevLink.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestInsertBefore.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestRemovePrevNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestSetEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetNextNode.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestGetNextLink.failMessage(JMLAssertionError e$)`
`protected String`	`TwoWayNode_JML_Test.TestHasNext.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.misc

Methods in org.jmlspecs.samples.misc with parameters of type JMLAssertionError
`protected abstract String`	`Counter_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Counter_JML_Test.TestInc.failMessage(JMLAssertionError e$)`
`protected String`	`Counter_JML_Test.TestValue.failMessage(JMLAssertionError e$)`
`protected abstract String`	`LinearSearch_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`LinearSearch_JML_Test.TestF.failMessage(JMLAssertionError e$)`
`protected String`	`LinearSearch_JML_Test.TestLimit.failMessage(JMLAssertionError e$)`
`protected String`	`LinearSearch_JML_Test.TestFind.failMessage(JMLAssertionError e$)`
`protected abstract String`	`Meter_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Meter_JML_Test.TestInc.failMessage(JMLAssertionError e$)`
`protected String`	`Meter_JML_Test.TestValue.failMessage(JMLAssertionError e$)`
`protected String`	`Meter_JML_Test.TestMeter.failMessage(JMLAssertionError e$)`
`protected abstract String`	`Proof_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Proof_JML_Test.TestFind_min.failMessage(JMLAssertionError e$)`
`protected String`	`Proof_JML_Test.TestGetRes.failMessage(JMLAssertionError e$)`
`protected String`	`Proof_JML_Test.TestFind.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.prelimdesign

Methods in org.jmlspecs.samples.prelimdesign with parameters of type JMLAssertionError
`protected abstract String`	`Account_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Account_JML_Test.TestAccount.failMessage(JMLAssertionError e$)`
`protected String`	`Account_JML_Test.TestBalance.failMessage(JMLAssertionError e$)`
`protected String`	`Account_JML_Test.TestPayInterest.failMessage(JMLAssertionError e$)`
`protected String`	`Account_JML_Test.TestDeposit.failMessage(JMLAssertionError e$)`
`protected String`	`Account_JML_Test.TestWithdraw.failMessage(JMLAssertionError e$)`
`protected String`	`Account_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`IntMathOps2_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntMathOps2_JML_Test.TestIsqrt.failMessage(JMLAssertionError e$)`
`protected abstract String`	`IntMathOps4_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntMathOps4_JML_Test.TestIsqrt.failMessage(JMLAssertionError e$)`
`protected abstract String`	`IntMathOps_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntMathOps_JML_Test.TestIsqrt.failMessage(JMLAssertionError e$)`
`protected abstract String`	`PlusAccount_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`PlusAccount_JML_Test.TestPlusAccount.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestPayInterest.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestWithdraw.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestDeposit.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestDepositToChecking.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestPayCheck.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`PlusAccount_JML_Test.TestBalance.failMessage(JMLAssertionError e$)`
`protected abstract String`	`Point2D_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`Point2D_JML_Test.TestPoint2D.failMessage(JMLAssertionError e$)`
`protected String`	`Point2D_JML_Test.TestPoint2D$1.failMessage(JMLAssertionError e$)`
`protected String`	`Point2D_JML_Test.TestGetX.failMessage(JMLAssertionError e$)`
`protected String`	`Point2D_JML_Test.TestGetY.failMessage(JMLAssertionError e$)`
`protected String`	`Point2D_JML_Test.TestMoveX.failMessage(JMLAssertionError e$)`
`protected String`	`Point2D_JML_Test.TestMoveY.failMessage(JMLAssertionError e$)`
`protected abstract String`	`USMoney_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`USMoney_JML_Test.TestUSMoney.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestUSMoney$1.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestPlus.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestMinus.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestScaleBy.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestGreaterThan.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestGreaterThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestLessThan.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestLessThanOrEqualTo.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestDollars.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestCents.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`USMoney_JML_Test.TestClone.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.reader

Methods in org.jmlspecs.samples.reader with parameters of type JMLAssertionError
`protected abstract String`	`BlankReader_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`BlankReader_JML_Test.TestBlankReader.failMessage(JMLAssertionError e$)`
`protected String`	`BlankReader_JML_Test.TestRefill.failMessage(JMLAssertionError e$)`
`protected String`	`BlankReader_JML_Test.TestClose.failMessage(JMLAssertionError e$)`
`protected String`	`BlankReader_JML_Test.TestRead.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.sets

Methods in org.jmlspecs.samples.sets with parameters of type JMLAssertionError
`protected abstract String`	`IntegerSetAsHashSet_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntegerSetAsHashSet_JML_Test.TestIntegerSetAsHashSet.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsHashSet_JML_Test.TestIsMember.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsHashSet_JML_Test.TestInsert.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsHashSet_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsHashSet_JML_Test.TestToString.failMessage(JMLAssertionError e$)`
`protected abstract String`	`IntegerSetAsTree_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`IntegerSetAsTree_JML_Test.TestIntegerSetAsTree.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsTree_JML_Test.TestInsert.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsTree_JML_Test.TestIsMember.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsTree_JML_Test.TestRemove.failMessage(JMLAssertionError e$)`
`protected String`	`IntegerSetAsTree_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.stacks

Methods in org.jmlspecs.samples.stacks with parameters of type JMLAssertionError
`protected abstract String`	`BoundedStackInterface_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`BoundedStackInterface_JML_Test.TestPop.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestPush.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestTop.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestGetSizeLimit.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestIsEmpty.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestIsFull.failMessage(JMLAssertionError e$)`
`protected String`	`BoundedStackInterface_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected abstract String`	`UnboundedStackAsArrayList_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`UnboundedStackAsArrayList_JML_Test.TestUnboundedStackAsArrayList.failMessage(JMLAssertionError e$)`
`protected String`	`UnboundedStackAsArrayList_JML_Test.TestPop.failMessage(JMLAssertionError e$)`
`protected String`	`UnboundedStackAsArrayList_JML_Test.TestPush.failMessage(JMLAssertionError e$)`
`protected String`	`UnboundedStackAsArrayList_JML_Test.TestTop.failMessage(JMLAssertionError e$)`
`protected String`	`UnboundedStackAsArrayList_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.samples.table

Methods in org.jmlspecs.samples.table with parameters of type JMLAssertionError
`protected abstract String`	`EntryImplementation_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`EntryImplementation_JML_Test.TestEntryImplementation.failMessage(JMLAssertionError e$)`
`protected String`	`EntryImplementation_JML_Test.TestGetIndex.failMessage(JMLAssertionError e$)`
`protected String`	`EntryImplementation_JML_Test.TestGetValue.failMessage(JMLAssertionError e$)`
`protected String`	`EntryImplementation_JML_Test.TestEquals.failMessage(JMLAssertionError e$)`
`protected String`	`EntryImplementation_JML_Test.TestHashCode.failMessage(JMLAssertionError e$)`
`protected String`	`EntryImplementation_JML_Test.TestClone.failMessage(JMLAssertionError e$)`
`protected abstract String`	`TableImplementation_JML_Test.OneTest.failMessage(JMLAssertionError e)` Format the error message for a test failure, based on the method's arguments.
`protected String`	`TableImplementation_JML_Test.TestTableImplementation.failMessage(JMLAssertionError e$)`
`protected String`	`TableImplementation_JML_Test.TestIsUsedIndex.failMessage(JMLAssertionError e$)`
`protected String`	`TableImplementation_JML_Test.TestAddEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TableImplementation_JML_Test.TestRemoveEntry.failMessage(JMLAssertionError e$)`
`protected String`	`TableImplementation_JML_Test.TestMapTo.failMessage(JMLAssertionError e$)`
`protected String`	`TableImplementation_JML_Test.TestToString.failMessage(JMLAssertionError e$)`

Uses of JMLAssertionError in org.jmlspecs.util

Methods in org.jmlspecs.util with parameters of type JMLAssertionError
`void`	`RacRunTestCase.checkJmlErr(Class c, JMLAssertionError e)`

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV NEXT

FRAMES NO FRAMES

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.

Uses of Classorg.jmlspecs.jmlrac.runtime.JMLAssertionError

Uses of Class
org.jmlspecs.jmlrac.runtime.JMLAssertionError