org.jmlspecs.jmlrac
Interface RacConstants

All Superinterfaces:

Constants, Constants, Constants

All Known Subinterfaces:

RacVisitor

All Known Implementing Classes:

Main.JmlGenerateAssertionTask, PreValueVars, QInterval, QSet, RacAbstractVisitor, RacPrettyPrinter, Translator, TransUtils, VarGenerator

public interface RacConstants

extends Constants

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).

Version:

$Revision: 1.34 $

Author:

Yoonsik Cheon

Field Summary
static String	MN_CHECK_HC           The method name prefix for methods that check history constraints.
static String	MN_CHECK_INV           The method name prefix for methods that check invariants.
static String	MN_CHECK_POST           The method name prefix for methods that check normal postconditions, often called normal postcondition check methods.
static String	MN_CHECK_PRE           The method name prefix for methods that check method preconditions, often called precondition check methods.
static String	MN_CHECK_XPOST           The method name prefix for methods that check exceptional postconditions, often called exceptional postcondition check methods.
static 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 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 String	MN_INIT           The name of the internal method and the assertion check methods for the constructors.
static String	MN_INTERNAL           The method name prefix for renaming original methods into private internal methods.
static String	MN_MODEL           The method name prefix for access methods generated for model fields.
static String	MN_MODEL_PUBLIC           The method name prefix of access methods generated for model methods.
static 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 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 String	MN_SPEC           The method name prefix for spec_public and spec_protected access methods generated for spec_public and spec_protected fields.
static String	MN_SPEC_PUBLIC           The method name prefix of access methods generated for spec_public and spec_protected methods.
static String	TN_JMLCHECKABLE           The type name of a private delegee field (VN_DELEGEE) of the surrogate class (TN_SURROGATE) for an interface.
static String	TN_JMLSURROGATE           The name of the interface that all surrogate classes have to implement.
static String	TN_JMLUNIT_TEST_POSTFIX           The name of test class generated by jmlunit.
static String	TN_JMLUNIT_TESTDATA_POSTFIX           The name of test case class generated by jmlunit.
static 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 String	TN_SURROGATE           The name of the surrogate class for an interface.
static String	VN_ASSERTION
static String	VN_CATCH_VAR           The name of variables to generate for use in catch clauses.
static String	VN_CLASS_INIT           Name of a static boolean field that indicates whether the initialization of a class or an inteface has been completed.
static String	VN_CONSTRUCTED           Name of a boolean variable that indicates whether an instance finishes its construction.
static String	VN_DELEGEE           Name of a private delegee field of a surrogate class (TN_SURROGATE) for an interface.
static 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 String	VN_EXCEPTION           Name of the exception parameter.
static String	VN_FREE_VAR           The name of local variables to be generated to evaluate varisous JML predicates and expressions.
static String	VN_INIT           Name of a non-static boolean field that indicates whether a class instance, during its construction, has finished its initialization.
static String	VN_OLD_VAR           The name of a private field generated to store the pre-state value of an old expression in postcoditions and history constraints and an old variable appearing in a method specification.
static String	VN_POST_VAR           The name of a local variable generated to store the result of evaluating a specification case of a postcondition
static 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 String	VN_PRECOND
static 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 asssertion check code.
static 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 String	VN_RESULT           The name of a varialbe that holds the return value of the method being assertion checked.
static String	VN_STACK_VAR           Name of the stack variable.
static String	VN_XRESULT           The name of a variable that holds the exceptional result of the method being assertion checked.

 

Fields inherited from interface org.jmlspecs.checker.Constants

ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET

 

Fields inherited from interface org.multijava.mjc.Constants

ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP

 

Fields inherited from interface org.multijava.util.classfile.Constants

ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID

 

Field Detail

TN_SURROGATE

public static final String TN_SURROGATE

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

See Also:

TransInterface

TN_JMLSURROGATE

public static final 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, TransInterface, JMLSurrogate

TN_JMLCHECKABLE

public static final 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, TransInterface, TransClass, TransType

TN_JMLVALUE

public static final 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, TransMethod, TransExpression, PreValueVars

TN_JMLUNIT_TEST_POSTFIX

public static final String TN_JMLUNIT_TEST_POSTFIX

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

TN_JMLUNIT_TESTDATA_POSTFIX

public static final 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.

MN_CHECK_PRE

public static final 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

MN_CHECK_POST

public static final 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

MN_CHECK_XPOST

public static final 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

MN_EVAL_OLD

public static final 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:

TransConstraint, TransType, TransClass, TransInterface

MN_CHECK_INV

public static final 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, TransType, TransClass, TransInterface

MN_CHECK_HC

public static final 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, TransConstraint, TransType, TransClass, TransInterface

MN_INTERNAL

public static final 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:

TransMethod

MN_MODEL

public static final 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.

MN_SPEC

public static final 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.

MN_GHOST

public static final 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.

MN_SPEC_PUBLIC

public static final 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.

MN_MODEL_PUBLIC

public static final 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.

MN_SAVE_TO

public static final 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

MN_RESTORE_FROM

public static final 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

MN_INIT

public static final String MN_INIT

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

VN_ERROR_SET

public static final 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.

VN_PRECOND

public static final String VN_PRECOND

VN_RESULT

public static final String VN_RESULT

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

VN_XRESULT

public static final String VN_XRESULT

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

VN_FREE_VAR

public static final String VN_FREE_VAR

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

See Also:

VarGenerator.freshVar()

VN_CATCH_VAR

public static final String VN_CATCH_VAR

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

See Also:

VarGenerator.freshCatchVar()

VN_OLD_VAR

public static final String VN_OLD_VAR

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

See Also:

VarGenerator.freshOldVar()

VN_PRE_VAR

public static final 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:

VarGenerator.freshPreVar()

VN_POST_VAR

public static final 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:

VarGenerator.freshPostVar()

VN_ASSERTION

public static final String VN_ASSERTION

VN_EXCEPTION

public static final String VN_EXCEPTION

Name of the exception parameter.

VN_STACK_VAR

public static final 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, VarGenerator.freshStackVar()

VN_INIT

public static final 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()

VN_CLASS_INIT

public static final String VN_CLASS_INIT

Name of a static boolean field that indicates whether the initialization of a class or an inteface 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 asssertion checks while a class has not fininished its initialization.

See Also:

VN_INIT, ConstructorWrapper.generate(), TransType.finalizeTranslation()

VN_DELEGEE

public static final 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

VN_RAC_LEVEL

public static final 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 maded to the method JMLChecker.setLevel(Class, int) and JMLChecker.getLevel(Class).

See Also:

JMLChecker.setLevel(Class, int), JMLChecker.getLevel(Class)

VN_RAC_COMPILED

public static final 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 asssertion check code. If the value of this field is changed, the same change should be maded to the method JMLChecker.isRacCompiled(Class).

See Also:

JMLChecker.isRACCompiled(Class)

VN_CONSTRUCTED

public static final 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()