JML

org.jmlspecs.jmlrac
Class TransType

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.TransType
All Implemented Interfaces:
Cloneable, Constants, Constants, Constants, RacConstants
Direct Known Subclasses:
TransClass, TransInterface

public abstract class TransType
extends TransUtils

An abstract class for translating JML type declarations. The translation may produce (1) a set of assertion check methods and supporting fields (e.g., to hold old values) for classes, and (2) for an interface declaration, a surrogate class as a static inner class.

This class implements the Template Method Pattern [GoF94]. The main template method is translate which deines the major flow of control and calls such translation methods as:

Some methods are abstract and others are concrete. They may be refined by concrete subclasses such as TransClass and TransInterface.

(David Cok): THIS IS NOT UP TO DATE The original code (which is intact) has been embellished to handle the situation in which source code is not available to be used to generate new java code containing runtime assertion checks. This is the case, for example, in checking the assertions of classes in java.* . This situation obtains when the assertion check code is being generated from a non-.java file and the object being tested is a class, not an interface. In this case the variable genSpecTestFile is set true, and the generated code is produced as follows. (If genSpecTestFile==false, the original rewrite-the-java-file mechanism is used unchanged.)

The generated class must be different from the class under test, since it cannot replace it. We presume that we cannot add to the package of the class under test either, and in any case it is convenient to have the generated class have the same name as the class under test (convenient for generating test code). Thus we use the same class name but a different package for the generated class. For clarity, we will call the class under test class p.C and the generated class testspecs.p.C . The actual generated class name is determined by the --packageName option.

There are two subcases. One in which we generate a subclass of p.C, which is called Wrapper, and one in which we do not generate such a subclass. The variable genWrapperClass is true in the first case, false in the second.

  • genWrapperClass must be true if there are any protected methods, fields, or constructors that must be tested or are used in specifications.
  • genWrapperClass must be false if the class p.C is final
  • genWrapperClass must be false if the class p.C has only or private constructors
  • genWrapperClass must be false if the class p.C has fields that are of type p.C (e.g. BigInteger.ZERO, Double.MAX_INTEGER) because we have not implemented any mechanisms to convert a p.C object to a Wrapper object. Although straightforward for BigInteger and Double, it would need to rely on the presence of a copy constructor. Hence we just forbid a Wrapper class in this case.
  • If a protected method of p.C is final, we are stuck - we cannot test or access this method.

We generate testspecs.p.C with the following content.

  • - All methods that check specifications are members of the generated class, as they are in the case of genSpecTestFile==false, but some field or method access may be different.
  • - (genWrapperClass==true): A static public nested class named Wrapper which has p.C as a super class and with content as described in the following.
  • - A field named delegee of type p.C if genWrapperClass==false of type Wrapper if genWrapperClass==true
  • - Members of p.C with package or private access are not available and cannot be tested. If specifications need to access these members, it may not be possible to test the class.
  • - For each public method m of p.C: a public method m in testspecs.p.C is generated (even with genSpecTestFile false) that checks specifications appropriately, calling internal$m(...) as needed. When genSpecTestFile==true, internal$m is modified to call delegee.m(...)
  • - For each protected method m of p.C: [must have genWrapperClass==true] a public method m in testspecs.p.C is *generated (even with genSpecTestFile false) that checks *specifications appropriately, calling internal$m(...) as needed. *When genSpecTestFile==true, internal$m is modified to call *delegee.m(...) Also generate a public method in Wrapper with the *same name and arguments that simply calls/returns super.m(...). *Note: If there are any such protected methods of p.C, then *genWrapperClass must be true, since testspecs.p.C will not be able *to call p.C.m .
  • - For each public constructor of p.C: If (genWrapperClass==false) generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new p.C(...) as needed. If (genWrapperClass==true) generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new Wrapper(...) as needed and generate a public constructor in Wrapper with the same name and arguments that simply calls super(...)
  • - For each protected constructor of p.C: [Must have genWrapperClass==true] generate a public constructor in testspecs.p.C that checks specifications appropriately, calling new Wrapper(...) as needed. And if (genWrapperClass==true) generate a public method in Wrapper with the same name and arguments that simply calls/returns super(...) [not strictly needed for public methods of p.C].
  • - there are no public or protected constructors of p.C then genWrapperClass must be false. We then add one constructor to testspecs.p.C of the form public C(p.C o) { delegee = o; } [genWrapperClass==false] public C(Wrapper o) { delegee = o; } [genWrapperClass==true]
  • If p.C has only a default constructor, then testspecs.p.C is given a constructor with no arguments that simply sets delegee == new p.C();
  • - For each public field f of p.C: If (genWrapperClass==false) references to the field in specifications are changed to delegee.f If (genWrapperClass==true) generate a public method in Wrapper named spec$f$C that simply returns the value of the field. References to the field in specifications will call delegee.spec$f$C(). [ In this latter case, we could use delegee.f, but we do it this way to be consistent with the mechanism for protected fields.]
  • - For each protected field f of p.C: [Must have genWrapperClass==true] generate a public method in Wrapper named spec$f$C that simply returns the value of the field. Any references to the field in specifications will call delegee.spec$f$C().
  • - Creating objects for testcases. The receivers need to be of type testspecs.p.C. Other objects used as arguments should be of dynamic type Wrapper (if getWrapperClass is true) otherwise of type p.C .

