JML

org.jmlspecs.jmlrac.qexpr
Class QInterval

java.lang.Object
  extended byorg.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

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.