JML

org.jmlspecs.jmlrac.runtime
Class JMLChecker

java.lang.Object
  extended byorg.jmlspecs.jmlrac.runtime.JMLChecker
All Implemented Interfaces:
JMLOption

public abstract class JMLChecker
extends Object
implements JMLOption

A class to set various runtime options and to check and report runtime assertion violations.

Version:
$Revision: 1.25 $
Author:
Yoonsik Cheon

Nested Class Summary
static class JMLChecker.CoverageCount
           
 
Field Summary
static JMLNonExecutableException ANGELIC_EXCEPTION
          An exception object indicating angelic undefinedness.
static HashMap classes
          A map from fully quallified class names to class objects.
static int CONSTRAINT
           
protected static Map coverage
          A map to hold information about coverage
static RuntimeException DEMONIC_EXCEPTION
          An exception object indicating demonic undefinedness.
static int INTRACONDITION
           
static int INVARIANT
           
protected static int level
          Runtime option indicating the assertion check level, the kinds of assertions to be checked.
static Object NO_CLASS
          A unique object to indicate non-existing class.
static int POSTCONDITION
           
static int PRECONDITION
           
static int PROTOCOL
           
private static boolean reportAssumptionViolation
          Indicates whether an assumption violation should be reported to the user by throwing an appropriate exception
protected static Set threadsBeingChecked
          Stores a flag per thread to turn assertion check on/off for every thread to avoid recursive assertion checking.
 
Fields inherited from interface org.jmlspecs.jmlrac.runtime.JMLOption
ALL, NONE, PRECONDITIONS_ONLY
 
Constructor Summary
JMLChecker()
           
 
Method Summary
static void addCoverage(String location, boolean value)
           
static void clearCoverage()
           
static void enter()
          Indicates the start of assertion check by the current thread.
static void exit()
          Indicates the end of assertion check for the current thread.
static int getLevel()
          Returns the current global runtime assertion check level.
static int getLevel(Class clazz)
          Returns the current runtime assertion check level of the given class, clazz.
private static Class getRacClass(Class clazz)
          Returns the runtime assertion checker class of the given class, clazz.
static Object getSurrogate(String name, Class clazz, Object thisObj)
          Returns a surrogate object, an instance of the given surrogate class clazz, that is suitable for statically calling JML access methods on the object thisObj.
static boolean inheritedFrom(Class clazz, String name, Class[] params)
          Returns true if a method named name with the formal parameter types, params, can be inherited from the type, class, or its supertypes.
static boolean isActive(int type)
          Determines if the runtime code for checking this type of assertion should be executed.
static boolean isRACCompiled(Class clazz)
          Returns true only if the given class, clazz, is compiled with runtime assertion check code.
static boolean reportAssumptionViolation()
          Indicates whether an assumption violation should be reported to the user by throwing an appropriate exception (i.e., JMLIntraconditionError).
static void reportAssumptionViolation(boolean flag)
          Sets whether an assumption violation should be reported to the user by throwing an appropriate exception (i.e., JMLIntraconditionError).
static void reportCoverage(PrintStream writer)
           
static void setLevel(int l)
          Sets the global runtime assertion check level to the level l.
static void setLevel(Class clazz, int l)
          Sets the runtime assertion check level of the class, clazz, to the level, l.
static String toString(boolean i)
          Returns the string representation of the given argument.
static String toString(byte i)
          Returns the string representation of the given argument.
static String toString(char i)
          Returns the string representation of the given argument.
static String toString(double value)
          Returns the string representation of the given argument.
static String toString(float value)
          Returns the string representation of the given argument.
static String toString(int i)
          Returns the string representation of the given argument.
static String toString(Object obj)
          Returns the result of invoking the toString method to the argument, obj.
static String toString(long i)
          Returns the string representation of the given argument.
static String toString(short i)
          Returns the string representation of the given argument.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

level

protected static int level
Runtime option indicating the assertion check level, the kinds of assertions to be checked. The default is JMLOption.ALL.

  public invariant level == JMLOption.NONE || 
    level == JMLOption.PRECONDITIONS_ONLY ||
    level == JMLOption.ALL;
 


threadsBeingChecked

protected static Set threadsBeingChecked
Stores a flag per thread to turn assertion check on/off for every thread to avoid recursive assertion checking. The flag is "created" for every thread on demand basis taking default value to be true.


reportAssumptionViolation

private static boolean reportAssumptionViolation
Indicates whether an assumption violation should be reported to the user by throwing an appropriate exception


classes

public static HashMap classes
A map from fully quallified class names to class objects. If a class name is mapped to the object NO_CLASS, it means that there is no such named class. This map is used by the generated method rac$forName(String), to save class lookup and load time.


NO_CLASS

public static final Object NO_CLASS
A unique object to indicate non-existing class. This constant is used as an entry in the map classes.


ANGELIC_EXCEPTION

public static final JMLNonExecutableException ANGELIC_EXCEPTION
An exception object indicating angelic undefinedness. Instead of creating a new exception object for each occurrence of angelic undefinedness, this global constant is used. Creating an exception object is costly.


DEMONIC_EXCEPTION

