Uses of Class
org.jmlspecs.jml4.rac.runtime.JMLAssertionError

Packages that use JMLAssertionError

org.jmlspecs.jml4.rac.runtime

Uses of JMLAssertionError in org.jmlspecs.jml4.rac.runtime

Subclasses of JMLAssertionError in org.jmlspecs.jml4.rac.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	JMLConstraintError A JML error class to notify history constraint violations.
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 an invariant violation.
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.jml4.rac.runtime with parameters of type JMLAssertionError

static boolean	JMLRacUtil.checkErr(java.lang.Class c, JMLAssertionError e) Under the old semantics, ensure that e is an instance of c.
static boolean	JMLRacUtil.matchCause(java.lang.Class c, JMLAssertionError e)

Constructors in org.jmlspecs.jml4.rac.runtime with parameters of type JMLAssertionError

JMLEvaluationError(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.