org.jmlspecs.jmlrac
Class TransInterface

java.lang.Object
  org.multijava.util.Utils
      org.jmlspecs.jmlrac.TransUtils
          org.jmlspecs.jmlrac.TransType
              org.jmlspecs.jmlrac.TransInterface

All Implemented Interfaces:

Cloneable, Constants, Constants, Constants, RacConstants

public class TransInterface

extends TransType

A class for translating JML interface declarations. The translation produces an inner class in the interface, called a surrogate class. The surrogate class takes the responsibility of checking assertions of the interface and thus defines all the assertion check methods for the interface. This class supports the Template Method Pattern laid out by the abstract superclass TransType.

Version:

$Revision: 1.48 $

Author:

Yoonsik Cheon

Field Summary
private  RacNode	hcMethod           History constraint check methods for the current interface.
private  JmlInterfaceDeclaration	interfaceDecl           Target interface to be translated.
private  RacNode	invMethod           Invariant check methods for the current interface.
private  List	newFields           New field declarations to be added to the surrogate class.
private  List	newMethods           New mehtod declarations to be added to the surrogate class.
private static TokenReference	NO_REF           Null token reference.

 

Fields inherited from class org.jmlspecs.jmlrac.TransType

dynamicInvocationMethodNeeded, genSpecTestFile, genWrapperClass, modelMethods, specInheritanceMethodNeeded, typeDecl, varGen

 

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

TransInterface(JmlInterfaceDeclaration interfaceDecl)           Construct a TransInterface object.

 

Method Summary
protected  void	addNewMethod(JmlMethodDeclaration mdecl)           Adds a new method declaration, mdecl, to the surrogate class to be generated in the finalization step of this translation.
protected  JmlMethodDeclaration	assertionInheritanceMethod()           Returns a method declaration implementing dynamic inheritance using the Java's reflection facility.
private  JmlMethodDeclaration	concreteMethod(CMethod mdecl)           Returns a concrete (delegation) method that implements the abstract method declaration, mdecl.
private  RacNode	concreteMethods()           Returns concrete method declarations, often called delegation methods, that implements the abstract methods declared in the interface (and its super-interfaces).
private  JmlMethodDeclaration	defaultModelFieldAccessor(CField field)           Returns a default accessor method for a model field, field.
protected  void	finalizeTranslation()           Finalizes the translation of this interface.
private  void	genSurrogateClass(RacNode newFdecls, RacNode newMdecls)           Generates a surrogate class for the interface declaration being translated.
protected  JmlMethodDeclaration	ghostFieldAccessors(JmlFieldDeclaration fdecl)           Returns a pair of ghost field accessor methods (getter and setter) for the given ghost field declaration.
protected  String	receiver(String clsName, String clazz, String receiver)           Returns a string form of code that, if executed, returns the receiver of for a dynamic call.
private  JmlMethodDeclaration	specPublicMethodAccessor(JmlMethodDeclaration mdecl)           Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
protected  String	surrogatePlaceHolders(RacNode newFdecls, RacNode newMdecls, RacNode mdecls)           Returns a place holder string ($0...
protected  Object[]	surrogatePlaceValues(RacNode newFdecls, RacNode newMdecls, RacNode mdecls)           Returns an array of objects representing actual values for the place holder.
protected  void	translateConstraint()           Translates constraint clauses of this interface declaration.
protected  JmlFieldDeclaration	translateField(JmlFieldDeclaration fieldDecl)           Translates the given JML field declaration, fieldDecl, by specially handling final, model, model, spec_public, and spec_protected fields.
protected  void	translateInvariant()           Translates invariant clauses of this interface declaration.
protected  void	translateMethod(JmlMethodDeclaration mdecl)           Translates a JML method declaration.
protected  void	translateModelMethod(JmlMethodDeclaration mdecl)           Translates the given model method (or constructor), mdecl. !

 

Methods inherited from class org.jmlspecs.jmlrac.TransType

dynamicCallNeeded, dynamicInvocationMethod, findTypeWithRepresentsFor, forNameMethod, ident, initFlags, isAccessorGenerated, isInterface, postTranslationChangesForSpecTestFile, setAccessorGenerated, translate, translateBody, translateForSpecTestFile, translateRepresents

 

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

interfaceDecl

private JmlInterfaceDeclaration interfaceDecl

Target interface to be translated.

 private invariant interfaceDecl == (JmlInterfaceDeclaration)typeDecl;
 

newMethods

private List newMethods

New mehtod declarations to be added to the surrogate class.

newFields

private List newFields

New field declarations to be added to the surrogate class.

invMethod

private RacNode invMethod

Invariant check methods for the current interface.

hcMethod

private RacNode hcMethod

History constraint check methods for the current interface.

NO_REF

private static final TokenReference NO_REF

Null token reference.

TransInterface

public TransInterface(JmlInterfaceDeclaration interfaceDecl)

Construct a TransInterface object.

Parameters:

interfaceDecl - target interface declaration to be translated

translateInvariant

protected void translateInvariant()

Translates invariant clauses of this interface declaration. This method produces a couple of invariant check methods, one for the static invariants and the other for instance invariants.

 also
   modifies invMethod;
 

translateConstraint

protected void translateConstraint()

Translates constraint clauses of this interface declaration. This method produces a couple of constraint check methods, one for the static constraints and the other for instance constraints.

 also
   modifies hcMethod;
 

translateField

protected JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)

