JML

org.jmlspecs.jmlrac
Class MotherConstraintMethod

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.AssertionMethod
              extended byorg.jmlspecs.jmlrac.InvariantLikeMethod
                  extended byorg.jmlspecs.jmlrac.ConstraintMethod
                      extended byorg.jmlspecs.jmlrac.MotherConstraintMethod
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
SubtypeConstraintMethod

public class MotherConstraintMethod
extends ConstraintMethod

A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes. The generated constraint methods are supposed to be called by wrapper methods and constructors. This class can generate both instance and static constraint check methods. For details on constraint check methods, refer to the class ConstraintMethod.

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

Version:
$Revision: 1.5 $
Author:
Yoonsik Cheon
See Also:
AssertionMethod

Field Summary
private  List restoreMethods
          The names of the restoration methods that can restore the correct values for old expressions appearing in the constraint clause in the presence of recursive method calls.
 
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
protected MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, String postfix, List restoreMethods)
          Construct a new instance.
  MotherConstraintMethod(boolean isStatic, JmlTypeDeclaration typeDecl, List restoreMethods)
          Construct a new instance.
 
Method Summary
protected  StringBuffer buildHeader(String returnType, String name, JFormalParameter[] parameters, CClassType[] exceptions)
          Builds, in a string form, the header of constraint method.
protected  String checker(boolean initValue, RacNode stmt, JFormalParameter[] params)
          Returns the given constraint check code, stmt, wrapped with code to inherit supertypes's constraints.
 JMethodDeclarationType generate(RacNode stmt)
          Returns a constraint check method with the given body, stmt.
protected  String inheritAssertion(JFormalParameter[] parameters)
          Return the code to inherit constraints of the superclass and interfaces, i.e., to call the constraint methods of the superclass and interfaces.
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 formal parameter types of the supertype's constraint check method.
protected  String inheritFrom(boolean isWeaksubtype, CClass clazz)
          Returns code that, if executed, inherits constraints from the given type, clazz.
protected  String nonReflectiveCall(boolean isWeakly, CClass clazz)
          Return code, in the string form, that calls non-reflectively the constraint check method of the given supertype, claszz.
private static String postfix(boolean isStatic, JmlTypeDeclaration typeDecl)
          Returns the postfix to be used for constraint check method's name.
protected  String reflectiveCall(boolean isWeakly, CClass clazz)
          Return code, in the string form, that calls reflectively the constraint check method of the given supertype, claszz.
 
Methods inherited from class org.jmlspecs.jmlrac.ConstraintMethod
formalParameters
 
Methods inherited from class org.jmlspecs.jmlrac.InvariantLikeMethod
canInherit, inheritFrom, nonReflectiveCall, reflectiveCall
 
Methods inherited from class org.jmlspecs.jmlrac.AssertionMethod
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
 

Field Detail

restoreMethods

private List restoreMethods
The names of the restoration methods that can restore the correct values for old expressions appearing in the constraint clause in the presence of recursive method calls. Each entry of this list is a string.

 private invariant (\forall Object o; restoreMethods.contains(o);
   o instanceof String);
 

Constructor Detail

MotherConstraintMethod

public MotherConstraintMethod(boolean isStatic,
                              JmlTypeDeclaration typeDecl,
                              List restoreMethods)
Construct a new instance.

  requires (\forall Object o; restoreMethods.contains(o);
    o instanceof String);
 

Parameters:
isStatic - the kind of constraint method to generate; true for static and false for non-static (instance) constraint method.
typeDecl - the target type declaration whose constraint methods are to be generated.
restoreMethods - the names of resore methods to be used to restore the values of old expression fields.

MotherConstraintMethod

protected MotherConstraintMethod(boolean isStatic,
                                 JmlTypeDeclaration typeDecl,
                                 String postfix,
                                 List restoreMethods)
Construct a new instance.

  requires typeDecl != null;
  requires (\forall Object o; restoreMethods.contains(o);
    o instanceof String);
 

Parameters:
isStatic - the kind of constraint method to generate; true for static and false for non-static (instance) constraint method.
typeDecl - the target type declaration whose constraint methods are to be generated.
restoreMethods - the names of resore methods to be used to restore the values of old expression fields.
Method Detail

postfix

private static String postfix(boolean isStatic,
                              JmlTypeDeclaration typeDecl)
Returns the postfix to be used for constraint check method's name. The return value is of the form: [static|instance$T].


generate

public JMethodDeclarationType generate(RacNode stmt)
Returns a constraint check method with the given body, stmt. Appended to the body (stmt) are (1) code to check the inherited assertions if any, and (2) code to throw an appropriate exception to notify an assertion violation.

Overrides:
generate in class InvariantLikeMethod
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, in a string form, the header of constraint method. The header of a constraint method has the following form.
  public [static] void name(String rac$msg, String rac$name,
    String rac$params)
 

Overrides:
buildHeader in class InvariantLikeMethod
Parameters:
returnType - return type
name - method name
parameters - formal parameters
exceptions - checked exceptions

checker

protected String checker(boolean initValue,
                         RacNode stmt,
                         JFormalParameter[] params)
Returns the given constraint check code, stmt, wrapped with code to inherit supertypes's constraints. For each supertype, its strong or weak form of constraint check method is called to inherit its constraints.

Overrides:
checker in class AssertionMethod
Parameters:
initValue - not used
stmt - constraint check code to be wrapped
params - not used

inheritAssertion

protected String inheritAssertion(JFormalParameter[] parameters)
Return the code to inherit constraints of the superclass and interfaces, i.e., to call the constraint methods of the superclass and interfaces.

Overrides:
inheritAssertion in class InvariantLikeMethod
Parameters:
parameters - parameters to the inherited assertion check method; not used in this specialization.

inheritFrom

protected String inheritFrom(boolean isWeaksubtype,
                             CClass clazz)
Returns code that, if executed, inherits constraints from the given type, clazz.

See Also:
#reflectiveCall(CClass), #nonReflectiveCall(CClass)

reflectiveCall

protected String reflectiveCall(boolean isWeakly,
                                CClass clazz)
Return code, in the string form, that calls reflectively the constraint check method of the given supertype, claszz. If the argument, isWeakly is true, the code calls the supertype's constraint method that checks constraints according to the weak subtyping; otherwise, called is the one that checks constraints according to the strong form of subtyping.

See Also:
inheritFrom(boolean, CClass)

nonReflectiveCall

protected String nonReflectiveCall(boolean isWeakly,
                                   CClass clazz)
Return code, in the string form, that calls non-reflectively the constraint check method of the given supertype, claszz. If the argument, isWeakly is true, the code calls the supertype's constraint method that checks constraints according to the weak subtyping; otherwise, called is the one that checks constraints according to the strong form of subtyping.

See Also:
inheritFrom(boolean, CClass)

inheritCallArgTypes

protected String inheritCallArgTypes()
Returns, in the string form, the formal parameter types of the supertype's constraint check method. The returned value is used to look up the supertype's constraint check method using the Java's reflection facility.

Overrides:
inheritCallArgTypes in class ConstraintMethod
See Also:
reflectiveCall(boolean, CClass), nonReflectiveCall(boolean, CClass)

inheritCallArgs

protected String inheritCallArgs()
Returns, in the string form, the arguments for calling supertype's constraint check method.

Overrides:
inheritCallArgs in class ConstraintMethod
See Also:
reflectiveCall(boolean, CClass), nonReflectiveCall(boolean, CClass)

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.