org.jmlspecs.jml4.rac.runtime
Class JMLAssertionError

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

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

JMLConstraintError, JMLEvaluationError, JMLHistoryConstraintError, JMLIntraconditionError, JMLInvariantError, JMLPostconditionError, JMLPreconditionError

public abstract class JMLAssertionError
extends java.lang.Error

An abstract error class to notify all kinds of runtime assertion violations.

Version:

$Revision: 1.8 $

Author:

Yoonsik Cheon and Amritam

See Also:

Serialized Form

Nested Class Summary

static class

JMLAssertionError.Location Data structure class to represent a source code location including file name, line number, and character position.

Constructor Summary

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

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

java.lang.String	className() Return the name of class that contains the violated assertion.
java.lang.String	getMessage() Returns the associated message along with optional location and state information.
java.util.Set<JMLAssertionError.Location>	locations() Return the locations.
java.lang.String	message() Return the associated message.
java.lang.String	methodName() Return the name of method that contains the violated assertion.
java.util.Map<java.lang.String,java.lang.Object>	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

JMLAssertionError

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

JMLAssertionError

public JMLAssertionError(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 Detail

className

public java.lang.String className()

Return the name of class that contains the violated assertion. The result is not null.

  ensures \result.equals(className);
 

Returns:

a class name

methodName

public java.lang.String methodName()

Return the name of method that contains the violated assertion. The result may be null, e.g., in case of invariant or history constraint violations.

  ensures \result == null || \result.equals(methodName);
 

Returns:

a method name

message

public java.lang.String message()

Return the associated message.

Returns:

a String message

locations

public java.util.Set<JMLAssertionError.Location> locations()

Return the locations. The result is not null and contains strings of the form: "file_name:line_no:column_no".

  ensures \result == locations;
 

Returns:

locations

values

public java.util.Map<java.lang.String,java.lang.Object> values()

getMessage

public java.lang.String getMessage()

Returns the associated message along with optional location and state information.

Overrides:

getMessage in class java.lang.Throwable