Translates the given JML field declaration, fieldDecl, by specially handling final, model, model, spec_public, and spec_protected fields.

If this is a model field and has no accessor method generated yet (i.e., by represents clauses), generates the following form of default model accessor method:

 [[... model T m ...;]] ==
   protected T m() {
     throw new JMLNonExecutableException();
   }
 

If the given declaration is a ghost field declaration, generates a pair of ghost field accessor methods (getter and setter), a private field for storing ghost values, and possibly an initialization block. The generated code has the following structure:

  private [static] T v;
  [static] {
     v = initializer;
  }
  public [static] T ghost$v$C() {
     return v;
  } 
  public [static] void ghost$v$C(T x) {
     v = x;
  } 
 

The generated code is added to the surrogate class.

 also
   requires fieldDecl != null;
   modifies modelMethods, interfaceDecl, newMethods;
 

Overrides:

translateField in class TransType

See Also:

#translateRepresents(JmlRepresentsDecl[]), ghostFieldAccessors(JmlFieldDeclaration), #modelMethods

translateMethod

protected 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.
  • Pre (\pre) expression 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).

 also
   requires mdecl != null;
   modifies newMethods, newFields;
 

translateModelMethod

protected void translateModelMethod(JmlMethodDeclaration mdecl)

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

Overrides:

translateModelMethod in class TransType

specPublicMethodAccessor

private JmlMethodDeclaration specPublicMethodAccessor(JmlMethodDeclaration mdecl)

Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl. The returned method has the following code structure.

 public [static] T specPublic$m(x1, ..., xn) {
   [return] m(x1, ..., xn);
 }
 

 requires mdecl.isSpecPublic() || mdecl.isSpecPublic();
 

finalizeTranslation

protected void finalizeTranslation()

Finalizes the translation of this interface. This method generates a surrogate class as an inner class of this interface.

 also
   modifies interfaceDecl, newMethods;
 

Overrides:

finalizeTranslation in class TransType

genSurrogateClass

private void genSurrogateClass(RacNode newFdecls,
                               RacNode newMdecls)

Generates a surrogate class for the interface declaration being translated. The generated surrogate class is added to the interface as a new member declaration. The surrogate class is responsible for checking assertions specified in the interface declaration, and thus declares all the assertion check methods for the interface. The surrogate class itself also implements the interface by delegating methods calls to implementing classes. Thus, (pure) method calls appearing in interface assertions are properly evaluated and checked by the implementing classes. The surrogate class is declared as a static inner class of the interface. The surrogate class has the following general structure.

 public class JmlSurrogate implements I, JMLSurrogate {
   public JmlSurrogate(JMLCheckeble self) {
     super(self);
   }
   public T1 m1(...) {
     try {
       return self.m1(...);
     }
     catch (java.lang.Throwable e) {
       throw new java.lang.RuntimeException();
     }
   }
   ...
   public Tn mn(...) {
     ...
   }
   private JMLCheckable self;
 }
 

