org.jmlspecs.jml4.rac.quantifiedexpression
Class StaticAnalysis

java.lang.Object
  org.jmlspecs.jml4.rac.quantifiedexpression.Translator
      org.jmlspecs.jml4.rac.quantifiedexpression.StaticAnalysis

All Implemented Interfaces:

RacConstants

public abstract class StaticAnalysis
extends Translator

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

Method Summary

java.lang.String	generateLoop(ASTNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
static StaticAnalysis	getInstance(VariableGenerator varGen, RacContext ctx, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding) Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.
java.lang.String	translate() Translate a JML quantified expression into Java source code and return the result.

Methods inherited from class java.lang.Object

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

Method Detail

getInstance

public static StaticAnalysis getInstance(VariableGenerator varGen,
                                         RacContext ctx,
                                         JmlQuantifiedExpression expr,
                                         java.lang.String resultVar,
                                         PostStateExpressionTranslator transExp,
                                         RacResult racResult,
                                         SourceTypeBinding typeBinding)

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.

racResult - data structure of rac results

typeBinding - sourceType

translate

public java.lang.String translate()
                           throws NonExecutableQuantifierException

Translate a JML quantified expression into Java source code and return the result.

Specified by:

translate in class Translator

Returns:

translated Java source code.

Throws:

NonExecutableQuantifierException - if not executable.

NonExecutableQuantifierException - if not executable.

generateLoop

public java.lang.String generateLoop(ASTNode 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.

Specified by:

generateLoop in class Translator

Parameters:

body - code to be executed as the loop body

Throws:

NonExecutableQuantifierException - if not executable.