JML

org.jmlspecs.jmlrac.runtime
Class JMLNonExecutableException

java.lang.Object
  extended byjava.lang.Throwable
      extended byjava.lang.Exception
          extended byjava.lang.RuntimeException
              extended byorg.jmlspecs.jmlrac.runtime.JMLNonExecutableException
All Implemented Interfaces:
Serializable

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 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:
TransExpression

Field Summary
 
Fields inherited from class java.lang.RuntimeException
 
Fields inherited from class java.lang.Throwable
 
Constructor Summary
JMLNonExecutableException()
          Constructs a new instance.
JMLNonExecutableException(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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Constructor Detail

JMLNonExecutableException

public JMLNonExecutableException()
Constructs a new instance.


JMLNonExecutableException

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


JML

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.