org.jmlspecs.jmlrac
Class AssertionMethod

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.AssertionMethod

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

Direct Known Subclasses:

InvariantLikeMethod, PreOrPostconditionMethod

public abstract class AssertionMethod

extends TransUtils

An abstract class for generating assertion check methods for specific kinds of assertions such as preconditions, normal and exceptional postconditions, invariants and (history) constraints. The generated assertion check methods inherit the superclass's assertions by dynamically invoking the superclass's corresponding assertion check methods. For example, the precondition check method of a method, m, invokes dynamically the m's precondition method of the superclass if the method m is overriden in the subclass. In general, the following rules are applied for inheriting assertions.

• Method specifications such as preconditions and postconditions are inherited by the subclass, but only for intance (non-static) methods. That is, class (static) method specifications are not inherited by subclasses. In addition, method specifications for constructors are not inherited by subclasses.

• Both static and non-static invariants are inherited by subclasses.

• Both static and non-static constraints are inherited by subclasses. However, the inheritance of constraints is subjected to the strong and weak behavioral subtyping, specified by the weakly annotation in the extends clause. Not implemented yet!

The class is implemented with a variant of the Template Pattern [GoF95]. The abstract method generate is supposed to call the methods buildHeader and checker, respectively, to compose the header and the body of the assertion method. The method checker calls the query method canInherit to decide whether to generate code for inheriting specifications or not. The actual code for inheritance is generated by calling the method inheritAssertion.

  generate {abstract}
    buildHeader
    checker
      canInherit {abstract}
      inheritAssertion
 

Version:

$Revision: 1.8 $

Author:

Yoonsik Cheon

Field Summary
protected  String	exceptionToThrow           name of exception class to be thrown if assertions are violated.
protected  boolean	isStatic           static-ness of assertion method
protected  String	javadoc           Javadoc comment to be added to the generated method.
protected  String	methodIdentification           name of the target method for printing assertion violation error.
protected  String	methodName           name of assertion method
protected  String	prefix           Name prefix of the method to be inherited, e.g., MN_CHECK_PRE
protected  JmlTypeDeclaration	typeDecl           target type declaration for generating assertion methods

 

Fields inherited from class org.jmlspecs.jmlrac.TransUtils

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

Fields inherited from interface org.jmlspecs.jmlrac.RacConstants

MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT

 

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

 

Constructor Summary

AssertionMethod()

 

Method Summary
protected  StringBuffer	buildHeader(String returnType, String name, JFormalParameter[] parameters, CClassType[] exceptions)           Builds and returns a method header as a string.
protected abstract  boolean	canInherit()           Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass.
protected  String	checker(boolean initValue, RacNode stmt, JFormalParameter[] params)           Returnd the assertion check code (stmt) wrapped with code to inherit superclass's assertions if any, and to signal an assertion violation if it happens at runtime.
abstract  JMethodDeclarationType	generate(RacNode stmt)           Generates and returns an assertion checking method.
protected  boolean	hasExplicitSuperClass()           Returns true if the type being translated has an explicitly specified superclass.
protected abstract  String	inheritAssertion(JFormalParameter[] parameters)           Returnd the code to inherit the superclass's assertions, i.e., to call the superclass's assertion check method and appropriately accumulate the result to the assertion variable (e.g., conjunction).

 

Methods inherited from class org.jmlspecs.jmlrac.TransUtils

applyBigintBinOperator, applyBigintCast, applyBigintToNumber, applyBigintUnOperator, applyUnaryPromoteExpression, beingTested, createBigintConvertionAssertion, defaultValue, dynamicCallName, evalOldName, evalOldName, evalOldName, evalOldName, excludedFromInheritance, getTypeID, initIncludedInInheritance, invariantLikeName, isBigintArray, isMain, modelPublicAccessorName, numberToBigint, specAccessorNeeded, specPublicAccessorName, subtypeConstraintName, toPrintableString, toString, toString, toString, typeToClass, unwrapObject, useReflection, wrappedValue, wrapValue

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

typeDecl

protected JmlTypeDeclaration typeDecl

target type declaration for generating assertion methods

prefix

protected String prefix

Name prefix of the method to be inherited, e.g., MN_CHECK_PRE

isStatic

protected boolean isStatic

static-ness of assertion method

methodName

protected String methodName

name of assertion method

exceptionToThrow

protected String exceptionToThrow

name of exception class to be thrown if assertions are violated.

javadoc

protected String javadoc

Javadoc comment to be added to the generated method.

methodIdentification

protected String methodIdentification

name of the target method for printing assertion violation error.

AssertionMethod

public AssertionMethod()

generate

public abstract JMethodDeclarationType generate(RacNode stmt)

Generates and returns an assertion checking method. Append to the body (stmt) code to check the inherited assertions if any, and code to throw an appropriate exception to notify an assertion violation if it happens at runtime.

Parameters:

stmt - code to evaluate the assertions; the result is supposed to be stored in the variable VN_ASSERTION. A null value means that no assertion is specified or the assertion is not executable.

checker

protected String checker(boolean initValue,
                         RacNode stmt,
                         JFormalParameter[] params)

Returnd the assertion check code (stmt) wrapped with code to inherit superclass's assertions if any, and to signal an assertion violation if it happens at runtime. The assertion check code (stmt), if non-null, evaluates all assertions specified in the class, conjoin the results, and store the final result to the variable VN_ASSERTION, called the assertion variable. The assertion variable is supposed to be declared in the block that encloses the assertion check code.

Parameters:

initValue - initial value of the assertion variable.

stmt - assertion check code to wrap

params - parameters to call the inherited check method if necessary.

inheritAssertion

protected abstract String inheritAssertion(JFormalParameter[] parameters)

Returnd the code to inherit the superclass's assertions, i.e., to call the superclass's assertion check method and appropriately accumulate the result to the assertion variable (e.g., conjunction).

Parameters:

parameters - parameters of the superclass's assertion check method

buildHeader

protected StringBuffer buildHeader(String returnType,
                                   String name,
                                   JFormalParameter[] parameters,
                                   CClassType[] exceptions)

Builds and returns a method header as a string.

Parameters:

returnType - return type

name - method name

parameters - formal parameters

exceptions - checked exceptions

canInherit

protected abstract boolean canInherit()

Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass.

hasExplicitSuperClass

protected boolean hasExplicitSuperClass()

Returns true if the type being translated has an explicitly specified superclass.