JML

org.jmlspecs.jmlrac
Class WrapperMethod

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.WrapperMethod
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
ConstructorWrapper, FinalizerWrapper

public class WrapperMethod
extends TransUtils

A class for generating wrapper methods. A wrapper method is a method that wraps a method with assertion check methods such as pre and postcondition check methods. The original method is renamed and called by the wrapper method inside the wrap. Wrapper methods are generated for only concrete methods; no wrapper methods are generated for abstract methods.

Version:
$Revision: 1.31 $
Author:
Yoonsik Cheon

Field Summary
protected  StringBuffer args
          arguments to pre/orig, post, or xpost method calls
private  boolean hasReturn
          true if the target method has return type.
protected  String ident
          name of the target method.
protected  boolean isHelper
          true if the target method is a helper.
protected  boolean isStatic
          true if the target method is a static method.
protected  JmlMethodDeclaration methodDecl
          target method to be wrapped.
protected  StringBuffer postArgs
          arguments to pre/orig, post, or xpost method calls
protected  CType returnType
          return type of the target method.
protected  String typeName
          type name whose methods are to be wrapped.
protected  StringBuffer xpostArgs
          arguments to pre/orig, post, or xpost method calls
 
Fields inherited from class org.jmlspecs.jmlrac.TransUtils
typeDecl
 
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
WrapperMethod(String typeName, JmlMethodDeclaration mdecl)
          Construct a new instance.
 
Method Summary
protected  void buildArguments()
          Builds arguments to various assertion check methods such as pre- and postcondition check methods.
protected  JBlock buildWrapperBody()
          Returns code for the body of the wrapper method being created.
protected  String callOriginalMethod()
          Returns code for invoking the original method.
protected  String checkConstraint()
          Returns code for checking history constraint.
protected  String checkPostcondition()
          Returns code for checking normal postcondition.
protected  String checkPostInvariant()
          Returns code for checking invariant in the post-state.
protected  String checkPrecondition()
          Returns code for checking precondition.
protected  String checkPreInvariant()
          Returns code for checking invariant in the pre-state.
protected  String checkXPostcondition()
          Returns code for checking exceptional postcondition.
protected  String constraintCallArg()
          Returns, in the string form, the argument for calling a constraint check method.
protected  String evalOldInConstraint()
          Returns code for evaluating old expressions in constraints.
 JMethodDeclarationType generate()
          Returns a wrapper method.
protected  String identification(String state)
          Returns a string that identifies the method being translated.
protected  String isActive(String type)
          Returns a string representation of the condition that tests if the given type of assertion is active.
protected  String mandatoryReturn()
          Returns a mandatory return statement.
protected  String nocheckDuringInit()
          Returns code for bypassing assertion checks during the class and instance initialization.
protected  String optionalReturn()
          Returns an optional return statement.
protected  String racMethodName(String type)
          Returns the name of runtime assertion checker method for the given type.
protected  String resultVarDecl()
          Returns code for declaring result variable.
protected  String wrap(String type, String comment, String stmt)
          Returns the given statement, stmt, wrapped in assertion check demarcation.
protected  String wrap2(String type, String comment, String stmt)
          Returns the given statement, stmt, wrapped in assertion check demarcation.
protected  String wrap3(String type, String comment, String stmt)
          Returns the given statement, stmt, wrapped in assertion check demarcation.
 
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

typeName

protected final String typeName
type name whose methods are to be wrapped. This field is used to generate the names of various assertion check methods.


methodDecl

protected final JmlMethodDeclaration methodDecl
target method to be wrapped.

 protected invariant methodDecl != null;
 


isHelper

protected final boolean isHelper
true if the target method is a helper.

 protected invariant isHelper == methodDecl.isHelper();
 


isStatic

protected final boolean isStatic
true if the target method is a static method.

 protected invariant isStatic == methodDecl.isStatic();
 


hasReturn

private final boolean hasReturn
true if the target method has return type.

 private invariant hasReturn == 
   (returnType != null && !returnType.isVoid());
 


returnType

protected final CType returnType
return type of the target method.

 private invariant returnType == methodDecl.returnType();
 


ident

protected final String ident
name of the target method.

 private invariant ident == methodDecl.ident();
 


