org.jmlspecs.jml4.rac
Class InterfaceDeclarationTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.RacTranslator
      org.jmlspecs.jml4.rac.TypeDeclarationTranslator
          org.jmlspecs.jml4.rac.InterfaceDeclarationTranslator

All Implemented Interfaces:

RacConstants

public class InterfaceDeclarationTranslator
extends TypeDeclarationTranslator

Translates JML assertions associated with interfaces to runtime assertion checking (RAC) code. This class is for translating various JML assertions associated with Java interfaces to RAC code. The translated RAC code will be hosted in a new class declaration node, called a surrogate class, which is supposed to be pretty printed and parsed to be merged to the AST of the source interface, as a member class.

Author:

Amritam Sacar and Yoonsik Cheon

Nested Class Summary

Nested classes/interfaces inherited from interface org.jmlspecs.jml4.rac.RacConstants

RacConstants.Behavior, RacConstants.Condition

Field Summary

Fields inherited from interface org.jmlspecs.jml4.rac.RacConstants

ANNOTATION, AT_GHOST, AT_MODEL, EMPTY_STRING, ENTIRE_CLAUSE, ERROR_NEVER_CALL, ERROR_NOT_IMPL, ERROR_RAC_IMPL, GHOST_METHOD_PREFIX, HELPER, ID_INSTANCE_DOLLAR, ID_STATIC, INTERNAL_CONSTRUCTOR_PREFIX, INTERNAL_METHOD_PREFIX, JML_CHECKABLE, MN_CHECK_HC, MN_CHECK_INV, MN_CHECK_POST, MN_CHECK_PRE, MN_CHECK_XPOST, MN_EVAL_OLD, MN_GHOST, MN_INIT, MN_INTERNAL, MN_MODEL, MN_MODEL_PUBLIC, MN_RESTORE_FROM, MN_SAVE_TO, MN_SPEC, MN_SPEC_PUBLIC, MODEL_METHOD_PREFIX, NON_EXEC, PKG_RAC_RUNTIME, RAC_TMP_FILE_EXTENSION, RAC_TMP_FILE_PREFIX, TN_BOOLEAN, TN_CONSTRAINT_ERROR, TN_ENTRY_PRECONDITON_ERROR, TN_EXIT_EXCEPTIONAL_POSTCONDITION_ERROR, TN_EXIT_NORMAL_POSTCONDITION_ERROR, TN_INVARIANT_ERROR, TN_JMLCACHE, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_LOCATION, TN_SURROGATE, TN_VOID, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_MSG, VN_NAME, VN_OLD_VAR, VN_PARAMS, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_VALUE_SET, VN_XRESULT

Constructor Summary

InterfaceDeclarationTranslator(TypeDeclaration sourceType, CompilationUnitDeclaration sourceUnit, CompilationUnitDeclaration targetUnit)
Creates a new translator to translate the given source unit to the target unit.

Method Summary

static RacTypeDeclaration	createSurrogateClass(TypeDeclaration sourceType, CompilationResult cresult) Creates and returns a JML surrogate class for the given type using the given compilation result.
RacMethodDeclaration	createSurrogateConstructor() Creates the constructor of the surrogate class for the interface under translation.
TypeDeclaration	translate(TypeDeclaration sourceType, TypeDeclaration targetType) Translates JML assertions of sourceType to RAC code and store the RAC code to targetType.

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

needOwnRacRuntimeSupport

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

argumentsToString, argumentsToString, createImportForRacRuntimePackage, escapeString, escapeString, escapeString, getBoxedValue, getCharacterNumber, getClassType, getDeclaringClassName, getDeclaringClassName, getDefaultValue, getErrorLocation, getFullyQualifiedName, getFullyQualifiedName, getLineNumber, getRacErrorLocation, getSpecification, getUnboxedValue, getWrapperType, hasVoidReturnType, hasVoidReturnType, isGhostField, isModelField, makeMethod, makeMethod, makeMethod, parameterDeclarationToString, parameterDeclarationToString, racErrorDeclaration, racErrorDefinition, racMethodForName, racMethodsForGhostOrModel, racMethodsForSurrogate, racRuntimeMethods, throwsClauseToString, throwsClauseToString, typeName, typeName, unescapeString

Methods inherited from class java.lang.Object

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

Constructor Detail

InterfaceDeclarationTranslator

public InterfaceDeclarationTranslator(TypeDeclaration sourceType,
                                      CompilationUnitDeclaration sourceUnit,
                                      CompilationUnitDeclaration targetUnit)

Creates a new translator to translate the given source unit to the target unit.

Parameters:

sourceUnit - Compilation unit to be translated

targetUnit - Compilation unit to receive translated code

Method Detail

translate

public TypeDeclaration translate(TypeDeclaration sourceType,
                                 TypeDeclaration targetType)

Translates JML assertions of sourceType to RAC code and store the RAC code to targetType. For an interface, its RAC code is stored in its surrogate class, and the surrogate class is the last element of its member types.

Overrides:

translate in class TypeDeclarationTranslator

Parameters:

sourceType - Class to be translated to RAC code

targetType - Class to host translated RAC code

Returns:

targetType mutated to contain translated RAC code

See Also:

RacPrettyPrinter.cloneTypes(TypeDeclaration[])

createSurrogateClass

public static RacTypeDeclaration createSurrogateClass(TypeDeclaration sourceType,
                                                      CompilationResult cresult)

Creates and returns a JML surrogate class for the given type using the given compilation result.

createSurrogateConstructor

public RacMethodDeclaration createSurrogateConstructor()

Creates the constructor of the surrogate class for the interface under translation. The returned constructor has the following form:

        public JmlSurrogate(JMLCheckable self) {
    super(self);
        }