org.jmlspecs.jmlrac.runtime
Class JMLLoopInvariantError

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

All Implemented Interfaces:

Serializable

public class JMLLoopInvariantError

extends JMLIntraconditionError

A JML error class to report loop invariant violations.

Version:

1.0

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

JMLLoopInvariantError(String message, String className, String methodName, Set locations)           Creates a new JMLLoopInvariantError instance.

 

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

JMLLoopInvariantError

public JMLLoopInvariantError(String message,
                             String className,
                             String methodName,
                             Set locations)

Creates a new JMLLoopInvariantError instance.