org.jmlspecs.jml4.rac
Interface RacConstants

All Known Implementing Classes:

ClassDeclarationTranslator, ConstructorBodyTranslator, ConstructorHeaderTranslator, InterfaceDeclarationTranslator, MethodBodyTranslator, MethodHeaderTranslator, QInterval, RacTranslator, StaticAnalysis, Translator, TypeDeclarationTranslator

public interface RacConstants

A set of string constants used by RAC implementation classes. The convention is that a class or interface name starts with TN_ (e.g., TN_SURROGATE), a method name prefix starts with MN_ (e.g., MN_CHECK_PRE), and a variable name prefix starts with VN_ (e.g., VN_DELEGEE).

Author:

Yoonsik Cheon and Amritam Sarcar

Nested Class Summary

static class	RacConstants.Behavior Different types of behavior for heavyweight specification
static class	RacConstants.Condition Different types of Rac condition

Field Summary

static java.lang.String	ANNOTATION
static java.lang.String	AT_GHOST Ghost annotation.
static java.lang.String	AT_MODEL Model annotation.
static java.lang.String	EMPTY_STRING Empty string
static java.lang.String	ENTIRE_CLAUSE Warning message displayed due to non-executability of quantifiers.
static java.lang.String	ERROR_NEVER_CALL Error message indicating that a method should never be called.
static java.lang.String	ERROR_NOT_IMPL Error message indicating an unimplemented feature.
static java.lang.String	ERROR_RAC_IMPL Error message indicating a problem in RAC implementation.
static java.lang.String	GHOST_METHOD_PREFIX Prefix of ghost method name.
static java.lang.String	HELPER
static java.lang.String	ID_INSTANCE_DOLLAR
static java.lang.String	ID_STATIC
static java.lang.String	INTERNAL_CONSTRUCTOR_PREFIX Prefix of internal constructor name.
static java.lang.String	INTERNAL_METHOD_PREFIX Prefix of internal method name.
static java.lang.String	JML_CHECKABLE Interface JMLCheckable used by the RAC runtime system.
static java.lang.String	MN_CHECK_HC The method name prefix for methods that check history constraints.
static java.lang.String	MN_CHECK_INV The method name prefix for methods that check invariants.
static java.lang.String	MN_CHECK_POST The method name prefix for methods that check normal postconditions, often called normal postcondition check methods.
static java.lang.String	MN_CHECK_PRE The method name prefix for methods that check method preconditions, often called precondition check methods.
static java.lang.String	MN_CHECK_XPOST The method name prefix for methods that check exceptional postconditions, often called exceptional postcondition check methods.
static java.lang.String	MN_EVAL_OLD The method name prefix for methods that evaluate, in the pre-state, old expressions appearing in history constraints, for use in the post-state by constraint check methods.
static java.lang.String	MN_GHOST The variable and method name prefix for the private field and a pair of access methods generated for a ghost variable.
static java.lang.String	MN_INIT The name of the internal method and the assertion check methods for the constructors.
static java.lang.String	MN_INTERNAL The method name prefix for renaming original methods into private internal methods.
static java.lang.String	MN_MODEL The method name prefix for access methods generated for model fields.
static java.lang.String	MN_MODEL_PUBLIC The method name prefix of access methods generated for model methods.
static java.lang.String	MN_RESTORE_FROM The method name prefix for the method that restores pre-state values from the private stack field (VN_STACK_VAR) for possible recursive method calls.
static java.lang.String	MN_SAVE_TO The method name prefix for the method that saves pre-state values into the private stack field (VN_STACK_VAR) for possible recursive method calls.
static java.lang.String	MN_SPEC The method name prefix for spec_public and spec_protected access methods generated for spec_public and spec_protected fields.
static java.lang.String	MN_SPEC_PUBLIC The method name prefix of access methods generated for spec_public and spec_protected methods.
static java.lang.String	MODEL_METHOD_PREFIX Prefix of model method name.
static java.lang.String	NON_EXEC
static java.lang.String	PKG_RAC_RUNTIME
static java.lang.String	RAC_TMP_FILE_EXTENSION
static java.lang.String	RAC_TMP_FILE_PREFIX
static java.lang.String	TN_BOOLEAN
static java.lang.String	TN_CONSTRAINT_ERROR
static java.lang.String	TN_ENTRY_PRECONDITON_ERROR
static java.lang.String	TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR
static java.lang.String	TN_EXIT_NORMAL_POSTCONDITION_ERROR
static java.lang.String	TN_INVARIANT_ERROR
static java.lang.String	TN_JMLCACHE The name of a special wrapper class that can encapsulate two special values in addition to Java regular values: undefined and non-executable.
static java.lang.String	TN_JMLCHECKABLE The type name of a private delegee field (VN_DELEGEE) of the surrogate class (TN_SURROGATE) for an interface.
static java.lang.String	TN_JMLSURROGATE The name of the interface that all surrogate classes have to implement.
static java.lang.String	TN_JMLUNIT_TEST_POSTFIX The name of test class generated by jmlunit.
static java.lang.String	TN_JMLUNIT_TESTDATA_POSTFIX The name of test case class generated by jmlunit.
static java.lang.String	TN_JMLVALUE The name of a special wrapper class that can encapsulate two special values in addition to Java regular values: undefined and non-executable.
static java.lang.String	TN_LOCATION
static java.lang.String	TN_SURROGATE The name of the surrogate class for an interface.
static java.lang.String	TN_VOID
static java.lang.String	VN_ASSERTION
static java.lang.String	VN_CATCH_VAR The name of variables to generate for use in catch clauses.
static java.lang.String	VN_CLASS_INIT Name of a static boolean field that indicates whether the initialization of a class or an interface has been completed.
static java.lang.String	VN_CONSTRUCTED Name of a boolean variable that indicates whether an instance finishes its construction.
static java.lang.String	VN_DELEGEE Name of a private delegee field of a surrogate class (TN_SURROGATE) for an interface.
static java.lang.String	VN_ERROR_SET The name of a set variable that holds information about all the assertion violations detected so far by the runtime assertion checker.
static java.lang.String	VN_EXCEPTION Name of the exception parameter.
static java.lang.String	VN_FREE_VAR The name of local variables to be generated to evaluate varisous JML predicates and expressions.
static java.lang.String	VN_INIT Name of a non-static boolean field that indicates whether a class instance, during its construction, has finished its initialization.
static java.lang.String	VN_MSG
static java.lang.String	VN_NAME
static java.lang.String	VN_OLD_VAR The name of a private field generated to store the pre-state value of an old expression in postconditions and history constraints and an old variable appearing in a method specification.
static java.lang.String	VN_PARAMS
static java.lang.String	VN_POST_VAR The name of a local variable generated to store the result of evaluating a specification case of a postcondition
static java.lang.String	VN_PRE_VAR The name of a private field generated to store the result of precondition evaluation, for reference by the postcondition check methods.
static java.lang.String	VN_PRECOND
static java.lang.String	VN_RAC_COMPILED Name of the static final field generated by the runtime assertion checker to indicate that a type is compiled with the runtime assertion check code.
static java.lang.String	VN_RAC_LEVEL Name of the static field generated by the runtime assertion checker to indicate the per-class runtime assertion check level.
static java.lang.String	VN_RESULT The name of a varialbe that holds the return value of the method being assertion checked.
static java.lang.String	VN_STACK_VAR Name of the stack variable.
static java.lang.String	VN_VALUE_SET
static java.lang.String	VN_XRESULT The name of a variable that holds the exceptional result of the method being assertion checked.

