org.jmlspecs.jmlrac.runtime
Class JMLInternalPreconditionError

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

All Implemented Interfaces:

Serializable

public class JMLInternalPreconditionError

extends JMLPreconditionError

A JML error class to notify internal precondition violations. An internal precondition violation refers to a precondition violation that arises inside the execution of the method that we are interested in.

Version:

$Revision: 1.3 $

Author:

Yoonsik Cheon

See Also:

JMLPreconditionError, 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

JMLInternalPreconditionError(JMLAssertionError e)           Creates a new instance from the given assertion error.

 

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

JMLInternalPreconditionError

public JMLInternalPreconditionError(JMLAssertionError e)

Creates a new instance from the given assertion error.