Version:
$Revision: 1.74 $
Author:
Yoonsik Cheon, David Cok
See Also:
TransClass, TransInterface

Field Summary
private static CClass currentCClass
          CClass of the target type declaration.
protected static boolean dynamicInvocationMethodNeeded
          True if a dynamic invocation method need be generated for the current type declaration as the result of the translation.
static boolean genSpecTestFile
          true if we are operating on spec files
static boolean genWrapperClass
           
private  ArrayList laterMethods
           
protected  Set modelMethods
          The set of model or spec_public field names whose access methods have alredy been generated.
static boolean specInheritanceMethodNeeded
          True if a specification inheritance method need be generated for the current type declaration as the result of the translation.
protected  JmlTypeDeclaration typeDecl
          Target type declaration to be translated.
protected  VarGenerator varGen
          Variable generator for generating fresh variable names.
 
Fields inherited from class org.jmlspecs.jmlrac.TransUtils
 
Fields inherited from class org.multijava.util.Utils
DBG_LEVEL_HIGH, DBG_LEVEL_LOW, DBG_LEVEL_NO
 
Fields inherited from interface org.jmlspecs.jmlrac.RacConstants
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, TN_JMLCHECKABLE, TN_JMLSURROGATE, TN_JMLUNIT_TEST_POSTFIX, TN_JMLUNIT_TESTDATA_POSTFIX, TN_JMLVALUE, TN_SURROGATE, VN_ASSERTION, VN_CATCH_VAR, VN_CLASS_INIT, VN_CONSTRUCTED, VN_DELEGEE, VN_ERROR_SET, VN_EXCEPTION, VN_FREE_VAR, VN_INIT, VN_OLD_VAR, VN_POST_VAR, VN_PRE_VAR, VN_PRECOND, VN_RAC_COMPILED, VN_RAC_LEVEL, VN_RESULT, VN_STACK_VAR, VN_XRESULT
 
Fields inherited from interface org.jmlspecs.checker.Constants
ACC2_RAC_METHOD, ACC_CODE, ACC_CODE_BIGINT_MATH, ACC_CODE_JAVA_MATH, ACC_CODE_SAFE_MATH, ACC_GHOST, ACC_HELPER, ACC_INSTANCE, ACC_MODEL, ACC_MONITORED, ACC_QUERY, ACC_SECRET, ACC_SPEC_BIGINT_MATH, ACC_SPEC_JAVA_MATH, ACC_SPEC_PROTECTED, ACC_SPEC_PUBLIC, ACC_SPEC_SAFE_MATH, ACC_UNINITIALIZED, ACCESS_FLAG_ARRAY, ACCESS_FLAG_NAMES, AMID_BIGINT_MATH, EVERYTHING, JML_JMLObjectSet, NOT_SPECIFIED, NOTHING, OPE_BACKWARD_IMPLIES, OPE_EQUIV, OPE_EXISTS, OPE_FORALL, OPE_IMPLIES, OPE_L_ARROW, OPE_MAX, OPE_MIN, OPE_NOT_EQUIV, OPE_NUM_OF, OPE_PRODUCT, OPE_R_ARROW, OPE_SUBTYPE, OPE_SUM, SAME, TID_BIGINT, TID_REAL, TID_TYPE, TN_JMLOBJECTSET, TN_JMLTYPE, TN_JMLVALUESET
 
