org.jmlspecs.jml4.rac.runtime
Class JMLExitNormalPostconditionError

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.JMLNormalPostconditionError
                      org.jmlspecs.jml4.rac.runtime.JMLExitNormalPostconditionError

All Implemented Interfaces:

java.io.Serializable, JMLExitPostconditionError

public class JMLExitNormalPostconditionError
extends JMLNormalPostconditionError
implements JMLExitPostconditionError

A JML error class to notify exit normal postcondition violations.

Version:

$Revision: 1.3 $

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

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

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

JMLExitNormalPostconditionError

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

JMLExitNormalPostconditionError

public JMLExitNormalPostconditionError(java.lang.Throwable cause)