org.jmlspecs.jml4.rac.runtime
Class JMLPreconditionError

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

All Implemented Interfaces:

java.io.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, Serialized Form

Nested Class Summary

Nested classes/interfaces inherited from class org.jmlspecs.jml4.rac.runtime.JMLAssertionError

JMLAssertionError.Location

Constructor Summary

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

Method Summary

Methods inherited from class org.jmlspecs.jml4.rac.runtime.JMLAssertionError

className, getMessage, locations, message, methodName, 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

JMLPreconditionError

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