org.jmlspecs.jml4.rac.runtime
Class JMLAssumeError

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

All Implemented Interfaces:

java.io.Serializable

public class JMLAssumeError
extends JMLIntraconditionError

A JML error class to report violations of JML assume specification statements.

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

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

JMLAssumeError(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

JMLAssumeError(java.lang.Throwable cause)
Creates a new instance with the given casue.

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

JMLAssumeError

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

JMLAssumeError

public JMLAssumeError(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

JMLAssumeError

public JMLAssumeError(java.lang.Throwable cause)

Creates a new instance with the given casue.