args

protected StringBuffer args
arguments to pre/orig, post, or xpost method calls


postArgs

protected StringBuffer postArgs
arguments to pre/orig, post, or xpost method calls


xpostArgs

protected StringBuffer xpostArgs
arguments to pre/orig, post, or xpost method calls

Constructor Detail

WrapperMethod

public WrapperMethod(String typeName,
                     JmlMethodDeclaration mdecl)
Construct a new instance.

 requires typeName != null && mdecl != null && mdecl.body() != null;
 

Parameters:
mdecl - method to be wrapped; must not be abstract.
Method Detail

generate

public JMethodDeclarationType generate()
Returns a wrapper method. The original method is renamed and called by the wrapper method enclosed in assertion check code such as pre and postcondition check methods. The body of the wrapper method has the following general structure:
 T m(T1 x1, ..., Tn xn) {
   checkPre$m(x1, ..., xn);
   checkInv();
   T r = init_T;
   boolean ok = true;
   try {
     r = orig$m(x1, ..., xn);
     checkPost$m(x1, ..., xn, r);
   }
   catch (JMLEntryPreconditionError e) {
     ok = false;
     throw new JMLInternalPreconditionError(e);
   }
   catch (JMLExitPostconditionError e) {
     ok = false;
     throw new JMLInternalPostconditionError(e);
   }
   catch (JMLAssertionError e) {
     ok = false;
     throw e;
   }
   catch (Throwable e) {
     try {
       checkXPost$m(x1, ..., xn, r, e);
     } 
     catch (JMLAssertionError e1) {
       ok = false;
       throw e1;
     }
   }
   finally {
     if (ok) {
        checkInv();
        checkConstraint();
     }
   }
 }
 

 old String n = methodDecl.ident();
 modifies methodDecl.*;
 assignable args, postArgs, xpostArgs;
 ensures methodDecl.ident().equals(MN_INTERNAL + n) &&
         \fresh(\result);
 


buildWrapperBody

protected JBlock buildWrapperBody()
Returns code for the body of the wrapper method being created. For the structure of the returned code refers to the method generate().

 ensures \result != null;
 

See Also:
generate()

nocheckDuringInit

protected String nocheckDuringInit()
Returns code for bypassing assertion checks during the class and instance initialization. Assertions are also not checked while the object is being constructed. The returned code has the following structure.
  if (!VN_CLASS_INIT [|| !VN_INIT] [|| !VN_CONSTRUCTED()]) {
     [return] m(x1, ..., xn);
     [return;]
  }
 


checkPreInvariant

protected String checkPreInvariant()
Returns code for checking invariant in the pre-state. If the method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.
  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated. The code for checking instance invariant is generated only if the target method is an instance method.

   requires isHelper;
   ensures \fresh(\result) && "".equals(\result);
 also
   requires !isHelper;
   ensures \fresh(\result) && \result.length() > 0 &&
     (* \result is of the above form of code *);
 


checkPostInvariant

protected String checkPostInvariant()
Returns code for checking invariant in the post-state. If the target method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.
  // check static invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$static();
    JMLChecker.exit();
  }
  // check instance invariant
  if (JMLChecker.isActive(JMLChecker.INVARIANT)) {
    JMLChecker.enter();
    checkInv$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated. The code for checking instance invariant is generated only if the target method is an instance method.

   requires isHelper;
   ensures \fresh(\result) && "".equals(\result);
 also
   requires !isHelper;
   ensures \fresh(\result) && \result.length() > 0 &&
     (* \result is of the above form of code *);
 


evalOldInConstraint

protected String evalOldInConstraint()
Returns code for evaluating old expressions in constraints. A helper need not establish the constraints. Thus, an empty string is returned for a helper and the following form of code for a non-helper.
  // eval old exprs in static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$satic(); 
    JMLChecker.exit();
  }
  // eval old exprs in non-static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    evalOldExprInHC$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated. The code for instance constraints is generated only if the target method is an instance method.


checkConstraint

