Uses of Package
org.jmlspecs.jml4.rac.runtime

Packages that use org.jmlspecs.jml4.rac.runtime

org.jmlspecs.jml4.rac.runtime

Classes in org.jmlspecs.jml4.rac.runtime used by org.jmlspecs.jml4.rac.runtime

JMLAssertionError
An abstract error class to notify all kinds of runtime assertion violations.

JMLAssertionError.Location
Data structure class to represent a source code location including file name, line number, and character position.

JMLCheckable
The common behavior of all runtime assertion checkable classes.

JMLExceptionalPostconditionError
A JML error class to notify exceptional postcondition violations.

JMLExitPostconditionError
A mark interface for JML exit postcondition errors.

JMLInternalPostconditionError
A mark interface for JML internal postcondition errors.

JMLIntraconditionError
A JML exception class to signal intracondition violations.

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.

JMLNormalPostconditionError
A JML error class to notify normal postcondition violations.

JMLOption
An interface to provide compile-time and runtime options.

JMLPostconditionError
A JML error class to notify postcondition violations.

JMLPreconditionError
A JML exception class for notifying precondition violations.

JMLRacValue
A class for denoting JML expressible values for the runtime assertion checker.

JMLSurrogate
The common behavior of all surrogate classes.