Field Detail

RAC_TMP_FILE_PREFIX

static final java.lang.String RAC_TMP_FILE_PREFIX

See Also:

Constant Field Values

RAC_TMP_FILE_EXTENSION

static final java.lang.String RAC_TMP_FILE_EXTENSION

See Also:

Constant Field Values

EMPTY_STRING

static final java.lang.String EMPTY_STRING

Empty string

See Also:

Constant Field Values

JML_CHECKABLE

static final java.lang.String JML_CHECKABLE

Interface JMLCheckable used by the RAC runtime system.

See Also:

Constant Field Values

AT_GHOST

static final java.lang.String AT_GHOST

Ghost annotation.

See Also:

Constant Field Values

GHOST_METHOD_PREFIX

static final java.lang.String GHOST_METHOD_PREFIX

Prefix of ghost method name.

See Also:

Constant Field Values

AT_MODEL

static final java.lang.String AT_MODEL

Model annotation.

See Also:

Constant Field Values

MODEL_METHOD_PREFIX

static final java.lang.String MODEL_METHOD_PREFIX

Prefix of model method name.

See Also:

Constant Field Values

INTERNAL_METHOD_PREFIX

static final java.lang.String INTERNAL_METHOD_PREFIX

Prefix of internal method name.

See Also:

Constant Field Values