Fields inherited from interface org.multijava.mjc.Constants
ACC_MODIFIER_FLAGS_MASK, ACC_NON_NULL, ACC_NON_NULL_BY_DEFAULT, ACC_NULLABLE, ACC_NULLABLE_BY_DEFAULT, ACC_PURE, AMID_JAVA_MATH, AMID_MAX, AMID_SAFE_MATH, CMP_VERSION, IMPLICITLY_NON_NULL, JAV_ASSERTION_ERROR, JAV_CLASS, JAV_CLASSLOADER, JAV_CLASSNOTFOUND_EXCEPTION, JAV_CLONE, JAV_CLONEABLE, JAV_CONSTRUCTOR, JAV_ERROR, JAV_EXCEPTION, JAV_INIT, JAV_LENGTH, JAV_NAME_SEPARATOR, JAV_NOCLASSDEFFOUND_ERROR, JAV_OBJECT, JAV_OUTER_THIS, JAV_RMJ_RUNTIME_EXCEPTION, JAV_RUNTIME, JAV_RUNTIME_EXCEPTION, JAV_SERIALIZABLE, JAV_STATIC_INIT, JAV_STRING, JAV_STRINGBUFFER, JAV_SUPER, JAV_THIS, JAV_THROWABLE, MJ_ANCHOR, NULLITY_MODS, OPE_BAND, OPE_BNOT, OPE_BOR, OPE_BSR, OPE_BXOR, OPE_EQ, OPE_GE, OPE_GT, OPE_LAND, OPE_LE, OPE_LNOT, OPE_LOR, OPE_LT, OPE_MINUS, OPE_NE, OPE_PERCENT, OPE_PLUS, OPE_POSTDEC, OPE_POSTINC, OPE_PREDEC, OPE_PREINC, OPE_SIMPLE, OPE_SL, OPE_SLASH, OPE_SR, OPE_STAR, TID_ARRAY, TID_BOOLEAN, TID_BYTE, TID_CHAR, TID_CLASS, TID_DOUBLE, TID_FLOAT, TID_INT, TID_LONG, TID_MAX, TID_SHORT, TID_VOID, UNIV_ARRAY_TMP, UNIV_TMP
 
