- All Implemented Interfaces:
- public class JMLNonExecutableException
- extends 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
(* ... *),
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.
- $Revision: 1.5 $
- Yoonsik Cheon
- See Also:
|Specifications inherited from class Throwable|
public invariant \nonnullelements(this._stackTrace);|
public represents causeSet <- this._cause != this;
|Specifications inherited from class Object|
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;|
public represents _getClass <- \typeof(this);
|Methods inherited from class java.lang.Throwable
fillInStackTrace, getCause, getLocalizedMessage, getMessage, getStackTrace, initCause, printStackTrace, printStackTrace, printStackTrace, setStackTrace, toString
- Constructs a new instance.
public JMLNonExecutableException(String msg)
- Constructs a new instance with the given message,
JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.