org.jmlspecs.jmlrac
Class TransPostcondition

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.checker.JmlAbstractVisitor
          org.jmlspecs.jmlrac.RacAbstractVisitor
              org.jmlspecs.jmlrac.AbstractExpressionTranslator
                  org.jmlspecs.jmlrac.TransExpression
                      org.jmlspecs.jmlrac.TransPredicate
                          org.jmlspecs.jmlrac.TransPostcondition

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, JmlVisitor, MjcVisitor, RacConstants, RacVisitor

public class TransPostcondition

extends TransPredicate

A RAC visitor class for transforming JML postconditions into Java source code. The generated code is a sequence of Java statements that evaluate and store the boolean result in the given variable. The boolean result variable is assumed to be declared in the outer scope that incorporates the code.

Version:

$Revision: 1.31 $

Author:

Yoonsik Cheon

See Also:

TransExpression, TransPredicate

Nested Class Summary
private  class	TransPostcondition.QVarChecker           A class to check whether an expression has any references to quantified variables.

 

Nested classes inherited from class org.jmlspecs.jmlrac.TransExpression

TransExpression.DiagTerm

 

Field Summary
private  boolean	forStatic           Indicates whether this translation is for a static method declaration.
private  List	oldExprs           A list of RacNode's representing old expressions that must be executed in the pre-state.
private  VarGenerator	oldVarGen           Variable generator to be used in the translation of old expression.
private  Stack	quantifiers           The set of quantifiers that enclose the old expression currently being translated.

 

Fields inherited from class org.jmlspecs.jmlrac.TransExpression

context, expression, paramStack, resultStack, resultVar, typeDecl, varGen

 

Fields inherited from class org.multijava.util.Utils

DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO

 

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

 

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

 

Constructor Summary

TransPostcondition(VarGenerator varGen, RacContext ctx, VarGenerator oldVarGen, boolean forStatic, JExpression pred, String resultVar, JTypeDeclarationType typeDecl)           Constructs a new instance and translates the given postcondition, pred.

 

Method Summary
private  String	buildKey()           Returns a key for retrieving the value of old expression currently being translated.
private  boolean	hasQuantifiedVar(JmlSpecExpressionWrapper expr)           Does the given old or pre expression, expr, have any free quantified variables?
private  void	oldExpressionInQuantifiers(JmlSpecExpressionWrapper self)           Translates a JML old expression, self, enclosed in quantifiers.
List	oldExprs()           Returns a list of old expressions (as RacNode) that must be executed in the pre-state.
void	transPreExpression(JmlSpecExpressionWrapper self)
void	visitJmlOldExpression(JmlOldExpression self)           Translates a JML old expression.
void	visitJmlPreExpression(JmlPreExpression self)           Translates a JML pre expression.
void	visitJmlResultExpression(JmlResultExpression self)           Translates a JML result expression.
void	visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)           Translates the given JML quantified expression.

 

Methods inherited from class org.jmlspecs.jmlrac.TransPredicate

wrappedStmt

 

Methods inherited from class org.jmlspecs.jmlrac.TransExpression

addDiagTerm, addDiagTermResult, addDiagTermThis, applyArrayAccessExpression, applyCast, applyOperator, applyOperator, booleanNonExecutableExpression, canMakeStaticCall, defaultValue, diagTerms, freshVar, GET_ARGUMENT, GET_RESULT, guardUndefined, hasDiagTerms, initDiagTerms, isNonExecutableFieldReference, nonExecutableExpression, PEEK_ARGUMENT, perform, PUT_ARGUMENT, RETURN_RESULT, specAccessorNeeded, stmt, toString, translate, translate, translateEquivalence, translateImplication, translateIsSubtypeOf, transPrefix, transPrefixSpec, visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssignmentExpression, visitBigintLiteral, visitBinaryExpression, visitBitwiseExpression, visitBooleanBinaryExpression, visitBooleanLiteral, visitByteLiteral, visitCastExpression, visitCharLiteral, visitClassExpression, visitCompoundAssignmentExpression, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitDivideExpression, visitDoubleLiteral, visitEqualityExpression, visitExplicitConstructorInvocation, visitFieldExpression, visitFloatLiteral, visitInstanceofExpression, visitIntLiteral, visitJmlElemTypeExpression, visitJmlFreshExpression, visitJmlInformalExpression, visitJmlInvariantForExpression, visitJmlIsInitializedExpression, visitJmlLabelExpression, visitJmlLockSetExpression, visitJmlMaxExpression, visitJmlNonNullElementsExpression, visitJmlNotAssignedExpression, visitJmlNotModifiedExpression, visitJmlPredicate, visitJmlReachExpression, visitJmlRelationalExpression, visitJmlSetComprehension, visitJmlSpecExpression, visitJmlTypeExpression, visitJmlTypeOfExpression, visitLocalVariableExpression, visitLongLiteral, visitMethodCallExpression, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRacPredicate, visitRealLiteral, visitRelationalExpression, visitShiftExpression, visitShortLiteral, visitStringLiteral, visitSuperExpression, visitThisExpression, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, warn, wrapBooleanResult, wrapBooleanResultTC, wrappedStmt

 