Fields inherited from interface org.multijava.util.classfile.Constants
ACC_ABSTRACT, ACC_FINAL, ACC_INTERFACE, ACC_NATIVE, ACC_PRIVATE, ACC_PROTECTED, ACC_PUBLIC, ACC_STATIC, ACC_STRICT, ACC_SUPER, ACC_SYNCHRONIZED, ACC_SYNTHETIC, ACC_TRANSIENT, ACC_VOLATILE, ATT_ANCHOR, ATT_BRIDGE, ATT_CODE, ATT_CONSTANTVALUE, ATT_DEPRECATED, ATT_DISPATCHER, ATT_EXCEPTIONS, ATT_GENERIC, ATT_GENERIC_FUNCTIONS, ATT_INNERCLASSES, ATT_LINENUMBERTABLE, ATT_LOCALVARIABLETABLE, ATT_MM_BODY, ATT_REDIRECTOR, ATT_RMJ_GLUE, ATT_RMJ_SIGNATURE, ATT_RUNTIME_VISIBLE_ANNOTATIONS, ATT_RUNTIME_VISIBLE_PARAMETER_ANNOTATIONS, ATT_SIGNATURE, ATT_SOURCEFILE, ATT_SYNTHETIC, ATT_UNIVERSE_FIELD, ATT_UNIVERSE_METHOD, ATT_UNIVERSE_VERSION, CST_CLASS, CST_DOUBLE, CST_FIELD, CST_FLOAT, CST_INTEGER, CST_INTERFACEMETHOD, CST_LONG, CST_METHOD, CST_NAMEANDTYPE, CST_STRING, CST_UTF8, ENV_DEBUG_MODE, ENV_USE_CACHE, JAVA_MAGIC, JAVA_MAJOR, JAVA_MINOR, MAX_CODE_PER_METHOD, opc_aaload, opc_aastore, opc_aconst_null, opc_aload, opc_aload_0, opc_aload_1, opc_aload_2, opc_aload_3, opc_anewarray, opc_areturn, opc_arraylength, opc_astore, opc_astore_0, opc_astore_1, opc_astore_2, opc_astore_3, opc_athrow, opc_baload, opc_bastore, opc_bipush, opc_caload, opc_castore, opc_checkcast, opc_d2f, opc_d2i, opc_d2l, opc_dadd, opc_daload, opc_dastore, opc_dcmpg, opc_dcmpl, opc_dconst_0, opc_dconst_1, opc_ddiv, opc_dload, opc_dload_0, opc_dload_1, opc_dload_2, opc_dload_3, opc_dmul, opc_dneg, opc_drem, opc_dreturn, opc_dstore, opc_dstore_0, opc_dstore_1, opc_dstore_2, opc_dstore_3, opc_dsub, opc_dup, opc_dup2, opc_dup2_x1, opc_dup2_x2, opc_dup_x1, opc_dup_x2, opc_f2d, opc_f2i, opc_f2l, opc_fadd, opc_faload, opc_fastore, opc_fcmpg, opc_fcmpl, opc_fconst_0, opc_fconst_1, opc_fconst_2, opc_fdiv, opc_fload, opc_fload_0, opc_fload_1, opc_fload_2, opc_fload_3, opc_fmul, opc_fneg, opc_frem, opc_freturn, opc_fstore, opc_fstore_0, opc_fstore_1, opc_fstore_2, opc_fstore_3, opc_fsub, opc_getfield, opc_getstatic, opc_goto, opc_goto_w, opc_i2b, opc_i2c, opc_i2d, opc_i2f, opc_i2l, opc_i2s, opc_iadd, opc_iaload, opc_iand, opc_iastore, opc_iconst_0, opc_iconst_1, opc_iconst_2, opc_iconst_3, opc_iconst_4, opc_iconst_5, opc_iconst_m1, opc_idiv, opc_if_acmpeq, opc_if_acmpne, opc_if_icmpeq, opc_if_icmpge, opc_if_icmpgt, opc_if_icmple, opc_if_icmplt, opc_if_icmpne, opc_ifeq, opc_ifge, opc_ifgt, opc_ifle, opc_iflt, opc_ifne, opc_ifnonnull, opc_ifnull, opc_iinc, opc_iload, opc_iload_0, opc_iload_1, opc_iload_2, opc_iload_3, opc_imul, opc_ineg, opc_instanceof, opc_invokeinterface, opc_invokespecial, opc_invokestatic, opc_invokevirtual, opc_ior, opc_irem, opc_ireturn, opc_ishl, opc_ishr, opc_istore, opc_istore_0, opc_istore_1, opc_istore_2, opc_istore_3, opc_isub, opc_iushr, opc_ixor, opc_jsr, opc_jsr_w, opc_l2d, opc_l2f, opc_l2i, opc_ladd, opc_laload, opc_land, opc_lastore, opc_lcmp, opc_lconst_0, opc_lconst_1, opc_ldc, opc_ldc2_w, opc_ldc_w, opc_ldiv, opc_lload, opc_lload_0, opc_lload_1, opc_lload_2, opc_lload_3, opc_lmul, opc_lneg, opc_lookupswitch, opc_lor, opc_lrem, opc_lreturn, opc_lshl, opc_lshr, opc_lstore, opc_lstore_0, opc_lstore_1, opc_lstore_2, opc_lstore_3, opc_lsub, opc_lushr, opc_lxor, opc_monitorenter, opc_monitorexit, opc_multianewarray, opc_new, opc_newarray, opc_nop, opc_pop, opc_pop2, opc_putfield, opc_putstatic, opc_ret, opc_return, opc_saload, opc_sastore, opc_sipush, opc_swap, opc_tableswitch, opc_wide, opc_xxxunusedxxx, POO_ASCII_CONSTANT, POO_CLASS_CONSTANT, POO_DOUBLE_CONSTANT, POO_FLOAT_CONSTANT, POO_INTEGER_CONSTANT, POO_LONG_CONSTANT, POO_NAT_CONSTANT, POO_REF_CONSTANT, POO_STRING_CONSTANT, TYP_ADDRESS, TYP_DOUBLE, TYP_FLOAT, TYP_INT, TYP_LONG, TYP_REFERENCE, TYP_VOID
 
Constructor Summary
protected TransType(JmlTypeDeclaration typeDecl)
          Constructs a TransType object.
 
Method Summary
protected abstract  void addNewMethod(JmlMethodDeclaration mdecl)
          Adds a new method declaration, mdecl, to the instrumented type.
static boolean dynamicCallNeeded(CClass clazz)
          Returns true if dynamic calls are needed to access model, ghost, spec_public, and spec_protected fields declared in the given class clazz.