protected String checkConstraint()
Returns code for checking history constraint. The constraint is not checked for constructors. If the target method being translated is a helper method, an empty string is returned; otherwise, the following form of code is returned.
  // check static constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$static();
    JMLChecker.exit();
  }
  // check instance constraint
  if (JMLChecker.isActive(JMLChecker.CONSTRAINT)) {
    JMLChecker.enter();
    checkHC$instance$T();
    JMLChecker.exit();
  }
 
where T is the name of type being translated. The code for checking instance constraint is generated only if the target method is an instance method.


constraintCallArg

protected String constraintCallArg()
Returns, in the string form, the argument for calling a constraint check method.


buildArguments

protected void buildArguments()
Builds arguments to various assertion check methods such as pre- and postcondition check methods. If the target method has arguments x1, x2, ..., xn, and throws some exceptions, this method sets the field args to "(x1,...,xn)", postArgs to "(x1,...,xn,VN_RESULT)", and xpostArgs to "(x1,...,xn,VN_XRESULT)".

 assignable args, postArgs, xpostArgs;
 ensures args != null && postArgs != null && xpostArgs != null;
 


callOriginalMethod

protected String callOriginalMethod()
Returns code for invoking the original method. I.e., [ VN_RESULT = ] internal$m(x1,...,xn);.


resultVarDecl

protected String resultVarDecl()
Returns code for declaring result variable. I.e., T VN_RESULT = init_value_of_T;, where T is the return type.


checkPrecondition

protected String checkPrecondition()
Returns code for checking precondition. The returned code has the following structure.
  // check precondition
  if (JMLChecker.isActive(JMLChecker.PRECONDITION)) {
    JMLChecker.enter();
    checkPre$m$T(x1,...,xn);
    JMLChecker.exit();
  }
 
where m is the name of method being translated and T is the name of the owning type.


checkPostcondition

protected String checkPostcondition()
Returns code for checking normal postcondition. The returned code has the following structure.
  // check normal postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)) {
    JMLChecker.enter();
    checkPost$m$T(x1,...,xn,r);
    JMLChecker.exit();
  }
 
where m is the name of method being translated and T is the name of the owning type.


checkXPostcondition

protected String checkXPostcondition()
Returns code for checking exceptional postcondition. The returned code has the following structure.
  // check exceptional postcondition
  if (JMLChecker.isActive(JMLChecker.POSTCONDITION)) {
    JMLChecker.enter();
    checkXPost$m$T(x1,...,xn,r,e);
    JMLChecker.exit();
  }
 
where m is the name of method being translated and T is the name of the owning type.


mandatoryReturn

protected String mandatoryReturn()
Returns a mandatory return statement. I.e, return [ VN_RESULT ];. The optional result variable is generated only if the method being translated has a non-void return type.


optionalReturn

protected String optionalReturn()
Returns an optional return statement. I.e, [ return VN_RESULT ; ]. If the method being translated has a void return type, the result is an empty string.


wrap

protected String wrap(String type,
                      String comment,
                      String stmt)
Returns the given statement, stmt, wrapped in assertion check demarcation. The returned code has the following structure.
  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 

Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

wrap2

protected String wrap2(String type,
                       String comment,
                       String stmt)
Returns the given statement, stmt, wrapped in assertion check demarcation. The whole code is indented two tabs. The returned code has the following structure.
  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 

Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

wrap3

protected String wrap3(String type,
                       String comment,
                       String stmt)
Returns the given statement, stmt, wrapped in assertion check demarcation. The whole code is indented three tabs. The returned code has the following structure.
  // comment
  if (JMLChecker.isActive(JMLChecker.type)) {
    JMLChecker.enter();
    stmt;
    JMLChecker.exit();
  }
 

Parameters:
type - assertion type, e.g., PRECONDITION, etc.
comment - header comment
stmt - statement to be wrapped

isActive

protected String isActive(String type)
Returns a string representation of the condition that tests if the given type of assertion is active.

 ensures \result.equals("JMLChecker.isActive(JMLChecker." + type +")"); 
 


identification

protected String identification(String state)
Returns a string that identifies the method being translated.


racMethodName

protected String racMethodName(String type)
Returns the name of runtime assertion checker method for the given type.

 requires (* type is MN_CHECK_PRE, MN_CHECK_POST, MN_CHECK_XPOST, etc.*);
 ensures \result.equals(type + ident + "$" + typeName);
 


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.