Methods inherited from class org.jmlspecs.jmlrac.RacAbstractVisitor

visitRacNode

 

Methods inherited from class org.jmlspecs.checker.JmlAbstractVisitor

visitAssertStatement, visitBlockStatement, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion, visitLabeledStatement, visitMathModeExpression, visitMethodDeclaration, visitPackageImport, visitPackageName, visitReturnStatement, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement

 

Methods inherited from class org.multijava.util.Utils

assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray

 

Methods inherited from class java.lang.Object

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

 

Methods inherited from interface org.jmlspecs.checker.JmlVisitor

visitJmlAbruptSpecBody, visitJmlAbruptSpecCase, visitJmlAccessibleClause, visitJmlAssertStatement, visitJmlAssignableClause, visitJmlAssignmentStatement, visitJmlAssumeStatement, visitJmlAxiom, visitJmlBehaviorSpec, visitJmlBreaksClause, visitJmlCallableClause, visitJmlCapturesClause, visitJmlClassBlock, visitJmlClassDeclaration, visitJmlClassOrGFImport, visitJmlCodeContract, visitJmlCompilationUnit, visitJmlConstraint, visitJmlConstructorDeclaration, visitJmlConstructorName, visitJmlContinuesClause, visitJmlDebugStatement, visitJmlDeclaration, visitJmlDivergesClause, visitJmlDurationClause, visitJmlDurationExpression, visitJmlEnsuresClause, visitJmlExample, visitJmlExceptionalBehaviorSpec, visitJmlExceptionalExample, visitJmlExceptionalSpecBody, visitJmlExceptionalSpecCase, visitJmlExpression, visitJmlExtendingSpecification, visitJmlFieldDeclaration, visitJmlForAllVarDecl, visitJmlFormalParameter, visitJmlGeneralSpecCase, visitJmlGenericSpecBody, visitJmlGenericSpecCase, visitJmlGuardedStatement, visitJmlHenceByStatement, visitJmlInformalStoreRef, visitJmlInGroupClause, visitJmlInitiallyVarAssertion, visitJmlInterfaceDeclaration, visitJmlInvariant, visitJmlInvariantStatement, visitJmlLetVarDecl, visitJmlLoopInvariant, visitJmlLoopStatement, visitJmlMapsIntoClause, visitJmlMeasuredClause, visitJmlMethodDeclaration, visitJmlMethodName, visitJmlMethodNameList, visitJmlMethodSpecification, visitJmlModelProgram, visitJmlMonitorsForVarAssertion, visitJmlName, visitJmlNode, visitJmlNondetChoiceStatement, visitJmlNondetIfStatement, visitJmlNormalBehaviorSpec, visitJmlNormalExample, visitJmlNormalSpecBody, visitJmlNormalSpecCase, visitJmlOnlyAccessedExpression, visitJmlOnlyAssignedExpression, visitJmlOnlyCalledExpression, visitJmlOnlyCapturedExpression, visitJmlPackageImport, visitJmlPredicateKeyword, visitJmlReadableIfVarAssertion, visitJmlRedundantSpec, visitJmlRefinePrefix, visitJmlRepresentsDecl, visitJmlRequiresClause, visitJmlReturnsClause, visitJmlSetStatement, visitJmlSignalsClause, visitJmlSignalsOnlyClause, visitJmlSpaceExpression, visitJmlSpecBody, visitJmlSpecification, visitJmlSpecStatement, visitJmlSpecVarDecl, visitJmlStoreRef, visitJmlStoreRefExpression, visitJmlStoreRefKeyword, visitJmlUnreachableStatement, visitJmlVariableDefinition, visitJmlVariantFunction, visitJmlWhenClause, visitJmlWorkingSpaceClause, visitJmlWorkingSpaceExpression, visitJmlWritableIfVarAssertion

 

