org.jmlspecs.jml4.rac
Class MethodDeclarationTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.MethodDeclarationTranslator

public class MethodDeclarationTranslator
extends java.lang.Object

Translate a method declaration into RAC code. This class translates a method or constructor declaration into RAC code, and the resulting RAC code may consist of new field and method declarations. Given a method m of class T, this class may produce the following member declarations that need to be added to the owning class T.

• A wrapper method: m
• An internal method: internal$m
• A precondition check method: checkPre$m$T
• A normal postcondition check method: checkPost$m$T
• An excpetional postcondition check method: checkXPost$m$T
• A pre-values stack field: rac$stacki
• A pair of pre-values stack push and pop method: saveTo$rac$stacki, and restoreFrom$rac$stacki
• A set of fields for storing pre-state values such as preconditions, old variables, and old expressions.

To use this class, follow the three steps shown below.

1. Create a new instance by calling either forClass(JmlTypeDeclaration, VariableGenerator) or #forInterface(JmlTypeDeclaration, VariableGenerator); the first is for translating class methods and the second is for translating interface methods.
2. Invoke the translate(AbstractMethodDeclaration) method to translate a method declaration.
3. Retrieve translation result by invoking newFields() and newMethods().

Author:

Yoonsik Cheon and Amritam Sarcar

Method Summary

static MethodDeclarationTranslator	forClass(JmlTypeDeclaration typeDecl, VariableGenerator varGen) Creates a translator for translating methods contained in the given type.
static MethodDeclarationTranslator	forInterface(JmlTypeDeclaration typeDecl, VariableGenerator varGen, boolean tSpec) Creates a translator for translating methods contained in the given type.
boolean	hasNewFields() Returns true if new field declarations have been generated during the last translation.
boolean	hasNewMethods() Returns true if new method declarations have been generated during the last translation.
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.
RacResult	translate(AbstractMethodDeclaration meth) Translates the given method to RAC code.
RacResult	translate(MethodBinding meth) Translates the given method to RAC code.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

forClass

public static MethodDeclarationTranslator forClass(JmlTypeDeclaration typeDecl,
                                                   VariableGenerator varGen)

Creates a translator for translating methods contained in the given type. The given type is assumed to be a class declaration, and the translator will use the given variable generator to create various kinds of unique RAC variables and fields. The variable generator is assumed to be created with VariableGenerator.forClass().

forInterface

public static MethodDeclarationTranslator forInterface(JmlTypeDeclaration typeDecl,
                                                       VariableGenerator varGen,
                                                       boolean tSpec)

Creates a translator for translating methods contained in the given type. The given type is assumed to be an interface declaration, and the translator will use the given variable generator to create various kinds of unique RAC variables and fields. The variable generator is assumed to be created with VariableGenerator.forClass().

hasNewFields

public boolean hasNewFields()

Returns true if new field declarations have been generated during the last translation.

hasNewMethods

public boolean hasNewMethods()

Returns true if new method declarations have been generated during the last translation.

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.

translate

public RacResult translate(AbstractMethodDeclaration meth)

Translates the given method to RAC code. The translation results in new field and method declarations.

Returns:

TODO

See Also:

newFields(), newMethods()

translate

public RacResult translate(MethodBinding meth)

Translates the given method to RAC code. The translation results in new field and method declarations.

Returns:

TODO

See Also:

newFields(), newMethods()