JML

org.jmlspecs.jmlrac.qexpr
Class StaticAnalysis

java.lang.Object
  extended byorg.jmlspecs.jmlrac.qexpr.Translator
      extended byorg.jmlspecs.jmlrac.qexpr.StaticAnalysis
All Implemented Interfaces:
Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
StaticAnalysis.EnumerationBased, StaticAnalysis.IntervalBased, StaticAnalysis.SetBased

abstract class StaticAnalysis
extends Translator

An abstract class for translating JML quantified expressions into Java source code. The translation is based on the static analysis of the expression's structures.


Nested Class Summary
private static class StaticAnalysis.EnumerationBased
          A concrete class for translating JML quantified expressions into Java source code.
private static class StaticAnalysis.IntervalBased
          A concrete class for translating JML quantified expressions into Java source code.
private static class StaticAnalysis.SetBased
          A concrete class for translating JML quantified expressions into Java source code.
 
Field Summary
protected  RacContext context
          current translation context
protected static TokenReference NO_REF
           
protected  JmlSpecQuantifiedExpression quantiExp
          taget quantified expression to translate
protected  String resultVar
          variable name to have the value of quantified expression in the translated code
protected  AbstractExpressionTranslator transExp
           
protected  VarGenerator varGen
          variable generator for generating unique local variables
 
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 StaticAnalysis(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
          Constructs a StaticAnalysis object.
 
Method Summary
private  String applySumOrProduct(String strResultVar, String strOptr, String strV2, CType vType)
           
 RacNode generateLoop(RacNode body)
          Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected abstract  RacNode generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result)
          Returns a loop code evaluating the body of the quantified predicate.
static StaticAnalysis getInstance(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
          Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.
private  JExpression rangePredicate()
          Returns the range predicate of the quantified expression.
protected  RacNode transExpression(JExpression expr, String var)
          Returns code for evaluating expression expr and storing the result to the variable var.
private  RacNode transForAllOrExists()
          Returns Java source code for evaluating the JML quantified expression, which is either a universal or existential quantifier.
 RacNode translate()
          Translate a JML quantified expression into Java source code and return the result.
private  RacNode translateExists()
          Return Java source code for evaluating a JML quantified expression of an existential quantifier.
private  RacNode translateForAll()
          Return Java source code for evaluating a JML quantified expression of a univeral quantifier.
private  RacNode translateMax()
          Return Java source code for evaluating a JML quantified expression of a generalized quantifier \max.
private  RacNode translateMin()
          Return Java source code for evaluating a JML quantified expression of a generalized quantifier \min.
private  RacNode translateNumOf()
          Returns code for evaluating numerical quantifiers\num_of.
private  RacNode translateProduct()
          Return Java source code for evaluating a JML quantified expression of a generalized quantifier \product.
private  RacNode translateSum()
          Return Java source code for evaluating a JML quantified expression of a generalized quantifier \sum.
private  RacNode transMinOrMax()
          Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \min or \max.
private  RacNode transSumOrProduct()
          Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \sum or \product.
private static JExpression unwrapJmlExpression(JExpression expr)
          Unwraps a given JML expression if it is an instance of JmlPredicate or JmlSpecExpression.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

NO_REF

protected static final TokenReference NO_REF

varGen

protected VarGenerator varGen
variable generator for generating unique local variables


context

protected RacContext context
current translation context


quantiExp

protected JmlSpecQuantifiedExpression quantiExp
taget quantified expression to translate


resultVar

protected String resultVar
variable name to have the value of quantified expression in the translated code


transExp

protected AbstractExpressionTranslator transExp
Constructor Detail

StaticAnalysis

protected StaticAnalysis(VarGenerator varGen,
                         RacContext ctx,
                         JmlSpecQuantifiedExpression expr,
                         String resultVar,
                         AbstractExpressionTranslator transExp)
Constructs a StaticAnalysis object.

Parameters:
varGen - variable generator to be used in translation for generating unique local variables.
expr - quantified expression to be translated.
resultVar - variable name to have the value of quantified expression in the translated code.
transExp - translator to use for translating subexpressions of the quantified expression.
Method Detail

getInstance

public static StaticAnalysis getInstance(VarGenerator varGen,
                                         RacContext ctx,
                                         JmlSpecQuantifiedExpression expr,
                                         String resultVar,
                                         AbstractExpressionTranslator transExp)
Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.

Parameters:
varGen - variable generator to be used in translation for generating unique local variables.
expr - quantified expression to be translated.
resultVar - variable name to store the result value of quantified expression in the translated code.
transExp - translator to use for translating subexpressions.

translate

public RacNode translate()
                  throws NonExecutableQuantifierException
Translate a JML quantified expression into Java source code and return the result.

Returns:
translated Java source code.
Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateForAll

private RacNode translateForAll()
                         throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of a univeral quantifier. The returned code has the following general form:
   [[(\forall T x1, ..., xn; P; Q), r]] =
     r = true;
     Collection c1 = null;
     [[S, c1]]  // S is the qset of P ==> Q
     Iterator iter1 = c1.iterator();
     while (r && iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[S, cn]]
        Iterator itern = cn.iterator();
        while (r && itern.hasNext()) {
            T xn = itern.next();
            [[P ==> Q, r]]
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\forall T x1, ..., xn; P; Q), r]] =
     r = true;
     T l1 = 0;
     T u1 = 0;
     [[l1 and u1 calculation from P]]
     while (r && l < u) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[ln and un calculation from P]]
        while (r && ln < un) {
            T xn = ln;
            [[P ==> Q, r]]
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateExists

private RacNode translateExists()
                         throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of an existential quantifier. The returned code has the following general form:
   [[(\exists T x1, ..., xn; P; Q), r]] =
     r = false;
     Collection c1 = null;
     [[S, c1]]  // S is the qset of P ==> Q
     Iterator iter1 = c1.iterator();
     while (!r && iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[S, cn]]
        Iterator itern = cn.iterator();
        while (!r && itern.hasNext()) {
            T xn = itern.next();
            [[P && Q, r]]
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\exists T x1, ..., xn; P; Q), r]] =
     r = false;
     T l1 = 0;
     T u1 = 0;
     [[l1 and u1 calculation from P]]
     while (!r && l < u) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[ln and un calculation from P]]
        while (!r && ln < un) {
            T xn = ln;
            [[P && Q, r]]
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateSum

private RacNode translateSum()
                      throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \sum. The returned code has the following general form:
   [[(\sum T x1, ..., xn; P; Q), r]] =
     r = 0;
     Collection c1 = null;
     [[S1, c1]]  // S1 is the qset of P for x1
     Iterator iter1 = c1.iterator();
     while (iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[Sn, cn]] // Sn is the qset of P for xn
        Iterator itern = cn.iterator();
        while (itern.hasNext()) {
            T xn = itern.next();
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = resultVar + v2;
            }
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\sum T x1, ..., xn; P; Q), r]] =
     r = 0;
     T l1 = 0;
     T u1 = 0;
     [[calculation of l1 and u1 from P]]
     while (l1 < u1) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[calculation of ln and un from P]]
        while (ln < un) {
            T xn = ln;
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = resultVar + v2;
            }
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateProduct

