Package org.jmlspecs.jmlrac.runtime

Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc).

See:
Description

Interface Summary

JMLCheckable	The common behavior of all runtime assertion checkable classes.
JMLExitPostconditionError	A mark interface for JML exit postcondition errors.
JMLInternalPostconditionError	A mark interface for JML internal postcondition errors.
JMLOption	An interface to provide compile-time and runtime options.

Class Summary

JMLChecker	A class to set various runtime options and to check and report runtime assertion violations.
JMLChecker.CoverageCount
JMLOldExpressionCache	An abstraction of caches for JML old expressions.
JMLOldExpressionCache.Key	A class for representing keys for cache objects.
JMLRacBigIntegerUtils
JMLRacUtil
JMLRacValue	A class for denoting JML expressible values for the runtime assertion checker.
JMLSurrogate	The common behavior of all surrogate classes.
JMLSurrogate.MapKey	A class for implementing keys for the method cache.

Exception Summary

JMLNonExecutableException

Thrown by generated runtime assertion check code to indicate that an attempt has been made to execute a JML expression that is not executable.

Error Summary

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

Package org.jmlspecs.jmlrac.runtime Description

Classes for use during runtime assertion checking for code compiled with JML's runtime assertion checking compiler (jmlc). The runtime assertion checker allows one to check the Java Modeling Language (JML) assertions at runtime when the programs are being executed. It adds assertion check code to the generated Java bytecode that checks pre- and postconditions, invariants, and history constraints. The classes in this package are used at runtime to control and perform assertion checks.

The source code for this package uses the GNU Lesser General Public License, since it is part of the JML runtime libraries.