JML

org.jmlspecs.jmlrac
Class PreconditionMethod

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.AssertionMethod
              extended byorg.jmlspecs.jmlrac.PreOrPostconditionMethod
                  extended byorg.jmlspecs.jmlrac.PreconditionMethod
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants

public class PreconditionMethod
extends PreOrPostconditionMethod

A class for generating precondition check methods. The precondition check code is wrapped with code to check the inherited preconditions if any, and to throw an appropriate exception to signal a violation if the precondition is violated.

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

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

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.jmlrac.PreOrPostconditionMethod
 
Field Summary
private  boolean hasAssertion
           
 
Fields inherited from class org.jmlspecs.jmlrac.PreOrPostconditionMethod
methodDecl, modifiers, name, parameters, stackMethod
 
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
PreconditionMethod(JmlTypeDeclaration typeDecl, JmlMethodDeclaration mdecl, boolean hasAssertion, String saveMethod)
          Construct a new PreconditionMethod object.
 
Method Summary
protected  String checker(boolean start, RacNode stmt, JFormalParameter[] params)
          Returns the precondition check code (stmt) wrapped with code to inherit superclass's preconditions if any, and to signal an assertion violation if it happens at runtime.
 JMethodDeclarationType generate(RacNode stmt)
           
 JMethodDeclarationType generate(RacNode stmt, List preExprs)
          Generates and returns a precondition checking method.
protected  String inheritAssertion(JFormalParameter[] parameters)
          Return the code to check inherited preconditions (from both the superclass and interfaces), i.e., to call the proper precondition check methods and appropriately disjoin the result to the assertion variable.
private  String preValueSaveCode()
          Returns code for saving pre-values to internal stacks to be fetched by the post-state assertion check method such as the postcondition method in the post-state.
private  String preValueSaveCode2()
          Returns code for saving pre-values to internal stacks to be fetched by the post-state assertion check method such as the postcondition method in the post-state.
 
Methods inherited from class org.jmlspecs.jmlrac.PreOrPostconditionMethod
canInherit, methodName, nonReflectiveCall, reflectiveCall
 
Methods inherited from class org.jmlspecs.jmlrac.AssertionMethod
buildHeader, 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

hasAssertion

private boolean hasAssertion
Constructor Detail

PreconditionMethod

public PreconditionMethod(JmlTypeDeclaration typeDecl,
                          JmlMethodDeclaration mdecl,
                          boolean hasAssertion,
                          String saveMethod)
Construct a new PreconditionMethod object.

Parameters:
mdecl - method for which the precondition method is generated
hasAssertion - true if mdecl has a precondition specification
Method Detail

generate

public JMethodDeclarationType generate(RacNode stmt)
Description copied from class: AssertionMethod
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.


generate

public JMethodDeclarationType generate(RacNode stmt,
                                       List preExprs)
Generates and returns a precondition checking method. Append to the body (stmt) (1) code to check the inherited precondition if any, and (2) code to throw an appropriate exception to notify a violation if the precondition is violated.

Parameters:
stmt - code to evaluate the precondition; the result is supposed to be stored in the variable VN_ASSERTION. A null value means that no precondition is specified or the precondition is not executable.
preExprs - a list of RacNodes denoting expressions to be executed in the pre-sate, e.g., specification variables \old expressions.

checker

protected String checker(boolean start,
                         RacNode stmt,
                         JFormalParameter[] params)
Returns the precondition check code (stmt) wrapped with code to inherit superclass's preconditions if any, and to signal an assertion violation if it happens at runtime. The precondition check code (stmt), if non-null, evaluates all preconditions specified in the class, disconjoin 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 precondition check code.

Overrides:
checker in class AssertionMethod
Parameters:
start - initial value of the assertion variable.
stmt - precondition check code to wrap
params - parameters to call the inherited check method if necessary.

preValueSaveCode

private String preValueSaveCode()
Returns code for saving pre-values to internal stacks to be fetched by the post-state assertion check method such as the postcondition method in the post-state.

   requires stackMethod == null;
   ensures \result.equals("");
 also
   requires stackMethod != null;
   ensures (* \result is stack save code *);
 


preValueSaveCode2

private String preValueSaveCode2()
Returns code for saving pre-values to internal stacks to be fetched by the post-state assertion check method such as the postcondition method in the post-state. The returned code has the same structure of that of the method preValueSaveCode, but indented to the two tab position.

See Also:
preValueSaveCode()

inheritAssertion

protected String inheritAssertion(JFormalParameter[] parameters)
Return the code to check inherited preconditions (from both the superclass and interfaces), i.e., to call the proper precondition check methods and appropriately disjoin the result to the assertion variable.

Parameters:
parameters - parameters to the precondition check methods

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.