org.jmlspecs.jml4.rac.runtime
Class JMLEntryPreconditionError

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

All Implemented Interfaces:

java.io.Serializable

public class JMLEntryPreconditionError
extends JMLPreconditionError

A JML error class to notify entry precondition violations. An entry precondition violation refers to an assertion violation concerned with the precondition of the method that we are interested in.

Version:

$Revision: 1.5 $

Author:

Yoonsik Cheon

See Also:

JMLPreconditionError, JMLInternalPreconditionError, Serialized Form

Nested Class Summary

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

JMLAssertionError.Location

Constructor Summary

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

JMLEntryPreconditionError(java.lang.Throwable cause)

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

JMLEntryPreconditionError

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

JMLEntryPreconditionError

public JMLEntryPreconditionError(java.lang.Throwable cause)