org.jmlspecs.jml4.rac.runtime
Class JMLNonExecutableException

java.lang.Object
  java.lang.Throwable
      java.lang.Exception
          java.lang.RuntimeException
              org.jmlspecs.jml4.rac.runtime.JMLNonExecutableException

All Implemented Interfaces:

java.io.Serializable

public class JMLNonExecutableException
extends java.lang.RuntimeException

Thrown by generated runtime assertion check code to indicate that an attempt has been made to execute a JML expression that is not executable. The following expressions are statically determined to be non-executable: \not_modified, \fresh, (* ... *), \invariant_for, \is_initialized, \reach, \elemtype, and \lockset. For certain expressions such as quantified expressions, executability is determined dynamically at runtime. If an expression becomes non-executable, its value is contextually determined by the smallest, enclosing boolean expression.

Version:

$Revision: 1.5 $

Author:

Yoonsik Cheon

See Also:

Serialized Form

Constructor Summary

JMLNonExecutableException()
Constructs a new instance.

JMLNonExecutableException(java.lang.String msg)
Constructs a new instance with the given message, msg.

Method Summary

Methods inherited from class java.lang.Throwable

fillInStackTrace, getCause, getLocalizedMessage, getMessage, getStackTrace, initCause, printStackTrace, printStackTrace, printStackTrace, setStackTrace, toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

JMLNonExecutableException

public JMLNonExecutableException()

Constructs a new instance.

JMLNonExecutableException

public JMLNonExecutableException(java.lang.String msg)

Constructs a new instance with the given message, msg.