org.jmlspecs.jml4.rac.runtime
Class JMLInternalExceptionalPostconditionError

java.lang.Object
  java.lang.Throwable
      java.lang.Error
          org.jmlspecs.jml4.rac.runtime.JMLAssertionError
              org.jmlspecs.jml4.rac.runtime.JMLPostconditionError
                  org.jmlspecs.jml4.rac.runtime.JMLExceptionalPostconditionError
                      org.jmlspecs.jml4.rac.runtime.JMLInternalExceptionalPostconditionError

All Implemented Interfaces:

java.io.Serializable, JMLInternalPostconditionError

public class JMLInternalExceptionalPostconditionError
extends JMLExceptionalPostconditionError
implements JMLInternalPostconditionError

A JML error class to notify internal exceptional postcondition violations.

Version:

$Revision: 1.2 $

Author:

Yoonsik Cheon

See Also:

Serialized Form

Nested Class Summary

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

JMLAssertionError.Location

Constructor Summary

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

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

JMLInternalExceptionalPostconditionError

public JMLInternalExceptionalPostconditionError(JMLAssertionError e)

Creates a new instance from the given assertion error.