org.jmlspecs.jml4.rac.runtime
Class JMLLoopInvariantError

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

All Implemented Interfaces:

java.io.Serializable

public class JMLLoopInvariantError
extends JMLIntraconditionError

A JML error class to report loop invariant violations.

Version:

1.0

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

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

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

JMLLoopInvariantError

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