private RacNode translateProduct()
                          throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \product. The returned code has the following general form:
   [[(\product T x1, ..., xn; P; Q), r]] =
     r = 1;
     Collection c1 = null;
     [[S1, c1]]  // S1 is the qset of P for x1
     Iterator iter1 = c1.iterator();
     while (iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[Sn, cn]] // Sn is the qset of P for xn
        Iterator itern = cn.iterator();
        while (itern.hasNext()) {
            T xn = itern.next();
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = resultVar * v2;
            }
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\product T x1, ..., xn; P; Q), r]] =
     r = 0;
     T l1 = 0;
     T u1 = 0;
     [[calculation of l1 and u1 from P]]
     while (l1 < u1) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[calculation of ln and un from P]]
        while (ln < un) {
            T xn = ln;
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = resultVar * v2;
            }
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateMin

private RacNode translateMin()
                      throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \min. The returned code has the following general form:
   [[(\min T x1, ..., xn; P; Q), r]] =
     r = Integer.MAX_VALUE;
     Collection c1 = null;
     [[S1, c1]]  // S1 is the qset of P for x1
     Iterator iter1 = c1.iterator();
     while (iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[Sn, cn]] // Sn is the qset of P for xn
        Iterator itern = cn.iterator();
        while (itern.hasNext()) {
            T xn = itern.next();
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = Math.min(resultVar, v2);
            }
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\max T x1, ..., xn; P; Q), r]] =
     r = Integer.MAX_VALUE;
     T l1 = 0;
     T u1 = 0;
     [[calculation of l1 and u1 from P]]
     while (l1 < u1) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[calculation of ln and un from P]]
        while (ln < un) {
            T xn = ln;
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = Math.min(resultVar, v2);
            }
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateMax

private RacNode translateMax()
                      throws NonExecutableQuantifierException
