Package org.jmlspecs.jml4.rac.runtime

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

JMLAssertionError.Location	Data structure class to represent a source code location including file name, line number, and character position.
JMLChecker	A class to set various runtime options and to check and report runtime assertion violations.
JMLChecker.CoverageCount
JMLNonExecutableUtil
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.

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.
JMLConstraintError	A JML error class to notify history constraint violations.
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 an invariant violation.
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.