org.jmlspecs.jml4.rac
Class ConstraintTranslator

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

All Implemented Interfaces:

TypeAssertionTranslator

public class ConstraintTranslator
extends PostStateExpressionTranslator
implements TypeAssertionTranslator

Translates constraint clauses to history constraint checking methods.

Author:

Amritam Sarcar

Field Summary

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

localclassTransformation, terms

Constructor Summary

ConstraintTranslator(JmlTypeDeclaration type, VariableGenerator varGen)
Creates a new translator.

Method Summary

java.util.List<FieldDeclaration>	newFields() Returns a list of new field declarations generated during the last translation that need to be added to the class or interface under translation.
java.util.List<AbstractMethodDeclaration>	newMethods() Returns a list of new method declarations generated during the last translation that need to be added to the class or interface under translation.
java.util.List<AbstractMethodDeclaration>	translate(TypeDeclaration type, RacResult result) Translates the constraint clauses of the given type to RAC code and returns a list of constraint checking methods.

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

getOldExpressions, getOldQuantifiedExpressions, putOldExpressions, 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

ConstraintTranslator

public ConstraintTranslator(JmlTypeDeclaration type,
                            VariableGenerator varGen)

Creates a new translator.

Method Detail

translate

public java.util.List<AbstractMethodDeclaration> translate(TypeDeclaration type,
                                                           RacResult result)

Translates the constraint clauses of the given type to RAC code and returns a list of constraint checking methods. If the given type is not a JML type declaration or it contains no constraint clause, an empty list is returned.

Specified by:

translate in interface TypeAssertionTranslator

newFields

public java.util.List<FieldDeclaration> newFields()

Returns a list of new field declarations generated during the last translation that need to be added to the class or interface under translation.

newMethods

public java.util.List<AbstractMethodDeclaration> newMethods()

Returns a list of new method declarations generated during the last translation that need to be added to the class or interface under translation.