public static final RuntimeException DEMONIC_EXCEPTION
An exception object indicating demonic undefinedness. Instead of creating a new exception object for each occurrence of demonic undefinedness, this global constant is used. Creating an exception object is costly.


PRECONDITION

public static final int PRECONDITION

POSTCONDITION

public static final int POSTCONDITION

INVARIANT

public static final int INVARIANT

CONSTRAINT

public static final int CONSTRAINT

INTRACONDITION

public static final int INTRACONDITION

PROTOCOL

public static final int PROTOCOL

coverage

protected static Map coverage
A map to hold information about coverage

Constructor Detail

JMLChecker

public JMLChecker()
Method Detail

isRACCompiled

public static boolean isRACCompiled(Class clazz)
Returns true only if the given class, clazz, is compiled with runtime assertion check code.


setLevel

public static void setLevel(int l)
Sets the global runtime assertion check level to the level l.

 normal_behavior
   requires l == NONE || l == PRECONDITIONS_ONLY || l == ALL;
   assignable level;
   ensures level == l;
 


getLevel

public static int getLevel()
Returns the current global runtime assertion check level. The returned value is NONE, PRECONDITIONS_ONLY, or ALL.

 normal_behavior
   assignable \nothing;
   ensures \result == level;
 


setLevel

public static void setLevel(Class clazz,
                            int l)
Sets the runtime assertion check level of the class, clazz, to the level, l. If no such class exists, this method has no effect.

 normal_behavior
   requires l == NONE || l == PRECONDITIONS_ONLY || l == ALL;
   assignable \not_specified;
 


getRacClass

private static Class getRacClass(Class clazz)
Returns the runtime assertion checker class of the given class, clazz. If the given class is an interface, its surrogate class is returned; otherwise, the given class itself is returned.


inheritedFrom

public static boolean inheritedFrom(Class clazz,
                                    String name,
                                    Class[] params)
Returns true if a method named name with the formal parameter types, params, can be inherited from the type, class, or its supertypes. If either clazz or name is null, false is returned.


getLevel

public static int getLevel(Class clazz)
Returns the current runtime assertion check level of the given class, clazz. The returned value is NONE, PRECONDITIONS_ONLY, or ALL. If no such class is found or the class is not compiled with runtime assertion check code, NONE is returned.


reportAssumptionViolation

public static boolean reportAssumptionViolation()
Indicates whether an assumption violation should be reported to the user by throwing an appropriate exception (i.e., JMLIntraconditionError). The default is to report assumption violations.

See Also:
reportAssumptionViolation(boolean)

reportAssumptionViolation

public static void reportAssumptionViolation(boolean flag)
Sets whether an assumption violation should be reported to the user by throwing an appropriate exception (i.e., JMLIntraconditionError). The default is to report assumption violations.

See Also:
reportAssumptionViolation()

enter

public static void enter()
Indicates the start of assertion check by the current thread.

 normal_behavior
   old Thread cur = Thread.currentThread();
   requires !threadsBeingChecked.contains(cur);
   assignable threadsBeingChecked;
   ensures (* threadsBeingChecked.add(cur) *);
 


exit

public static void exit()
Indicates the end of assertion check for the current thread.

 normal_behavior
   old Thread cur = Thread.currentThread();
   requires threadsBeingChecked.contains(cur);
   assignable threadsBeingChecked;
   ensures (* threadsBeingChecked.remove(cur) *);
 


isActive

public static boolean isActive(int type)
Determines if the runtime code for checking this type of assertion should be executed. It depends on three factors 1. Assertion check is not turned off at runtime 2. Runtime option permits you to execute this code 3. This method is not a part of another assertion already being checked in this thread

Parameters:
type - Type of the current assertion check (e.g., PRECONDITION)
Returns:
true if the current assertion can be checked; false otherwise.

getSurrogate

public static Object getSurrogate(String name,
                                  Class clazz,
                                  Object thisObj)
Returns a surrogate object, an instance of the given surrogate class clazz, that is suitable for statically calling JML access methods on the object thisObj. The argument clazz must be a surrogate class. If the object thisObj itself is a surrogate, the delegee's surrogate cache is looked upon for an existing surrogate object or creating a new one; otherwise, the object's surrogate cache is looked upon. The arument name equals to clazz.getName(); it is passed in for the performance reason, i.e., to prevent extra calls to the method getName().


toString

public static String toString(Object obj)
Returns the result of invoking the toString method to the argument, obj. If the argument is null, "null" is returned. If the invocation encounters an exception, "UNKNOWN" is returned; otherwise, the result of invocation is returned.


toString

public static String toString(boolean i)
Returns the string representation of the given argument.


toString

public static String toString(byte i)
Returns the string representation of the given argument.


toString

public static String toString(char i)
Returns the string representation of the given argument.


toString

public static String toString(int i)
Returns the string representation of the given argument.


toString

public static String toString(short i)
Returns the string representation of the given argument.


toString

public static String toString(long i)
Returns the string representation of the given argument.


toString

public static String toString(float value)
Returns the string representation of the given argument.


toString

public static String toString(double value)
Returns the string representation of the given argument.


clearCoverage

public static void clearCoverage()

addCoverage

public static void addCoverage(String location,
                               boolean value)

reportCoverage

public static void reportCoverage(PrintStream writer)

JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.