where I is the name of the interface being translated. The interface JMLSurrogate defines properties that all surrogate classes have to implement, and the interface JMLCheckable defines properties for implementing classes. Both interfaces together define the minimal protocol for the surrogate class and the implementing class to communicate with each other for dynamic delegation.

  modifies interfaceDecl;
 

Parameters:

newFdecls - field declarations to be added to the surrogate class. It may be null.

newMdecls - method declarations (e.g., assertion check methods) to be added to the surrogate class. It may be null.

surrogatePlaceHolders

protected String surrogatePlaceHolders(RacNode newFdecls,
                                       RacNode newMdecls,
                                       RacNode mdecls)

Returns a place holder string ($0...$n) for fields and methods of the surrogate class.

See Also:

surrogatePlaceValues(RacNode, RacNode, RacNode)

surrogatePlaceValues

protected Object[] surrogatePlaceValues(RacNode newFdecls,
                                        RacNode newMdecls,
                                        RacNode mdecls)

Returns an array of objects representing actual values for the place holder.

See Also:

surrogatePlaceHolders(RacNode, RacNode, RacNode)

concreteMethods

private RacNode concreteMethods()

Returns concrete method declarations, often called delegation methods, that implements the abstract methods declared in the interface (and its super-interfaces). The returned methods delegate calls to the corresponding methods in the implementing class. If there is no method declared in the interface, this method returns null as the result. Refer to the method concreteMethod for the general structure of the delegation method.

See Also:

concreteMethod(CMethod), genSurrogateClass(RacNode, RacNode)

concreteMethod

private JmlMethodDeclaration concreteMethod(CMethod mdecl)

Returns a concrete (delegation) method that implements the abstract method declaration, mdecl. The returned method delegates calls to the corresponding method in the implementing class. The general structure of the delegation method is as follows.

 public T1 m1(...) {
   try {
     return self.m1(...);
   }
   catch (java.lang.Throwable e) {
     throw new java.lang.RuntimeException();
   }
 }
 

Since delegation methods are called only for evaluating interface assertions, all exceptions are caught and re-thrown as RuntimeException.

See Also:

concreteMethod(CMethod),

 requires mdecl != null;
 ensures \result != null;
 

defaultModelFieldAccessor

private JmlMethodDeclaration defaultModelFieldAccessor(CField field)

Returns a default accessor method for a model field, field. A default model field access method performs a dynamic call to the corresponding model field access method of the implementing class and has the following form:

  public [static] T model$n() {
    String cn = self.getClass().getName();
    Object obj = rac$invoke(cn, self, "model$n", null, null);
    return unwrapObject(T, obj);
  }
 

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.

  private [static] T v;
  [static] {
     v = initializer;
  }
 

This method is overwritten here to combine code for accessors and the new private field declaration and return it as a single object. In the overwritten method, the new field declaration is piggybacked in the given field declaration for later pretty-printing (see RacPrettyPrinter.visitJmlFieldDeclaration).

Overrides:

ghostFieldAccessors in class TransType

See Also:

TransType.ghostFieldAccessors(JmlFieldDeclaration)

addNewMethod

protected void addNewMethod(JmlMethodDeclaration mdecl)

Adds a new method declaration, mdecl, to the surrogate class to be generated in the finalization step of this translation.

receiver

protected String receiver(String clsName,
                          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.

 also
   ensures \result.equals(TN_JMLSURROGATE + ".getReceiver(" +
                          clazz + ", " + receiver + ")");
 

See Also:

TransType.dynamicInvocationMethod()

assertionInheritanceMethod

protected JmlMethodDeclaration assertionInheritanceMethod()

Returns a method declaration implementing dynamic inheritance using the Java's reflection facility. The returned method is often called an inheritance method. The inheritance method makes dynamic invocations to assertion check methods, given an assertion check method's class name, method name, formal parameter types, and actual arguments. If the target assertion check method returns a boolean value, that value is returned; otherwise, true is returned. An exception thrown by the targe method is transparently propagated to the caller.

 ensures \result != null;