org.jmlspecs.jml4.rac.runtime
Class JMLHistoryConstraintError

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

All Implemented Interfaces:

java.io.Serializable

public class JMLHistoryConstraintError
extends JMLAssertionError

A JML error class to notify history constraint violations.

Version:

$Revision: 1.4 $

Author:

Yoonsik Cheon, Amritam Sarcar

See Also:

Serialized Form

Nested Class Summary

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

JMLAssertionError.Location

Constructor Summary

JMLHistoryConstraintError(java.lang.String className, java.lang.String methodName, java.util.Set<JMLAssertionError.Location> assertions, java.util.Map<java.lang.String,java.lang.Object> state)
Creates a new JMLInvariantError instance.

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

JMLHistoryConstraintError

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

Creates a new JMLInvariantError instance.

JMLHistoryConstraintError

public JMLHistoryConstraintError(java.lang.Throwable cause)