org.jmlspecs.jmlrac.runtime
Class JMLPreconditionError

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

All Implemented Interfaces:

Serializable

Direct Known Subclasses:

JMLEntryPreconditionError, JMLInternalPreconditionError

public abstract class JMLPreconditionError

extends JMLAssertionError

A JML exception class for notifying precondition violations. The runtime assertion checker makes a distinction among precondition violations: internal precondition violations and entry precondition violations. An internal precondition violation refers to a precondition violation that arises inside the execution of the method, say M, that we are interested in. An entry precondition violation refers to a violation concerned with the method M's precondition.

Version:

$Revision: 1.4 $

Author:

Yoonsik Cheon

See Also:

JMLInternalPreconditionError, JMLEntryPreconditionError

Field Summary

 

Fields inherited from class org.jmlspecs.jmlrac.runtime.JMLAssertionError

className, locations, methodName

 

Fields inherited from class java.lang.Error

 

Fields inherited from class java.lang.Throwable

 

Constructor Summary
protected	JMLPreconditionError(String message, String className, String methodName, Set locations)           Constructs a new instance.
protected	JMLPreconditionError(String className, String methodName, Set locations)           Constructs a new instance.
protected	JMLPreconditionError(Throwable cause)

 

Method Summary

 

Methods inherited from class org.jmlspecs.jmlrac.runtime.JMLAssertionError

className, getMessage, locations, message, methodName

 

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

 

Constructor Detail

JMLPreconditionError

protected JMLPreconditionError(String className,
                               String methodName,
                               Set locations)

Constructs a new instance.

JMLPreconditionError

protected JMLPreconditionError(String message,
                               String className,
                               String methodName,
                               Set locations)

Constructs a new instance.

JMLPreconditionError

protected JMLPreconditionError(Throwable cause)