org.jmlspecs.jml4.rac
Class ExceptionalPostconditionTranslator

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

public class ExceptionalPostconditionTranslator
extends PostconditionTranslator

Translate the exceptional postcondition of a method or constructor.

Author:

Yoonsik Cheon and Amritam Sarcar

Field Summary

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

localclassTransformation, terms

Constructor Summary

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

Method Summary

MethodDeclaration

translate(JmlMethodSpecification methSpec, AbstractMethodDeclaration meth, java.util.List<java.lang.String> preVars, VariableGenerator vgen, RacResult result) Translates the exceptional precondition of the given method or constructor and returns an exceptional postcondition check method.

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

getOldExpressions, putOldExpressions, translate

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

ExceptionalPostconditionTranslator

public ExceptionalPostconditionTranslator(JmlTypeDeclaration sourceType,
                                          VariableGenerator varGen)

Creates a new postcondition translator for the given type.

Method Detail

translate

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

Translates the exceptional precondition of the given method or constructor and returns an exceptional postcondition check method.

Overrides:

translate in class PostconditionTranslator