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

Class Specifications

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

Specifications inherited from class Error

initially java.lang.Error.serialVersionUID == 4980196508277280342;

Specifications inherited from class Throwable

public invariant \nonnullelements(this._stackTrace); public represents causeSet <- this._cause != this;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Model Field Summary

 

Model fields inherited from class java.lang.Throwable

_cause, _message, _stackTrace, causeSet

 

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

 

Ghost Field Summary

 

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

 

Field Summary
[spec_public] protected  String	className
[spec_public] protected  Set	locations
[spec_public] protected  String	methodName           Name of the method that contains the violated assertion.

 

Fields inherited from class java.lang.Error

 

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

 

Model Method Summary

 

Model methods inherited from class java.lang.Throwable

initMessage, standardThrowable, standardThrowable, standardThrowable, standardThrowable

 

Model methods inherited from class java.lang.Object

hashValue

 

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

Specifications: spec_public

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.

Specifications: spec_public

locations

protected Set locations

Specifications: spec_public non_null

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.

Returns:

a class name

Specifications:

ensures \result .equals(this.className);

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.

Returns:

a method name

Specifications:

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

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".

Returns:

locations

Specifications:

ensures \result == this.locations;

getMessage

public String getMessage()

Return the associated message concatenated with location information.

Overrides:

getMessage in class Throwable

Returns:

a String message

Specifications: (inherited)pure

     also

ensures \result != null;

Specifications inherited from overridden method in class Throwable:
       pure nullable

public normal_behavior
ensures \result == this._message;