org.jmlspecs.jml4.rac
Class PostconditionTranslator

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

Direct Known Subclasses:

ExceptionalPostconditionTranslator

public class PostconditionTranslator
extends PostStateExpressionTranslator

Field Summary

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

localclassTransformation, terms

Constructor Summary

PostconditionTranslator(JmlTypeDeclaration sourceType, VariableGenerator varGen)
Creates a new postcondition translator for the given type.

Method Summary

java.util.List<RacOldExpression>	getOldExpressions() Return all old expressions found in the postcondition.
void	putOldExpressions(java.util.List<RacOldExpression> oldExp) Puts old expressions found in the expression under translation.
java.lang.String	translate(Expression expression, TypeBinding type, RacResult result) Translates the given expression of the given type.
MethodDeclaration	translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the postcondition of the given method or constructor and returns a postcondition check method.

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

getOldQuantifiedExpressions, translate

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

PostconditionTranslator

public PostconditionTranslator(JmlTypeDeclaration sourceType,
                               VariableGenerator varGen)

Creates a new postcondition translator for the given type.

Method Detail

getOldExpressions

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

Return all old expressions found in the postcondition.

Overrides:

getOldExpressions in class PostStateExpressionTranslator

putOldExpressions

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

Puts old expressions found in the expression under translation.

Overrides:

putOldExpressions in class PostStateExpressionTranslator

translate

public MethodDeclaration translate(JmlMethodSpecification methSpec,
                                   AbstractMethodDeclaration meth,
                                   java.util.List<java.lang.String> preVars,
                                   VariableGenerator vgen,
                                   RacResult result)

Translates the postcondition of the given method or constructor and returns a postcondition check method. Certain translation results such as whether inheriting a specification is stored in racResult.n

translate

public java.lang.String translate(Expression expression,
                                  TypeBinding type,
                                  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. This method is overridden here to also collect printable terms for violation reporting.