org.jmlspecs.jml4.rac.quantifiedexpression
Class QInterval

java.lang.Object
  org.jmlspecs.jml4.rac.quantifiedexpression.QInterval

All Implemented Interfaces:

RacConstants

public class QInterval
extends java.lang.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, Amritam Sarcar

Nested Class Summary

Nested classes/interfaces inherited from interface org.jmlspecs.jml4.rac.RacConstants

RacConstants.Behavior, RacConstants.Condition

Field Summary

Fields inherited from interface org.jmlspecs.jml4.rac.RacConstants

ANNOTATION, AT_GHOST, AT_MODEL, EMPTY_STRING, ENTIRE_CLAUSE, ERROR_NEVER_CALL, ERROR_NOT_IMPL, ERROR_RAC_IMPL, GHOST_METHOD_PREFIX, HELPER, ID_INSTANCE_DOLLAR, ID_STATIC, INTERNAL_CONSTRUCTOR_PREFIX, INTERNAL_METHOD_PREFIX, JML_CHECKABLE, 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, MODEL_METHOD_PREFIX, NON_EXEC, PKG_RAC_RUNTIME, RAC_TMP_FILE_EXTENSION, RAC_TMP_FILE_PREFIX, TN_BOOLEAN, TN_CONSTRAINT_ERROR, TN_ENTRY_PRECONDITON_ERROR, TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR, TN_EXIT_NORMAL_POSTCONDITION_ERROR, TN_INVARIANT_ERROR, TN_JMLCACHE, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_LOCATION, TN_SURROGATE, TN_VOID, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_MSG, VN_NAME, VN_OLD_VAR, VN_PARAMS, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_VALUE_SET, VN_XRESULT

Constructor Summary

QInterval(Expression expr, java.lang.String var, java.util.Collection xvars, TypeBinding type, RacResult racResult, SourceTypeBinding typeBinding)
Construct a QInterval object representing the quantifed interval for a (quantified) variable var with respect to the expression expr.

Method Summary

java.lang.String

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

Methods inherited from class java.lang.Object

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

Constructor Detail

QInterval

public QInterval(Expression expr,
                 java.lang.String var,
                 java.util.Collection xvars,
                 TypeBinding type,
                 RacResult racResult,
                 SourceTypeBinding typeBinding)

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

translate

public java.lang.String translate(VariableGenerator varGen,
                                  java.lang.String lowerVar,
                                  java.lang.String upperVar,
                                  PostStateExpressionTranslator 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