org.jmlspecs.jml4.rac
Class InvariantTranslator

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

All Implemented Interfaces:

TypeAssertionTranslator

public class InvariantTranslator
extends ExpressionTranslator
implements TypeAssertionTranslator

Translates invariants clauses to invariant checking methods.

Author:

Amritam Sarcar and Yoonsik Cheon TODO: (1) Static vs. non-static invariants.

Field Summary

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

localclassTransformation, terms

Constructor Summary

InvariantTranslator(VariableGenerator varGen)
Creates a new translator.

Method Summary

java.util.List<AbstractMethodDeclaration>

translate(TypeDeclaration type, RacResult result) Translates the invariant clauses of the given type to RAC code and returns a list of invariant checking methods.

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

InvariantTranslator

public InvariantTranslator(VariableGenerator varGen)

Creates a new translator.

Method Detail

translate

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

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

Specified by:

translate in interface TypeAssertionTranslator