org.jmlspecs.jml4.rac
Class PreconditionTranslator

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

public class PreconditionTranslator
extends PostStateExpressionTranslator

Translates the precondition of a method or constructor into RAC code. This class translates a precondition into a precondition check method. An object of this class should be used as follows.

1. First, invokes the #translate(AbstractMethodDeclaration, VariableGenerator) method to translate a precondition of a method or constructor to RAC code. After this invocation, the names of precondition variables become available (see getPreconditionVariables()); these names are needed to generate postcondition check methods.
2. Next, invokes the getPreconditionMethod(Collection, RacResult) to creates a postcondition method.

Author:

Yoonsik Cheon and Amritam Sarcar

Field Summary

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

localclassTransformation, terms

Constructor Summary

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

Method Summary

java.util.List<RacOldExpression>	getOldExpressions() Return all old expressions found in the postcondition.
MethodDeclaration	getPreconditionMethod(java.util.Collection<RacOldExpression> oldExprs, RacResult racResult) Returns a precondition check method that also executes the given old expressions (in the pre-state).
java.util.List<java.lang.String>	getPreconditionVariables() Returns names of boolean fields to store the truth of preconditions, one for each specification case in a method specification.
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.
void	translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, VariableGenerator vgen, RacResult result) Translates the precondition of the given method into RAC code.

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

PreconditionTranslator

public PreconditionTranslator(JmlTypeDeclaration sourceType,
                              VariableGenerator varGen)

Creates a new precondition translator for the given type.

Method Detail

getPreconditionVariables

public java.util.List<java.lang.String> getPreconditionVariables()

Returns names of boolean fields to store the truth of preconditions, one for each specification case in a method specification. This method should be called after a prepareTranslation method call.

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 void translate(JmlMethodSpecification methSpec,
                      AbstractMethodDeclaration meth,
                      VariableGenerator vgen,
                      RacResult result)

Translates the precondition of the given method into RAC code. The side effect of this method is that the set of precondition variables become known and can be retrieved by calling getPreconditionVariables(). After this call, the precondition method becomes available by calling getPreconditionMethod(Collection, RacResult).

See Also:

getPreconditionVariables(), getPreconditionMethod(Collection, RacResult)

getPreconditionMethod

public MethodDeclaration getPreconditionMethod(java.util.Collection<RacOldExpression> oldExprs,
                                               RacResult racResult)

Returns a precondition check method that also executes the given old expressions (in the pre-state). This method should be called after calling the #translate(AbstractMethodDeclaration, VariableGenerator).

Parameters:

racResult - TODO

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.