JML

org.jmlspecs.jmlrac.runtime
Class JMLAssertionError

java.lang.Object
  extended byjava.lang.Throwable
      extended byjava.lang.Error
          extended byorg.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);
 

Constructor Detail

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)
Method Detail

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

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.