protected  JmlMethodDeclaration dynamicInvocationMethod()
          Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility.
protected  void finalizeTranslation()
          Finalizes translation of the type declaration.
protected  JmlTypeDeclaration findTypeWithRepresentsFor(JmlTypeDeclaration tdecl, CField field)
          Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration.
protected  JmlMethodDeclaration forNameMethod()
          Returns a method declaration that returns the class object associated with the class or interface with the given string name.
protected  JmlMethodDeclaration ghostFieldAccessors(JmlFieldDeclaration fdecl)
          Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
static String ident()
          Returns the identifier of the type currently being tranlated.
protected  JmlMethodDeclaration initFlags()
          Returns declarations of class/instance initialization flags.
protected  boolean isAccessorGenerated(CField field)
          Returns true if an accessor (or a delegation method) is already generated for a model or spec_public field, field.
static boolean isInterface()
          Returns true if the currently tranlated type is an interface.
private static boolean isRepresentsDeclExecutable(JmlRepresentsDecl rdecl)
          Returns true if the given represents declaration is translatable.
private  JmlMethodDeclaration modelFieldAccessor(JmlSourceField field, JExpression expr)
          Returns a model accessor method for a model field with the given expression (of the represents clause).
 void postTranslationChangesForSpecTestFile(String wrapperClass)
           
private  void prepareSpecTestFile()
           
protected abstract  String receiver(String className, String clazz, String receiver)
          Returns a string form of code that, if executed, returns the receiver of for a dynamic call.
protected  void setAccessorGenerated(CField field)
          Indicates that an accessor (or a delegation method) has been generated for a model or spec_public field, field.
 void translate()
          Translates the given type declaration.
protected  void translateBody(ArrayList inners, ArrayList methods, JPhylum[] fieldsAndInits)
          Translates a class body, either of class or interface.
protected abstract  void translateConstraint()
          Translates history constraints, both static and non-static.
protected  JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)
          Translates a JML field declaration, fieldDecl.
 String translateForSpecTestFile()
           
protected abstract  void translateInvariant()
          Translates invariants, both static and non-static invariants.
protected abstract  void translateMethod(JmlMethodDeclaration mdecl)
          Translates a JML method declaration.
protected  void translateModelMethod(JmlMethodDeclaration mdecl)
          Translates the given model method (or constructor), mdecl. !
protected  void translateRepresents(JmlRepresentsDecl[] repDecls)
          Translates represents clauses of this type declaration.
private  String unwrap(CType t, String val)
           
private  String wrap(CType t, String val)
           
 
Methods inherited from class org.jmlspecs.jmlrac.TransUtils
applyBigintBinOperator, applyBigintCast, applyBigintToNumber, applyBigintUnOperator, applyUnaryPromoteExpression, beingTested, createBigintConvertionAssertion, defaultValue, dynamicCallName, evalOldName, evalOldName, evalOldName, evalOldName, excludedFromInheritance, getTypeID, initIncludedInInheritance, invariantLikeName, isBigintArray, isMain, modelPublicAccessorName, numberToBigint, specAccessorNeeded, specPublicAccessorName, subtypeConstraintName, toPrintableString, toString, toString, toString, typeToClass, unwrapObject, useReflection, wrappedValue, wrapValue
 
Methods inherited from class org.multijava.util.Utils
assertTrue, assertTrue, combineArrays, escapeString, escapeString, fail, fail, getFilePath, hasFlag, hasOtherFlags, parsePathParts, relativePathTo, splitQualifiedName, splitQualifiedName, stripJavaModifiers, stripNonJavaModifiers, stripPrivateModifier, unescapeString, vectorToArray, vectorToIntArray
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

genSpecTestFile

public static boolean genSpecTestFile
true if we are operating on spec files


genWrapperClass

public static boolean genWrapperClass

laterMethods

private ArrayList laterMethods

typeDecl

protected JmlTypeDeclaration typeDecl
Target type declaration to be translated.

 protected invariant typeDecl.getCClass() == currentCClass;
 


varGen

protected VarGenerator varGen
Variable generator for generating fresh variable names.


currentCClass

private static CClass currentCClass
CClass of the target type declaration.


dynamicInvocationMethodNeeded

protected static boolean dynamicInvocationMethodNeeded
True if a dynamic invocation method need be generated for the current type declaration as the result of the translation.

See Also:
dynamicInvocationMethod()

specInheritanceMethodNeeded