INTERNAL_CONSTRUCTOR_PREFIX

static final java.lang.String INTERNAL_CONSTRUCTOR_PREFIX

Prefix of internal constructor name.

See Also:

Constant Field Values

ERROR_NEVER_CALL

static final java.lang.String ERROR_NEVER_CALL

Error message indicating that a method should never be called.

See Also:

Constant Field Values

ERROR_RAC_IMPL

static final java.lang.String ERROR_RAC_IMPL

Error message indicating a problem in RAC implementation.

See Also:

Constant Field Values

ERROR_NOT_IMPL

static final java.lang.String ERROR_NOT_IMPL

Error message indicating an unimplemented feature.

See Also:

Constant Field Values

TN_SURROGATE

static final java.lang.String TN_SURROGATE

The name of the surrogate class for an interface. The surrogate class is declared as a static inner class of the corresponding interface.

See Also:

InterfaceDeclarationTranslator, Constant Field Values

TN_JMLSURROGATE

static final java.lang.String TN_JMLSURROGATE

The name of the interface that all surrogate classes have to implement. This interface defines a protocol for the surrogate class and the implementing class to communicate with each other for the dynamic delegation of assertion check methods.

See Also:

TN_JMLCHECKABLE, InterfaceDeclarationTranslator, JMLSurrogate, Constant Field Values

TN_JMLCHECKABLE

static final java.lang.String TN_JMLCHECKABLE

The type name of a private delegee field (VN_DELEGEE) of the surrogate class (TN_SURROGATE) for an interface. This interface defines a protocol for the surrogate class and the implementing class to communicate with each other for the dynamic delegation of assertion checks. All generated classes are supposed to implement this interface.

See Also:

VN_DELEGEE, TN_SURROGATE, TN_JMLSURROGATE, JMLCheckable, InterfaceDeclarationTranslator, ClassDeclarationTranslator, TypeDeclarationTranslator, Constant Field Values

TN_JMLVALUE

static final java.lang.String TN_JMLVALUE

The name of a special wrapper class that can encapsulate two special values in addition to Java regular values: undefined and non-executable. This type is used to store pre-state values such as old variables and old expressions into private fields for future references by post-state assertion check methods such as postcondition check methods and constraint check methods.

See Also:

JMLRacValue, MethodDeclarationTranslator, ExpressionTranslator, PreValueManager, Constant Field Values

TN_JMLCACHE

static final java.lang.String TN_JMLCACHE

The name of a special wrapper class that can encapsulate two special values in addition to Java regular values: undefined and non-executable. This type is used to store pre-state values such as old variables and old expressions into private fields for future references by post-state assertion check methods such as postcondition check methods and constraint check methods.

See Also:

Constant Field Values

TN_JMLUNIT_TEST_POSTFIX

static final java.lang.String TN_JMLUNIT_TEST_POSTFIX

The name of test class generated by jmlunit. A jmlunit-generated test class is not compiled by jmlc.

See Also:

Constant Field Values

TN_JMLUNIT_TESTDATA_POSTFIX

static final java.lang.String TN_JMLUNIT_TESTDATA_POSTFIX

The name of test case class generated by jmlunit. A jmlunit-generated test case class is not compiled by jmlc.

