JML

org.jmlspecs.jmlrac
Class LocalConstraintMethod

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.LocalConstraintMethod
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants

public class LocalConstraintMethod
extends ConstraintMethod

A class for generating constaint check methods that check locally specified type constraints without inheriting any constraints from supertypes. Two kinds of constraint check methods can be generated: instance constraint check methods 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.3 $
Author:
Yoonsik Cheon
See Also:
AssertionMethod, ConstraintMethod, generate(RacNode)

Field Summary
private  JmlMethodName[] names
          The names of methods to which the generated constraint check method is applicable; it is null if the constraint is applicable to all methods.
private  VarGenerator varGen
          The variable generator to be used in the translation.
 
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
LocalConstraintMethod(VarGenerator varGen, boolean isStatic, JmlTypeDeclaration typeDecl, JmlMethodName[] names, int suffix)
          Construct a new instance.
 
Method Summary
protected  boolean canInherit()
          Indicates whether the generated assertion method should try to dynamically inherit the corresponding assertion method of the superclass or interfaces.
 JMethodDeclarationType generate(RacNode stmt)
          Generates a constrain check method by using the given block of code, stmt, as the main body.
private  String isApplicable(JmlMethodName name, String var)
          Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.
private  RacNode isApplicable(JmlMethodName[] names)
          Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.
private  String nameMatched(JmlMethodName name, String var)
          Returns code that compares the given JML method name, name, with the method name given as a parameter (rac$name) to the constraint check method.
private  String paramMatched(JmlMethodName name, String var)
          Returns code that compares the foraml parameter types of the given JML method, name, with those of the constraint check method.
static String postfix(boolean isStatic, JmlTypeDeclaration typeDecl, int suffix)
          Returns the postfix to be used for constraint check method's name.
private  String simpleName(JmlName[] subnames)
          Returns a simplied method name of the given JML names, that can be compared with the method name given as a parameter of the constraint check method.
 
Methods inherited from class org.jmlspecs.jmlrac.ConstraintMethod
formalParameters, inheritCallArgs, inheritCallArgTypes
 
Methods inherited from class org.jmlspecs.jmlrac.InvariantLikeMethod
buildHeader, inheritAssertion, inheritFrom, nonReflectiveCall, reflectiveCall
 
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
 

Field Detail

varGen

private final VarGenerator varGen
The variable generator to be used in the translation. If necessary, fresh variables are generated by this translator using this variable generator.


names

private JmlMethodName[] names
The names of methods to which the generated constraint check method is applicable; it is null if the constraint is applicable to all methods.

Constructor Detail

LocalConstraintMethod

public LocalConstraintMethod(VarGenerator varGen,
                             boolean isStatic,
                             JmlTypeDeclaration typeDecl,
                             JmlMethodName[] names,
                             int suffix)
Construct a new instance.

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.
names - method names that the generated constraint check method is applicable to.
suffix - a unique sequence number to be used as the suffix of the constraint check method's name.
Method Detail

postfix

public static String postfix(boolean isStatic,
                             JmlTypeDeclaration typeDecl,
                             int suffix)
Returns the postfix to be used for constraint check method's name.


generate

public JMethodDeclarationType generate(RacNode stmt)
Generates a constrain check method by using the given block of code, stmt, as the main body. This method prefixes the body with the code that tests if the constraint is applicable to the argument method and appends the code to throw a constraint violation error. Thus, the returned method has the following structure.
 public void checkHC$instance1$Constraint1(String rac$msg,
   String rac$name, java.lang.Class[] rac$params) {
   boolean b = false;
   b = ...; // test if applicable to method  
   if (!b) {
     return;
   }
   stmt
   if (!constraint_hold) {
     throw new JMLHistoryConstraintError(...);
   }
 }
 

Overrides:
generate in class InvariantLikeMethod
Parameters:
stmt - code to evaluate the constraint; 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.

isApplicable

private RacNode isApplicable(JmlMethodName[] names)
Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method.


isApplicable

private String isApplicable(JmlMethodName name,
                            String var)
Returns code that tests if the given JML method name, name, is applicable to the method name given as a parameter (rac$name and rac$params) to the constraint check method. The code sets the given boolean variable, var to the result.


nameMatched

private String nameMatched(JmlMethodName name,
                           String var)
Returns code that compares the given JML method name, name, with the method name given as a parameter (rac$name) to the constraint check method. The code sets the given boolean variable, var to the result of the comparison.


paramMatched

private String paramMatched(JmlMethodName name,
                            String var)
Returns code that compares the foraml parameter types of the given JML method, name, with those of the constraint check method. The code sets the given boolean variable, var to the result of the comparison.


simpleName

private String simpleName(JmlName[] subnames)
Returns a simplied method name of the given JML names, that can be compared with the method name given as a parameter of the constraint check method. E.g., n for n or this.n, and null for all other cases.


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 == false;
 

Overrides:
canInherit in class InvariantLikeMethod

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.