public static boolean specInheritanceMethodNeeded
True if a specification inheritance method need be generated for the current type declaration as the result of the translation.

See Also:
TransExpression#visitJmlInvariantForExpression()

modelMethods

protected Set modelMethods
The set of model or spec_public field names whose access methods have alredy been generated.

See Also:
translateRepresents(JmlRepresentsDecl[]), translateField(JmlFieldDeclaration)
Constructor Detail

TransType

protected TransType(JmlTypeDeclaration typeDecl)
Constructs a TransType object.

Parameters:
typeDecl - target type declaration to be translated

 requires typeDecl != null;
 
Method Detail

prepareSpecTestFile

private void prepareSpecTestFile()

translate

public void translate()
Translates the given type declaration. The translation may produce a collection of assertion check methods.


translateInvariant

protected abstract void translateInvariant()
Translates invariants, both static and non-static invariants. This method must be implemented by concrete subclasses.


translateConstraint

protected abstract void translateConstraint()
Translates history constraints, both static and non-static. This method must be implemented by concrete subclasses.


translateForSpecTestFile

public String translateForSpecTestFile()

wrap

private String wrap(CType t,
                    String val)

unwrap

private String unwrap(CType t,
                      String val)

postTranslationChangesForSpecTestFile

public void postTranslationChangesForSpecTestFile(String wrapperClass)

translateRepresents

protected void translateRepresents(JmlRepresentsDecl[] repDecls)
Translates represents clauses of this type declaration. For each executable (i.e., functinal abstraction) form of represents clause, this method generates a model field accessor method that calculates the value of the model field in terms of the represents clause's expression. The accessor method has the following general form:
 [[represents m <- E;]] ==
   protected T m() {
     T v = T_init;
     [[E, v]]
     return v;
   }
 
where T is the type of expression E and v is a unique local variable. The generated method declaration is added to the current type (or surrogate class if the type is an interface), and the field is marked that its model access method is generated.

 requires repDecls != null;
 

See Also:
translateField(JmlFieldDeclaration), addNewMethod(JmlMethodDeclaration), setAccessorGenerated(CField)

finalizeTranslation

protected void finalizeTranslation()
Finalizes translation of the type declaration. This method may be overridden by subclasses to do subclass-specific finalization such as generation of specification inheritance mechanism (i.e., inheritance method, surrogate class, etc.). However, this method method must be called at the end to do the common finalization such as adding class/instance initialization flags.


translateBody

protected void translateBody(ArrayList inners,
                             ArrayList methods,
                             JPhylum[] fieldsAndInits)
Translates a class body, either of class or interface.

Parameters:
inners - inner classes
methods - mthod declarations
fieldsAndInits - field declarations

 requires inners != null && methods != null && fieldsAndInits != null;
 

translateField

protected JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)
Translates a JML field declaration, fieldDecl. This method strips off the final modifier from the field declaration. If necessary, this method should be overwritten by subclasses to specially handle final, model, model, spec_public, and spec_protected fields.

 requires fieldDecl != null;
 modifies fieldDecl.*;
 ensures \result != null && \result == fieldDecl;
 


translateModelMethod

protected void translateModelMethod(JmlMethodDeclaration mdecl)
Translates the given model method (or constructor), mdecl. !FIXME!describe translation rules.


translateMethod

protected abstract void translateMethod(JmlMethodDeclaration mdecl)
Translates a JML method declaration. A translation of JML method declaration produces four new methods, and the original method is renamed and made private-accessible:

  • Precondition checking method. A protected method to check the precondition of the original method (refer to the class PreconditionMethod).
  • Normal and exceptional postcondition checking methods. A couple of protected methods to check the normal and exceptional postconditions of the original method (refer to the classes PostconditionMethod and ExceptionalPostconditionMethod).
  • Wrapper method. A wrapper method that wraps the original method with pre and postcondition checking (refer to the class WappersMethod).

    The translation also generate several new instance fields to store temporally values used by the assertion checking methods. There are three kinds of variables that are generated and declared as instance fields.

    • Precondition variables.
    • Old (\old) expression variables.
    • Specification variables.
  • Similarly, translation of JML constructor declaration also produces four new methods, and the original constructor becomes a wrapper method (refer to the class TransConstructor).

    
     requires mdecl != null;
     


ghostFieldAccessors

