JMLChecker

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jml4.rac.runtime
Class JMLChecker

java.lang.Object
  org.jmlspecs.jml4.rac.runtime.JMLChecker

All Implemented Interfaces:: JMLOption

public abstract class JMLChecker
extends java.lang.Object
implements JMLOption
extends java.lang.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 java.util.HashMap<java.lang.String,java.lang.Class<?>>`	`classes` A map from fully qualified class names to class objects.
`static int`	`CONSTRAINT`
`static java.lang.RuntimeException`	`DEMONIC_EXCEPTION` An exception object indicating demonic undefinedness.
`static int`	`INTRACONDITION`
`static int`	`INVARIANT`
`static java.lang.Class<?>`	`NO_CLASS` A unique object to indicate non-existing class.
`static int`	`POSTCONDITION`
`static int`	`PRECONDITION`
`static int`	`PROTOCOL`

Fields inherited from interface org.jmlspecs.jml4.rac.runtime.JMLOption
`ALL, NONE, PRECONDITIONS_ONLY`

Constructor Summary
`JMLChecker()`

Method Summary
`static void`	`addCoverage(java.lang.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(java.lang.Class<?> clazz)` Returns the current runtime assertion check level of the given class, `clazz`.
`static java.lang.Object`	`getSurrogate(java.lang.String name, java.lang.Class<?> clazz, java.lang.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(java.lang.Class<?> clazz, java.lang.String name, java.lang.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(java.lang.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(java.io.PrintStream writer)`
`static void`	`setLevel(java.lang.Class clazz, int l)` Sets the runtime assertion check level of the class, `clazz`, to the level, `l`.
`static void`	`setLevel(int l)` Sets the global runtime assertion check level to the level `l`.
`static java.lang.String`	`toString(boolean i)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(byte i)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(char i)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(double value)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(float value)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(int i)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(long i)` Returns the string representation of the given argument.
`static java.lang.String`	`toString(java.lang.Object obj)` Returns the result of invoking the `toString` method to the argument, `obj`.
`static java.lang.String`	`toString(short i)` Returns the string representation of the given argument.

Methods inherited from class java.lang.Object
`equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

classes

public static java.util.HashMap<java.lang.String,java.lang.Class<?>> classes

A map from fully qualified 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 java.lang.Class<?> 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 java.lang.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

See Also:: Constant Field Values

POSTCONDITION

public static final int POSTCONDITION

See Also:: Constant Field Values

INVARIANT

public static final int INVARIANT

See Also:: Constant Field Values

CONSTRAINT

public static final int CONSTRAINT

See Also:: Constant Field Values

INTRACONDITION

public static final int INTRACONDITION

See Also:: Constant Field Values

PROTOCOL

public static final int PROTOCOL

See Also:: Constant Field Values

Constructor Detail

JMLChecker

public JMLChecker()

Method Detail

isRACCompiled

public static boolean isRACCompiled(java.lang.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(java.lang.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;

inheritedFrom

public static boolean inheritedFrom(java.lang.Class<?> clazz,
                                    java.lang.String name,
                                    java.lang.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(java.lang.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 java.lang.Object getSurrogate(java.lang.String name,
                                            java.lang.Class<?> clazz,
                                            java.lang.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 java.lang.String toString(java.lang.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.