See Also:

Constant Field Values

TN_VOID

static final java.lang.String TN_VOID

See Also:

Constant Field Values

TN_BOOLEAN

static final java.lang.String TN_BOOLEAN

See Also:

Constant Field Values

TN_LOCATION

static final java.lang.String TN_LOCATION

See Also:

Constant Field Values

TN_ENTRY_PRECONDITON_ERROR

static final java.lang.String TN_ENTRY_PRECONDITON_ERROR

See Also:

Constant Field Values

TN_EXIT_NORMAL_POSTCONDITION_ERROR

static final java.lang.String TN_EXIT_NORMAL_POSTCONDITION_ERROR

See Also:

Constant Field Values

TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR

static final java.lang.String TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR

See Also:

Constant Field Values

TN_INVARIANT_ERROR

static final java.lang.String TN_INVARIANT_ERROR

See Also:

Constant Field Values

TN_CONSTRAINT_ERROR

static final java.lang.String TN_CONSTRAINT_ERROR

See Also:

Constant Field Values

ID_STATIC

static final java.lang.String ID_STATIC

See Also:

Constant Field Values

ID_INSTANCE_DOLLAR

static final java.lang.String ID_INSTANCE_DOLLAR

See Also:

Constant Field Values

PKG_RAC_RUNTIME

static final java.lang.String PKG_RAC_RUNTIME

See Also:

Constant Field Values

MN_CHECK_PRE

static final java.lang.String MN_CHECK_PRE

The method name prefix for methods that check method preconditions, often called precondition check methods. The name of its precondition check method for a method m declared in a type T, is MN_CHECK_PRE + m + "$" + T.

See Also:

PreconditionMethod, Constant Field Values

MN_CHECK_POST

static final java.lang.String MN_CHECK_POST

The method name prefix for methods that check normal postconditions, often called normal postcondition check methods. The name of its normal postcondition check method for a method m declared in a type T, is MN_CHECK_POST + m + "$" + T.

See Also:

PostconditionMethod, Constant Field Values

MN_CHECK_XPOST

static final java.lang.String MN_CHECK_XPOST

The method name prefix for methods that check exceptional postconditions, often called exceptional postcondition check methods. The name of its exceptional postcondition check method for a method m declared in a type T, is MN_CHECK_XPOST + m + "$" + T.

See Also:

PostconditionMethod, Constant Field Values

MN_EVAL_OLD

static final java.lang.String MN_EVAL_OLD

The method name prefix for methods that evaluate, in the pre-state, old expressions appearing in history constraints, for use in the post-state by constraint check methods. For a type T, two old expression evaluation methods are generated, one for static constraints and other for non-static constraints, whose names are respectively MN_EVAL_OLD + "$" + T + "$" + instance and MN_EVAL_OLD + "$" + T + "$" + static.

See Also:

ConstraintTranslator, TypeDeclarationTranslator, ClassDeclarationTranslator, InterfaceDeclarationTranslator, Constant Field Values

MN_CHECK_INV

static final java.lang.String MN_CHECK_INV

The method name prefix for methods that check invariants. For a type T, two invariant check methods are generated, one for static invariants and the other for non-static invariants, whose names are respectively MN_CHECK_INV + "$" + T + "$" + static and MN_CHECK_INV + "$" + T + "$" + instance.

See Also:

InvariantMethod, TypeDeclarationTranslator, ClassDeclarationTranslator, InterfaceDeclarationTranslator, Constant Field Values

MN_CHECK_HC

static final java.lang.String MN_CHECK_HC

The method name prefix for methods that check history constraints. For a type T, two constraint check methods are generated, one for static constraints and the other for non-static constraints, whose names are respectively MN_CHECK_HC + "$" + T + "$" + static and MN_CHECK_HC + "$" + T + "$" + instance.

See Also:

ConstraintMethod, ConstraintTranslator, TypeDeclarationTranslator, ClassDeclarationTranslator, InterfaceDeclarationTranslator, Constant Field Values

MN_INTERNAL

static final java.lang.String MN_INTERNAL