protected JmlMethodDeclaration ghostFieldAccessors(JmlFieldDeclaration fdecl)
Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration. The name of both accessors is MN_GHOST + ident + "$" + className, where the constant MN_GHOST is usually "ghost$" and ident is the name of the ghost field. The accessor methods has the following general structure:
  public [static] T ghost$v$C() {
     return v;
  } 
  public [static] void ghost$v$C(T x) {
     v = x;
  } 
 
This method also generates a private field for storing ghost values and possibly an initializer block too. They are stored in the given field declaration for later pretty-printing (see RacPrettyPrinter.visitJmlFieldDeclaration).
  private [static] T v;
  [static] {
     v = initializer;
  }
 

 requires fdecl != null && hasFlag(fdecl.modifiers(), ACC_GHOST);
 modifies fdecl.*;
 ensures \result != null;
 


initFlags

protected JmlMethodDeclaration initFlags()
Returns declarations of class/instance initialization flags. The initialization flags indicate if classes/instances have finished their initializations, and are used to prevent invariant checks from happening during initialization.


addNewMethod

protected abstract void addNewMethod(JmlMethodDeclaration mdecl)
Adds a new method declaration, mdecl, to the instrumented type.


modelFieldAccessor

private JmlMethodDeclaration modelFieldAccessor(JmlSourceField field,
                                                JExpression expr)
Returns a model accessor method for a model field with the given expression (of the represents clause).

Parameters:
field - model field
expr - the right hand side of the represents clause (e.g., E in m <- E.

 requires field != null && field.isModel() && expr != null;
 ensures \result != null;
 

findTypeWithRepresentsFor

protected JmlTypeDeclaration findTypeWithRepresentsFor(JmlTypeDeclaration tdecl,
                                                       CField field)
Finds the applicable representsclause for a given model field by searching through the superclass and interface hierachies starting from the given type declaration. If such a clause is found, returns the type declaration that includes the clause; otherwise, returns null.

 requires tdecl != null && 
   field != null && hasFlag(field.modifiers(),ACC_MODEL);
 ensures \result != null ==> (* \result has represents clause  r 
   such that !r.isRedundantly() && r.usesAbstractionFunction() && 
   r.storeRef() refers to field *);
 


isRepresentsDeclExecutable

private static boolean isRepresentsDeclExecutable(JmlRepresentsDecl rdecl)
Returns true if the given represents declaration is translatable. A represents declaration is translatable if the following conditions are satisfied:

  • It is not redundant.
  • It uses a functional abstraction; i.e., it is of the form: x <- E).


 requires rdecl != null;
 


dynamicInvocationMethod

protected JmlMethodDeclaration dynamicInvocationMethod()
Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility. The target method is specified by its name, its owner's class name, formal parameter types, and actual arguments. The target method is typically an access method generated by the runtime assertion checker, such as an accessor for a model, ghost, spec_public, or spec_protected field, a setter for a ghost field, and an accessor for a spec_public or spec_protected method. The return value is that of the target method, if necessary, wrapped in an object. If the target method is not found, a instance of JMLNonExecutableException is thrown. If the target method throws a RuntimeException, including JMLNonExecutableException, the exception is rethrown; for other types of exceptions, an instanceof RuntimeException is thrown.

 ensures \result != null;
 


forNameMethod

protected JmlMethodDeclaration forNameMethod()
Returns a method declaration that returns the class object associated with the class or interface with the given string name.

 ensures \result != null;
 


receiver

protected abstract String receiver(String className,
                                   String clazz,
                                   String receiver)
Returns a string form of code that, if executed, returns the receiver of for a dynamic call. This method is used by the method dynamicInvocationMethod to define a subclass-specific dynamic invocation method.

See Also:
dynamicInvocationMethod()

isAccessorGenerated

protected boolean isAccessorGenerated(CField field)
Returns true if an accessor (or a delegation method) is already generated for a model or spec_public field, field.


setAccessorGenerated

protected void setAccessorGenerated(CField field)
Indicates that an accessor (or a delegation method) has been generated for a model or spec_public field, field.


dynamicCallNeeded

public static boolean dynamicCallNeeded(CClass clazz)
Returns true if dynamic calls are needed to access model, ghost, spec_public, and spec_protected fields declared in the given class clazz. The return value is true if the given class is not the same as the one being translated now.


isInterface

public static boolean isInterface()
Returns true if the currently tranlated type is an interface.


ident

public static String ident()
Returns the identifier of the type currently being tranlated.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.