org.jmlspecs.jml4.rac
Class InlineAssertionTranslator

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

public class InlineAssertionTranslator
extends ExpressionTranslator

Translates in-line assertions o RAC code.

Author:

Amritam Sarcar and Yoonsik Cheon

Field Summary

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

localclassTransformation, terms

Constructor Summary

InlineAssertionTranslator(VariableGenerator varGen)

Method Summary

java.lang.StringBuffer	translate(AbstractMethodDeclaration meth, RacResult result) Translates in-line assertions contained in the body of the given method to RAC code.
java.lang.StringBuffer	translate(Initializer initBlock, RacResult result)

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

InlineAssertionTranslator

public InlineAssertionTranslator(VariableGenerator varGen)

Method Detail

translate

public java.lang.StringBuffer translate(AbstractMethodDeclaration meth,
                                        RacResult result)

Translates in-line assertions contained in the body of the given method to RAC code. The return value is a sequence of RAC code (in a string form), one for each in-line assertion, in the AST traversal order. It is empty, if the body is empty or contains no in-line assertion. Other translation information is stored in result.

  ensures \result != null;
 

translate

public java.lang.StringBuffer translate(Initializer initBlock,
                                        RacResult result)

See Also:

translateForMeth