The method name prefix for renaming original methods into private internal methods. A method, m, of type T is renamed into a method MN_INTERNAL + "$" + m + "$" + T.

See Also:

MethodDeclarationTranslator, Constant Field Values

MN_MODEL

static final java.lang.String MN_MODEL

The method name prefix for access methods generated for model fields. For a model field, v, declared in a type, T, the name of the generated access method is MN_MODEL + v + "$" + T.

See Also:

Constant Field Values

MN_SPEC

static final java.lang.String MN_SPEC

The method name prefix for spec_public and spec_protected access methods generated for spec_public and spec_protected fields. For a spec_public field, v, declared in a type, T, the name of the generated access method is MN_SPEC + v + "$" + T.

See Also:

Constant Field Values

MN_GHOST

static final java.lang.String MN_GHOST

The variable and method name prefix for the private field and a pair of access methods generated for a ghost variable. E.g., for a ghost variable, v, a private field of name MN_GHOST + v is generated; also generated is the same named getter and setter methods.

See Also:

Constant Field Values

MN_SPEC_PUBLIC

static final java.lang.String MN_SPEC_PUBLIC

The method name prefix of access methods generated for spec_public and spec_protected methods. For a spec_public method, m, declared in a type, T, the name of the generated access method is MN_SPEC_PUBLIC + m + "$" + T.

See Also:

Constant Field Values

MN_MODEL_PUBLIC

static final java.lang.String MN_MODEL_PUBLIC

The method name prefix of access methods generated for model methods. For a model method, m, declared in a type, T, the name of the generated access method is MN_MODEL_PUBLIC + m + "$" + T.

See Also:

Constant Field Values

MN_SAVE_TO

static final java.lang.String MN_SAVE_TO

The method name prefix for the method that saves pre-state values into the private stack field (VN_STACK_VAR) for possible recursive method calls.

See Also:

VN_STACK_VAR, MN_RESTORE_FROM, Constant Field Values

MN_RESTORE_FROM

static final java.lang.String MN_RESTORE_FROM

The method name prefix for the method that restores pre-state values from the private stack field (VN_STACK_VAR) for possible recursive method calls.

See Also:

VN_STACK_VAR, MN_SAVE_TO, Constant Field Values

MN_INIT

static final java.lang.String MN_INIT

The name of the internal method and the assertion check methods for the constructors. E.g., internal$$init$ and checkPre$$init$.

See Also:

Constant Field Values

VN_ERROR_SET

static final java.lang.String VN_ERROR_SET

The name of a set variable that holds information about all the assertion violations detected so far by the runtime assertion checker.

See Also:

Constant Field Values

VN_VALUE_SET

static final java.lang.String VN_VALUE_SET

See Also:

Constant Field Values

VN_MSG

static final java.lang.String VN_MSG

See Also:

Constant Field Values

VN_PRECOND

static final java.lang.String VN_PRECOND

See Also:

Constant Field Values

VN_NAME

static final java.lang.String VN_NAME

See Also:

Constant Field Values

VN_PARAMS

static final java.lang.String VN_PARAMS

See Also:

Constant Field Values

VN_RESULT

static final java.lang.String VN_RESULT

The name of a varialbe that holds the return value of the method being assertion checked.

See Also:

Constant Field Values

VN_XRESULT

static final java.lang.String VN_XRESULT

The name of a variable that holds the exceptional result of the method being assertion checked.

See Also:

Constant Field Values

VN_FREE_VAR

static final java.lang.String VN_FREE_VAR

The name of local variables to be generated to evaluate varisous JML predicates and expressions.

See Also:

VariableGenerator.freshVar(), Constant Field Values

VN_CATCH_VAR

static final java.lang.String VN_CATCH_VAR

The name of variables to generate for use in catch clauses.

See Also:

VariableGenerator.freshCatchVar(), Constant Field Values

VN_OLD_VAR

static final java.lang.String VN_OLD_VAR

The name of a private field generated to store the pre-state value of an old expression in postconditions and history constraints and an old variable appearing in a method specification.

See Also:

