QInterval (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jmlrac.qexpr
Class QInterval

java.lang.Object
  org.jmlspecs.jmlrac.qexpr.QInterval

All Implemented Interfaces:: Constants, Constants, Constants, RacConstants

class QInterval
extends Object
implements RacConstants

A class for static approximations of the intervals for quantified variables of integeral types. For example, the static approximation of the interval for a quantified variable x with respect to an expression x <= 0 && x >= 10 is the interval between 0 and 10 including both ends.

Version:: $Revision: 1.11 $
Author:: Yoonsik Cheon

Nested Class Summary

private static class QInterval.Bound
          A class for representing tuples of JExpression objects and int values.

private static class QInterval.CheckRecursion
          A class to check an appearance of local variables in an expression.

Field Summary

private List lower
          a list of Bound objects representing the lower bound.

private CType type
          The type of the quantified variable.

private List upper
          a list of Bound objects representing the upper bound.

private String var
          the quantified variable name

private Collection xvars
          names of excluded variables private invariant xvars.contains(var);

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

QInterval(JExpression expr, String var, Collection xvars, CType type)
          Construct a QInterval object representing the quantifed interval for a (quantified) variable var with respect to the expression expr.

Method Summary

private void calculate(JExpression expr)
          Calculate the quantified interval with respect to the given expression.

private static boolean isLocalVariable(JExpression expr, String var)
          Is the expression expr a local variable expression consisting of variable named var?

private RacNode transBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExp, QInterval.Bound bound, int opr)
          Returns code that evaluates the given lower or upper bound.

RacNode translate(VarGenerator varGen, String lowerVar, String upperVar, AbstractExpressionTranslator transExp)
          Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.

private RacNode transLBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExpr, QInterval.Bound bound)
          Returns code that evaluates the given lower bound.

private RacNode transUBound(VarGenerator varGen, String var, AbstractExpressionTranslator transExpr, QInterval.Bound bound)
          Returns code that evaluates the given upper bound.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

lower

private List lower

a list of Bound objects representing the lower bound.


 private invariant (\forall Bound b; lower.contains(b);
                      b.oper == OPE_LT || b.oper == OPE_LE);

upper

private List upper

a list of Bound objects representing the upper bound.


 private invariant (\forall Bound b; upper.contains(b);
                      b.oper == OPE_GT || b.oper == OPE_GE);

var

private String var

the quantified variable name

See Also:: xvars

xvars

private Collection xvars

names of excluded variables


 private invariant xvars.contains(var);

type

private CType type

The type of the quantified variable.

Constructor Detail

QInterval

public QInterval(JExpression expr,
                 String var,
                 Collection xvars,
                 CType type)

Construct a QInterval object representing the quantifed interval for a (quantified) variable var with respect to the expression expr. The variables in xvars can't appear in the expressions defining the interval for var.


  requires xvars.contains(var);

Method Detail

calculate

private void calculate(JExpression expr)

Calculate the quantified interval with respect to the given expression.


  modifies lower, upper;

isLocalVariable

private static boolean isLocalVariable(JExpression expr,
                                       String var)

Is the expression expr a local variable expression consisting of variable named var?

transLBound

private RacNode transLBound(VarGenerator varGen,
                            String var,
                            AbstractExpressionTranslator transExpr,
                            QInterval.Bound bound)

Returns code that evaluates the given lower bound. The returned code has the following form:

  [T tvar = 0;]
  [[bound.expr, tvar]]
  [var = (T_of_var) tvar;]
  var = var + 1; // if bound.oper is <

transUBound

private RacNode transUBound(VarGenerator varGen,
                            String var,
                            AbstractExpressionTranslator transExpr,
                            QInterval.Bound bound)

Returns code that evaluates the given upper bound. The returned code has the following form:

  [T tvar = 0;]
  [[bound.expr, tvar]]
  [var = (T_of_var) tvar;]
  var = var + 1; // if bound.oper is >=

transBound

private RacNode transBound(VarGenerator varGen,
                           String var,
                           AbstractExpressionTranslator transExp,
                           QInterval.Bound bound,
                           int opr)

Returns code that evaluates the given lower or upper bound. The returned code has the following form:

  [T tvar = 0;]
  [[bound.expr, tvar]]
  [var = (T_of_var) tvar;]
  var = var + 1; // if bound.oper is opr

translate

public RacNode translate(VarGenerator varGen,
                         String lowerVar,
                         String upperVar,
                         AbstractExpressionTranslator transExp)
                  throws NonExecutableQuantifierException

Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.

Parameters:

varGen - the variable generator to be used in the translation for generating unique local variables.

lowerVar - the variable name to refer to the lower bound value in the translated code.

upperVar - the variable name to refer to the upper bound value in the translated code.

transExp - the translator to use for translating JML expressions.

Throws:

NonExecutableQuantifierException - if no interval is found. The translated code has the following form (lowerVar <= qvar < upperVar):

  [[l1, lowerVar]]
  lowerVar = lowerVar + 1; // if l1.oper is <
  T v = 0;
  [[li, v]]                // for i=2, ..., n
  v = v + 1;               // if li.oper is <
  lowerVar = Math.max(lowerVar, v);  
  [[u1, upperVar]]
  upperVar = upperVar + 1; // if u1.oper is >=
  [[ui, v]]                // for i=2, ..., n
  v = v + 1;               // if ui.oper is >=
  upperVar = Math.min(upperVar, v);

where li and ui are lower and upper bounds accumlated.

NonExecutableQuantifierException