org.jmlspecs.jml4.rac
Class PostStateExpressionTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.ExpressionTranslator
      org.jmlspecs.jml4.rac.PostStateExpressionTranslator

Direct Known Subclasses:

ConstraintTranslator, PostconditionTranslator, PreconditionTranslator

public class PostStateExpressionTranslator
extends ExpressionTranslator

Translates various Java and JML expressions to RAC code that may contain JML old expressions. The translated code is also an expression; perhaps, this approach may not work for complex JML expressions such as quantifiers which are currently not supported.

A JML old expression is translated into a unique new field, and its value is set by the precondition check method; i.e., an old expression is evaluated in the pre-state by the precondition check method, and its value is stored into the new field so that postcondition check methods can refer to it. For example, given an old expression \old(x + 1), the translation produces:

   ((java.lang.Integer) rac$old0.value()).intValue()
  

where rac$old0 is a new field introduced to store the value of the old expression. The field is declared as follows.

   private [static] JMLRacValue rac$old0;
  

And its value is assigned in the precondition check method as follows.

   rac$old0 = JMLRacValue.ofObject(new java.lang.Integer(x + 1));
  

Author:

Yoonsik Cheon and Amritam Sarcar

Field Summary

Fields inherited from class org.jmlspecs.jml4.rac.ExpressionTranslator

localclassTransformation, terms

Constructor Summary

PostStateExpressionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGenerator)

PostStateExpressionTranslator(VariableGenerator varGenerator, boolean isOn)

Method Summary

java.util.List<RacOldExpression>	getOldExpressions() Returns old expressions found in the expression under translation.
java.util.List<RacOldExpression>	getOldQuantifiedExpressions() Returns old expressions found in quantifiers under translation.
void	putOldExpressions(java.util.List<RacOldExpression> oldExp) Puts old expressions found in the expression under translation.
java.lang.String	translate(Expression expr, TypeBinding type, boolean isStaticExpr, VariableGenerator vgen, RacResult result) Translates the given expression of the given type.

Methods inherited from class org.jmlspecs.jml4.rac.ExpressionTranslator

embedSpecCase, getTerms, isPresent, setEvaluatorPDef, setEvaluatorPUse, translate, translate, translate, translate, translate

Methods inherited from class java.lang.Object

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

Constructor Detail

PostStateExpressionTranslator

public PostStateExpressionTranslator(JmlTypeDeclaration sourceType,
                                     VariableGenerator varGenerator)

PostStateExpressionTranslator

public PostStateExpressionTranslator(VariableGenerator varGenerator,
                                     boolean isOn)

Method Detail

getOldQuantifiedExpressions

public java.util.List<RacOldExpression> getOldQuantifiedExpressions()

Returns old expressions found in quantifiers under translation.

getOldExpressions

public java.util.List<RacOldExpression> getOldExpressions()

Returns old expressions found in the expression under translation.

putOldExpressions

public void putOldExpressions(java.util.List<RacOldExpression> oldExp)

Puts old expressions found in the expression under translation.

translate

public java.lang.String translate(Expression expr,
                                  TypeBinding type,
                                  boolean isStaticExpr,
                                  VariableGenerator vgen,
                                  RacResult result)

Translates the given expression of the given type. The returned value is a string representation of the translated expression, which is also an expression.