org.jmlspecs.jml4.rac.runtime
Class JMLIntraconditionError

java.lang.Object
  java.lang.Throwable
      java.lang.Error
          org.jmlspecs.jml4.rac.runtime.JMLAssertionError
              org.jmlspecs.jml4.rac.runtime.JMLIntraconditionError

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

JMLAssertError, JMLAssumeError, JMLDebugError, JMLHenceByError, JMLLoopInvariantError, JMLLoopVariantError, JMLUnreachableError

public abstract class JMLIntraconditionError
extends JMLAssertionError

A JML exception class to signal intracondition violations.

Version:

1.0

Author:

Yoonsik Cheon and Amritam

See Also:

Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class org.jmlspecs.jml4.rac.runtime.JMLAssertionError

JMLAssertionError.Location

Constructor Summary

JMLIntraconditionError(java.lang.String className, java.lang.String methodName, java.util.Set<JMLAssertionError.Location> assertions, java.util.Map<java.lang.String,java.lang.Object> state)

JMLIntraconditionError(java.lang.String message, java.lang.String className, java.lang.String methodName, java.util.Set<JMLAssertionError.Location> assertions, java.util.Map<java.lang.String,java.lang.Object> state)
Create a constructor with an associated message

Method Summary

Methods inherited from class org.jmlspecs.jml4.rac.runtime.JMLAssertionError

className, getMessage, locations, message, methodName, values

Methods inherited from class java.lang.Throwable

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

Methods inherited from class java.lang.Object

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

Constructor Detail

JMLIntraconditionError

public JMLIntraconditionError(java.lang.String className,
                              java.lang.String methodName,
                              java.util.Set<JMLAssertionError.Location> assertions,
                              java.util.Map<java.lang.String,java.lang.Object> state)

JMLIntraconditionError

public JMLIntraconditionError(java.lang.String message,
                              java.lang.String className,
                              java.lang.String methodName,
                              java.util.Set<JMLAssertionError.Location> assertions,
                              java.util.Map<java.lang.String,java.lang.Object> state)

Create a constructor with an associated message