VariableGenerator.freshOldVar(), Constant Field Values

VN_PRE_VAR

static final java.lang.String VN_PRE_VAR

The name of a private field generated to store the result of precondition evaluation, for reference by the postcondition check methods.

See Also:

VariableGenerator.freshPreVar(), Constant Field Values

VN_POST_VAR

static final java.lang.String VN_POST_VAR

The name of a local variable generated to store the result of evaluating a specification case of a postcondition

See Also:

VariableGenerator.freshPostVar(), Constant Field Values

VN_ASSERTION

static final java.lang.String VN_ASSERTION

See Also:

Constant Field Values

VN_EXCEPTION

static final java.lang.String VN_EXCEPTION

Name of the exception parameter.

See Also:

Constant Field Values

VN_STACK_VAR

static final java.lang.String VN_STACK_VAR

Name of the stack variable. Pre-state values such as preconditions, old variables, and old expressions are stored into, and restored from this variable to make post-state methods (e.g., postcondition check method) refer to right pre-state values in the presence of recursive method calls.

See Also:

MN_SAVE_TO, MN_RESTORE_FROM, VariableGenerator.freshStackVar(), Constant Field Values

VN_INIT

static final java.lang.String VN_INIT

Name of a non-static boolean field that indicates whether a class instance, during its construction, has finished its initialization. Here, by initialization we means the execution of the instance initializers and instance field initializers for the class, which is done after an explicit (or implicit) super call and before the execution of the constructor body (JLS 12.5). The intent here is to disable instance assertion checks while an instance has not finished its initialization.

See Also:

VN_CLASS_INIT, WrapperMethod#generate(), TransType#finalizeTranslation(), Constant Field Values

VN_CLASS_INIT

static final java.lang.String VN_CLASS_INIT

Name of a static boolean field that indicates whether the initialization of a class or an interface has been completed. By initialization, we mean that all static the static initializers and the initializers for static fields (class variables) have been executed (JLS 12.4). The intent here is to disable both static and instance assertion checks while a class has not finished its initialization.

See Also:

VN_INIT, ConstructorWrapper#generate(), TransType#finalizeTranslation(), Constant Field Values

VN_DELEGEE

static final java.lang.String VN_DELEGEE

Name of a private delegee field of a surrogate class (TN_SURROGATE) for an interface. The type of this field is the interface defined by the constant TN_JMLCHECKABLE.

See Also:

TN_JMLCHECKABLE, TN_SURROGATE, Constant Field Values

VN_RAC_LEVEL

static final java.lang.String VN_RAC_LEVEL

Name of the static field generated by the runtime assertion checker to indicate the per-class runtime assertion check level. If the value of this field is changed, the same change should be made to the method JMLChecker.setLevel(Class, int) and JMLChecker.getLevel(Class).

See Also:

JMLChecker.setLevel(Class, int), JMLChecker.getLevel(Class), Constant Field Values

VN_RAC_COMPILED

static final java.lang.String VN_RAC_COMPILED

Name of the static final field generated by the runtime assertion checker to indicate that a type is compiled with the runtime assertion check code. If the value of this field is changed, the same change should be made to the method JMLChecker.isRacCompiled(Class).

See Also:

JMLChecker.isRACCompiled(Class), Constant Field Values

VN_CONSTRUCTED

static final java.lang.String VN_CONSTRUCTED

Name of a boolean variable that indicates whether an instance finishes its construction. I.e., a constructor has completed its execution. This flag is used to prevent assertion check while an object is constructed.

See Also:

ConstructorWrapper#generate(), WrapperMethod#generate(), TransClass#finalizeTranslation(), Constant Field Values

ENTIRE_CLAUSE

static final java.lang.String ENTIRE_CLAUSE

Warning message displayed due to non-executability of quantifiers.

See Also:

Constant Field Values

NON_EXEC

static final java.lang.String NON_EXEC

See Also:

Constant Field Values

ANNOTATION

static final java.lang.String ANNOTATION

See Also:

Constant Field Values

HELPER

static final java.lang.String HELPER

See Also:

Constant Field Values