org.jmlspecs.jml4.rac
Class MethodSpecificationTranslator

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

public class MethodSpecificationTranslator
extends java.lang.Object

Translate a method declaration into RAC code. This class translates a method or constructor declaration into RAC code. The resulting RAC code consists of new field and method declarations.

Note that a non_null annotation to a formal parameter is treated as a precondition. It is conjoined to the precondition in that a non-null annotated formal parameter x has the same effect as conjoining a predicate x != null to the precondition. However, this feature is not implemented yet.

Author:

Yoonsik Cheon and Amritam Sarcar

Constructor Summary

MethodSpecificationTranslator(JmlTypeDeclaration typeDecl, VariableGenerator varGen)
Creates a new translator for translating methods of the given type declaration that uses the given variable generator.

Method Summary

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 declaratons 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.

Methods inherited from class java.lang.Object

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

Constructor Detail

MethodSpecificationTranslator

public MethodSpecificationTranslator(JmlTypeDeclaration typeDecl,
                                     VariableGenerator varGen)

Creates a new translator for translating methods of the given type declaration that uses the given variable generator. The variable generator is used to create unique RAC variables and is assumed to be created with VariableGenerator.forClass().

Method Detail

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 declaratons 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.

See Also:

newFields(), newMethods()