org.jmlspecs.jmlrac
Class InvariantLikeMethod

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

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

Direct Known Subclasses:

ConstraintMethod, InvariantMethod

public abstract class InvariantLikeMethod

extends AssertionMethod

A class for generating assertion check methods for class-level assertions such as invariants and history constraints. There are two types of class-level assertions: instance (non-static) assertions and class (static) assertions. As thus, two types of assertion check methods are generated. An instance assertion check method checks both the instance and class assertions while a class assertion check method checks only the class assertionss. The generated assertion check methods inherit assertions of its superclass interfaces by dynamically invoking the corresponding assertion methods.

The class implements a variant of the Template Pattern [GoF95], prescribed in the class AssertionMethod.

Version:

$Revision: 1.18 $

Author:

Yoonsik Cheon

See Also:

AssertionMethod

Field Summary

 

Fields inherited from class org.jmlspecs.jmlrac.AssertionMethod

exceptionToThrow, isStatic, javadoc, methodIdentification, methodName, prefix, typeDecl

 

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

InvariantLikeMethod(boolean isStatic, JmlTypeDeclaration typeDecl)           Construct a new InvariantLikeMethod object.

 

Method Summary
protected  StringBuffer	buildHeader(String returnType, String name, JFormalParameter[] parameters, CClassType[] exceptions)           Builds and returns the method header of the assertion check method as a string.
protected  boolean	canInherit()           Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass or interfaces.
protected  String	formalParameters()           Returns the formal parameters of the assertion check method.
JMethodDeclarationType	generate(RacNode stmt)           Generate and return a type-level assertion check method such as invariants and history constraints.
protected  String	inheritAssertion(JFormalParameter[] parameters)           Return the code to inherit assertions of the superclass and interfaces, i.e., to call the assertion check method of the superclass and interfaces and appropriately accumulate the result to the assertion variable (e.g., conjunction).
protected  String	inheritCallArgs()           Returns, in the string form, the arguments for calling supertype's constraint check method.
protected  String	inheritCallArgTypes()           Returns, in the string form, the parameter types of the supertype's assertion check method.
protected  String	inheritFrom(CClass clazz)           Return the code that, if executed, inherits invariant-like assertions such as invariants and constraints from the given class, clazz.
protected  String	nonReflectiveCall(CClass clazz)           Return code that calls non-reflectively the assertion check method of the given supertype, claszz.
protected  String	reflectiveCall(CClass clazz)           Return code that calls reflectively the assertion check method of the given supertype, claszz.

 

Methods inherited from class org.jmlspecs.jmlrac.AssertionMethod

checker, hasExplicitSuperClass

 

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

 

Constructor Detail

InvariantLikeMethod

public InvariantLikeMethod(boolean isStatic,
                           JmlTypeDeclaration typeDecl)

Construct a new InvariantLikeMethod object.

Parameters:

isStatic - the kind of assertion check method to generate; true for static and false for non-static (instance) assertion check method.

typeDecl - the target type declaration whose assertion check methods are to be generated.

generate

public JMethodDeclarationType generate(RacNode stmt)

Generate and return a type-level assertion check method such as invariants and history constraints. Append to the body (stmt): (1) code to check the inherited assertions if any, and (2) code to throw an appropriate exception to notify an assertion violation.

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.

buildHeader

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

Builds and returns the method header of the assertion check method as a string.

Overrides:

buildHeader in class AssertionMethod

Parameters:

returnType - return type

name - method name

parameters - formal parameters

exceptions - checked exceptions

formalParameters

protected String formalParameters()

Returns the formal parameters of the assertion check method.

inheritAssertion

protected String inheritAssertion(JFormalParameter[] parameters)

Return the code to inherit assertions of the superclass and interfaces, i.e., to call the assertion check method of the superclass and interfaces and appropriately accumulate the result to the assertion variable (e.g., conjunction).

Parameters:

parameters - parameters to the inherited assertion check method; not used in this specialization.

inheritFrom

protected String inheritFrom(CClass clazz)

Return the code that, if executed, inherits invariant-like assertions such as invariants and constraints from the given class, clazz. Because dynamic delegation is expensive, the inherting code is short-circuited in that it is executed only if the asssertion is not violated yet; i.e., not executed if the assertion is already violated in the inheriting class or in other classes whose assertions already inherited.

See Also:

reflectiveCall(CClass), nonReflectiveCall(CClass)

reflectiveCall

protected String reflectiveCall(CClass clazz)

Return code that calls reflectively the assertion check method of the given supertype, claszz.

See Also:

inheritFrom(CClass)

nonReflectiveCall

protected String nonReflectiveCall(CClass clazz)

Return code that calls non-reflectively the assertion check method of the given supertype, claszz.

See Also:

inheritFrom(CClass)

inheritCallArgTypes

protected String inheritCallArgTypes()

Returns, in the string form, the parameter types of the supertype's assertion check method. The returned value is used to look up the supertype's assertion check method using the Java's reflection facility.

See Also:

reflectiveCall(CClass)

inheritCallArgs

protected String inheritCallArgs()

Returns, in the string form, the arguments for calling supertype's constraint check method.

See Also:

reflectiveCall(CClass)

canInherit

protected boolean canInherit()

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

 also
   protected normal_behavior
     ensures \result == (!isStatic &&
      (hasExplicitSuperClass() || typeDecl.interfaces().length > 0));