JML

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

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.