org.jmlspecs.jmlrac.runtime
Class JMLAssertionError

java.lang.Object
  java.lang.Throwable
      java.lang.Error
          org.jmlspecs.jmlrac.runtime.JMLAssertionError

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

JMLEvaluationError, JMLHistoryConstraintError, JMLIntraconditionError, JMLInvariantError, JMLPostconditionError, JMLPreconditionError

public abstract class JMLAssertionError

extends Error

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

Version:

$Revision: 1.8 $

Author:

Yoonsik Cheon

Field Summary
protected  String	className           Name of the class or interface that contains the violated assertion.
protected  Set	locations           The locations (strings of the form: "file_name:line_num:column_num") of the violated assertion.
protected  String	methodName           Name of the method that contains the violated assertion.

 

Fields inherited from class java.lang.Error

 

Fields inherited from class java.lang.Throwable

 

Constructor Summary
protected	JMLAssertionError(String message)           Creates a new JMLAssertionError instance with given message.
protected	JMLAssertionError(String message, Throwable cause)
protected	JMLAssertionError(Throwable cause)

 

Method Summary
String	className()           Return the name of class that contains the violated assertion.
String	getMessage()           Return the associated message concatenated with location information.
Set	locations()           Return the locations.
String	message()           Return the associated message.
String	methodName()           Return the name of method that contains the violated assertion.

 

Methods inherited from class java.lang.Throwable

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

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

 

Field Detail

className

protected String className

Name of the class or interface that contains the violated assertion.

 invariant className != null;
 

methodName

protected String methodName

Name of the method that contains the violated assertion. It can be null if the assertion is not associated with any particular methods, e.g., invariants or history constraints.

locations

protected Set locations

The locations (strings of the form: "file_name:line_num:column_num") of the violated assertion. The violated assertion might be specified in several different places due to specification inheritance.

 invariant locations != null && 
  (\forall Object o; locations.contains(o); o instanceof String);
 

JMLAssertionError

protected JMLAssertionError(String message)

Creates a new JMLAssertionError instance with given message.

Parameters:

message - an informative message; can be null.

JMLAssertionError

protected JMLAssertionError(String message,
                            Throwable cause)

JMLAssertionError

protected JMLAssertionError(Throwable cause)

className

public 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 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 String message()

Return the associated message.

Returns:

a String message

locations

public Set 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

getMessage

public String getMessage()

Return the associated message concatenated with location information.

 also
   ensures \result != null;
 

Overrides:

getMessage in class Throwable

Returns:

a String message