JMLChecker (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlrac.runtime
Class JMLChecker

java.lang.Object
  org.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

Class Specifications

public invariant org.jmlspecs.jmlrac.runtime.JMLChecker.level == 0||org.jmlspecs.jmlrac.runtime.JMLChecker.level == 1||org.jmlspecs.jmlrac.runtime.JMLChecker.level == java.lang.Integer.MAX_VALUE;

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Nested Class Summary

static class JMLChecker.CoverageCount


Model Field Summary

Model fields inherited from class java.lang.Object

_getClass, objectState, theString

Ghost Field Summary

Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

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


[spec_public] protected static int level


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

[spec_public] 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()


Model Method Summary

Model methods inherited from class java.lang.Object

hashValue

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(non_null Class clazz)
          Returns the current runtime assertion check level of the given class, clazz.

private static Class getRacClass(non_null 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, non_null 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(non_null 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(non_null 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

Specifications: spec_public

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.

Specifications: spec_public non_null

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(non_null 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.

Specifications:: normal_behavior
requires l == 0||l == 1||l == java.lang.Integer.MAX_VALUE;
assignable level;
ensures org.jmlspecs.jmlrac.runtime.JMLChecker.level == l;

getLevel

public static int getLevel()

Returns the current global runtime assertion check level. The returned value is NONE, PRECONDITIONS_ONLY, or ALL.

Specifications:: normal_behavior
assignable \nothing;
ensures \result == org.jmlspecs.jmlrac.runtime.JMLChecker.level;

setLevel

public static void setLevel(non_null 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.

Specifications:: normal_behavior
requires l == 0||l == 1||l == java.lang.Integer.MAX_VALUE;
assignable \not_specified;

getRacClass

private static Class getRacClass(non_null 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,
                                    non_null 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(non_null 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.

Specifications:: normal_behavior
old java.lang.Thread cur = java.lang.Thread.currentThread();
requires !org.jmlspecs.jmlrac.runtime.JMLChecker.threadsBeingChecked.contains(cur);
assignable threadsBeingChecked;
ensures (* threadsBeingChecked.add(cur) *);

exit

public static void exit()

Indicates the end of assertion check for the current thread.

Specifications:: normal_behavior
old java.lang.Thread cur = java.lang.Thread.currentThread();
requires org.jmlspecs.jmlrac.runtime.JMLChecker.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.

Specifications: non_null