org.jmlspecs.jmlrac.runtime
Class JMLInternalNormalPostconditionError

java.lang.Object
  java.lang.Throwable
      java.lang.Error
          org.jmlspecs.jmlrac.runtime.JMLAssertionError
              org.jmlspecs.jmlrac.runtime.JMLPostconditionError
                  org.jmlspecs.jmlrac.runtime.JMLNormalPostconditionError
                      org.jmlspecs.jmlrac.runtime.JMLInternalNormalPostconditionError

All Implemented Interfaces:

JMLInternalPostconditionError, Serializable

public class JMLInternalNormalPostconditionError

extends JMLNormalPostconditionError

implements JMLInternalPostconditionError

A JML error class to notify internal normal postcondition violations.

Version:

$Revision: 1.2 $

Author:

Yoonsik Cheon

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

JMLInternalNormalPostconditionError(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

JMLInternalNormalPostconditionError

public JMLInternalNormalPostconditionError(JMLAssertionError e)

Creates a new instance from the given assertion error.