Return Java source code for evaluating a JML quantified expression of a generalized quantifier \max. The returned code has the following general form:
   [[(\max T x1, ..., xn; P; Q), r]] =
     r = Integer.MIN_VALUE;
     Collection c1 = null;
     [[S1, c1]]  // S1 is the qset of P for x1
     Iterator iter1 = c1.iterator();
     while (iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[Sn, cn]] // Sn is the qset of P for xn
        Iterator itern = cn.iterator();
        while (itern.hasNext()) {
            T xn = itern.next();
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = Math.max(resultVar, v2);
            }
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\max T x1, ..., xn; P; Q), r]] =
     r = Integer.MIN_VALUE;
     T l1 = 0;
     T u1 = 0;
     [[calculation of l1 and u1 from P]]
     while (l1 < u1) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[calculation of ln and un from P]]
        while (ln < un) {
            T xn = ln;
            boolean v1 = false;
            [[P, v1]]
            if (v1) {
               T_Q v2 = T_init;
               [[Q, v2]]
               resultVar = Math.max(resultVar, v2);
            }
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

translateNumOf

private RacNode translateNumOf()
                        throws NonExecutableQuantifierException
Returns code for evaluating numerical quantifiers\num_of. The returned code has the following general form:
   [[(\num_of T x1, ..., xn; P; Q), r]] =
     r = 0;
     Collection c1 = null;
     [[S1, c1]]  // S1 is the qset of P for x1
     Iterator iter1 = c1.iterator();
     while (iter1.hasNext()) {
        T x1 = iter1.next();
        ...
        Collection cn = null;
        [[Sn, cn]] // Sn is the qset of P for xn
        Iterator itern = cn.iterator();
        while (itern.hasNext()) {
            T xn = itern.next();
            boolean v1 = false;
            [[P, v1]]
            boolean v2 = false;
            [[Q, v2]]
            if (v1 && v2) {
               resultVar++;
            }
        }
        ...
     }
 
If the type (T) of the quantified variables is byte, char, short, int, or long. The following rule is applied:
   [[(\num_of T x1, ..., xn; P; Q), r]] =
     r = 0;
     T l1 = 0;
     T u1 = 0;
     [[calculation of l1 and u1 from P]]
     while (l1 < u1) {
        T x1 = l1;
        ...
        T ln = 0;
        T un = 0;
        [[calculation of ln and un from P]]
        while (ln < un) {
            T xn = ln;
            boolean v1 = false;
            [[P, v1]]
            boolean v2 = false;
            [[Q, v2]]
            if (v1 && v2) {
               resultVar++;
            }
            ln = ln + 1;
        }
        ...
        l1 = l1 + 1;
     }
 

Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

transForAllOrExists

private RacNode transForAllOrExists()
                             throws NonExecutableQuantifierException
Returns Java source code for evaluating the JML quantified expression, which is either a universal or existential quantifier. Refer to the method translateForAll and translateExists for the structure of the returned code.

 requires quantiExp.isForAll() || quantiExp.isExists();
 ensures \result != null;
 

Throws:
NonExecutableQuantifierException
See Also:
translateForAll(), translateExists()

rangePredicate

private JExpression rangePredicate()
Returns the range predicate of the quantified expression. The result is the conjuntion of explicit and implicit range predicates. The implicit range (e.g., p in (\forall d; r; p ==> q) and (\exists d; r; p && q)) is extracted from the predicate part of the quantified expressions and conjoined to the explicit range predicate (r).

 requires quantiExp.isForAll() || quantiExp.isExists();
 ensures (* \result maybe null *);
 

See Also:
transForAllOrExists()

unwrapJmlExpression

private static JExpression unwrapJmlExpression(JExpression expr)
Unwraps a given JML expression if it is an instance of JmlPredicate or JmlSpecExpression.


transSumOrProduct

private RacNode transSumOrProduct()
                           throws NonExecutableQuantifierException
Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \sum or \product.

 requires quantiExp.isSum() || quantiExp.isProduct();
 

Throws:
NonExecutableQuantifierException
See Also:
translateProduct(), translateSum()

applySumOrProduct

private String applySumOrProduct(String strResultVar,
                                 String strOptr,
                                 String strV2,
                                 CType vType)

transMinOrMax

private RacNode transMinOrMax()
                       throws NonExecutableQuantifierException
Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \min or \max.

 requires quantiExp.isMin() || quantiExp.isMax();
 

Throws:
NonExecutableQuantifierException
See Also:
translateMax(), translateMin()

generateLoop

public RacNode generateLoop(RacNode body)
                     throws NonExecutableQuantifierException
Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range. For example, the interval-based approach returns the following form of code:
  { 
    T l = 0;
    T u = 0;
    [[eval of l and u from predicate part]]
    while (l < u) {
      T x = l;
      result
      l = l + 1;
    }
  }
 
where x is the quantified variable.

Parameters:
body - code to be executed as the loop body
Throws:
NonExecutableQuantifierException - if not executable.

generateLoop

protected abstract RacNode generateLoop(JVariableDefinition varDef,
                                        JExpression qexpr,
                                        String cond,
                                        RacNode result)
                                 throws NonExecutableQuantifierException
Returns a loop code evaluating the body of the quantified predicate.

Parameters:
varDef - quantified variable
qexpr - target expression for interval calculation (i.e., normally, the predicate part of the quantified expression)
cond - additional condition to be conjoined (&&) to the loop condition; null for no conjoinable condition.
result - code for evaluating expression part (or inner loop)
Throws:
NonExecutableQuantifierException - if not executable.
NonExecutableQuantifierException

transExpression

protected RacNode transExpression(JExpression expr,
                                  String var)
Returns code for evaluating expression expr and storing the result to the variable var. As a special case, returns var = true; if expr is null.


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.