Methods inherited from interface org.multijava.mjc.MjcVisitor

visitAssertStatement, visitBlockStatement, visitBreakStatement, visitCatchClause, visitClassBlock, visitClassDeclaration, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDoStatement, visitEmptyStatement, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInterfaceDeclaration, visitLabeledStatement, visitMathModeExpression, visitMethodDeclaration, visitPackageImport, visitPackageName, visitReturnStatement, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement

 

Field Detail

forStatic

private boolean forStatic

Indicates whether this translation is for a static method declaration.

oldExprs

private List oldExprs

A list of RacNode's representing old expressions that must be executed in the pre-state.

oldVarGen

private VarGenerator oldVarGen

Variable generator to be used in the translation of old expression.

quantifiers

private Stack quantifiers

The set of quantifiers that enclose the old expression currently being translated.

 private invariant (\forall Object o; quantifiers.contains(o);
   o instanceof JmlSpecQuantifiedExpression);
 

TransPostcondition

public TransPostcondition(VarGenerator varGen,
                          RacContext ctx,
                          VarGenerator oldVarGen,
                          boolean forStatic,
                          JExpression pred,
                          String resultVar,
                          JTypeDeclarationType typeDecl)

Constructs a new instance and translates the given postcondition, pred. The translated Java source code can be accessed by such accessor methods as stmt() and wrappedStmt.

Parameters:

resultVar - variable to store the result

oldExprs

public List oldExprs()

Returns a list of old expressions (as RacNode) that must be executed in the pre-state. The declaration of a local variable to hold the result of the expression is stored in the name field of class RacNode. This method must be called after translation.

 normal_behavior
  assignable translated;
  ensures \result != null && \result == oldExprs;
 

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)

Translates a JML pre expression. The translation rules for this expression is defined as follows.

   [[\pre(E), r]] = 
      r = v;  
 

with the addition of a field declaration private T_E v = d_T_E; to the target class, and the insertion of evaluation [[E, v]] into the method prolog.

Specified by:

visitJmlPreExpression in interface JmlVisitor

Overrides:

visitJmlPreExpression in class TransExpression

See Also:

TransOldExpression

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)

Translates a JML old expression. The translation rules for this expression is defined as follows.

   [[\old(E), r]] = 
      r = v;  
 

with the addition of a field declaration private T_E v = d_T_E; to the target class, and the insertion of evaluation [[E, v]] into the method prolog.

Specified by:

visitJmlOldExpression in interface JmlVisitor

Overrides:

visitJmlOldExpression in class TransExpression

See Also:

TransOldExpression

transPreExpression

public void transPreExpression(JmlSpecExpressionWrapper self)

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)

Translates the given JML quantified expression. It is overridden here to keep track of the set of quantifiers that enclose the old expression currently being translated.

Specified by:

visitJmlSpecQuantifiedExpression in interface JmlVisitor

Overrides:

visitJmlSpecQuantifiedExpression in class TransExpression

See Also:

visitJmlPreExpression(JmlPreExpression), visitJmlOldExpression(JmlOldExpression)

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)

Translates a JML result expression. The translation rules for this expression is defined as follows.

   [[\result, r]] = 
     r = VN_RESULT;
 

with the insertion of a variable declaration T VN_RESULT = d_T; into the method proglog, where T is the return type of the method. The variable VN_RESULT is used to capture the return value of the method.

Specified by:

visitJmlResultExpression in interface JmlVisitor

Overrides:

visitJmlResultExpression in class TransExpression

hasQuantifiedVar

private boolean hasQuantifiedVar(JmlSpecExpressionWrapper expr)

Does the given old or pre expression, expr, have any free quantified variables?

oldExpressionInQuantifiers

private void oldExpressionInQuantifiers(JmlSpecExpressionWrapper self)

Translates a JML old expression, self, enclosed in quantifiers. The translation generates code that evaluates the old expression for each combination of bound variables of quantifiers and stores the result to a private cache. The original old expression is replaced with cache lookup code.

 requires !quantifiers.isEmpty();
 assignable oldExprs, resultStack;
 

buildKey

private String buildKey()

Returns a key for retrieving the value of old expression currently being translated. We store the old expression values as a mapping from quantified (bound) variables to values, and the quantified variables beomes a key. For example, if the quantifiers are x1, x2, ..., xn, the key is new Object[] { x1, x2, ..., xn }, where xi is wrapped if necessary.

 requires !quantifiers.isEmpty();
 ensures \result != null;