org.jmlspecs.jml4.rac
Class ConstructorHeaderTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.RacTranslator
      org.jmlspecs.jml4.rac.MethodHeaderTranslator
          org.jmlspecs.jml4.rac.ConstructorHeaderTranslator

All Implemented Interfaces:

RacConstants

public abstract class ConstructorHeaderTranslator
extends MethodHeaderTranslator

Translates a constructor header along with its specification to a set of RAC methods.

Author:

Amritam Sarcar 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

Method Summary

static ConstructorHeaderTranslator	forClass()
static ConstructorHeaderTranslator	forInterface()

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

createInternalMethod, createInternalMethod, createWrapperMethod, forInterface

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

Method Detail

forClass

public static ConstructorHeaderTranslator forClass()

forInterface

public static ConstructorHeaderTranslator forInterface()