org.jmlspecs.jml4.rac.quantifiedexpression
Class Translator

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

All Implemented Interfaces:

RacConstants

Direct Known Subclasses:

StaticAnalysis

public abstract class Translator
extends java.lang.Object
implements RacConstants

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

abstract 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.
abstract 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

translate

public abstract java.lang.String 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.

generateLoop

public abstract 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.

Parameters:

body - code to be executed as the loop body

Throws:

NonExecutableQuantifierException - if not executable.