JML

org.jmlspecs.jmlrac
Class TransClass

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

public class TransClass
extends TransType

A class for translating JML class declarations. The translation produces a set of assertion check methods for the class and any necessary fields, e.g., to hold old values. This class implements the Template Method Pattern layed out by the abstract superclass TransType.

Version:
$Revision: 1.77 $
Author:
Yoonsik Cheon

Field Summary
private  JmlClassDeclaration classDecl
          Target class declaration to be translated.
private  boolean surrogateCacheNeeded
          True if a cache for interface surrogates need be generated for the current class being translated.
 
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
TransClass(JmlClassDeclaration classDecl)
          Constructs a TransClass object.
 
Method Summary
protected  void addNewMethod(JmlMethodDeclaration mdecl)
          Adds a new method declaration, mdecl, to the instrumented class.
protected  JmlMethodDeclaration assertionInheritanceMethod()
          Returns a method declaration implementing dynamic inheritance using the Java's reflection facility.
protected  JmlMethodDeclaration constructionStatusAccessor()
          Returns declarations of a private instance field and a protected access method for storing and accessing the status of an instance construction.
protected  TransMethod createMethodTranslator(JmlMethodDeclaration mdecl)
          Creates a method translator for the given method declaration.
private  JmlConstructorDeclaration defaultConstructor()
          Returns a default constructor for the target class declaration.
private  JmlMethodDeclaration defaultModelFieldAccessor(CField field)
          Returns a default accessor method for a model field.
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()
          Performs a finialization of translation, e.g., generation of spec inheritance mechanism.
private  boolean generateAccessorsForInterfaceModelFields()
          Generates access methods for all the model fields inherited from the interfaces of this class.
private  JFieldDeclarationType[] interfaceModelFields()
          Returns all model fields inherited from the interfaces of this class, but excluding those also inherited from the superclass chain.
private  JmlMethodDeclaration modelFieldDelegationMethod(CField field, JmlTypeDeclaration tdecl)
          Returns a model field delegation method for model field, field, whose represents clause is found in type tdecl.
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.
protected  JmlMethodDeclaration specPublicAccessor(CField field)
          Returns a default access method for a spec_public field.
private  JmlMethodDeclaration specPublicConstructorAccessor(JmlConstructorDeclaration mdecl)
          Returns an access method for the given spec_public (or spec_protected) constructor declaration.
private  JmlMethodDeclaration specPublicMethodAccessor(JmlMethodDeclaration mdecl)
          Returns an access method for the given spec_public (or spec_protected) method declaration, mdecl.
protected  JmlMethodDeclaration staticInvariantCheckInitializer()
          Returns a static initializer that checks whether static invariants are established by the initialization of this class.
protected  JmlMethodDeclaration surrogateCacheDeclaration()
          Returns a field declaration for an interface surroagte cache with a cache lookup method and a cache update method.
private  Set toSet(JFieldDeclarationType[] fdecls)
          Returns a set containing elements from the given array.
protected  void translateBody(ArrayList inners, ArrayList methods, JPhylum[] fieldsAndInits)
          Translates a class body of the target class declaration.
protected  void translateConstraint()
          Translates constraint clauses of the target class.
protected  JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)
          Translates a JML field declaration, fieldDecl, e.g., handling final, model, spec_public, and spec_protected.
protected  void translateInvariant()
          Translates invariant clauses of this class 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, findTypeWithRepresentsFor, forNameMethod, ghostFieldAccessors, ident, initFlags, isAccessorGenerated, isInterface, postTranslationChangesForSpecTestFile, setAccessorGenerated, translate, 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

classDecl

private final JmlClassDeclaration classDecl
Target class declaration to be translated.

 private invariant classDecl == (JmlClassDeclaration)typeDecl;
 


surrogateCacheNeeded

private boolean surrogateCacheNeeded
True if a cache for interface surrogates need be generated for the current class being translated.

 private invariant dynamicInvocationMethodNeeded 
                     ==> surrogateCacheNeeded;
 

See Also:
dynamicInvocationMethod(), surrogateCacheDeclaration()
Constructor Detail

TransClass

public TransClass(JmlClassDeclaration classDecl)
Constructs a TransClass object.

Parameters:
classDecl - target class declaration to be translated
Method Detail

translateField

protected JmlFieldDeclaration translateField(JmlFieldDeclaration fieldDecl)
Translates a JML field declaration, fieldDecl, e.g., handling final, model, spec_public, and spec_protected.

If this is a model field and it has no accessor method generated by represents clauses, generate the following form of default model accessor method:

 [[... model T m ...;]] ==
   protected T m() {
     throw new JMLNonExecutableException();
   }
 
The generated method declaration is added to the current class, classDecl and its name is added to the field modelMethods.

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 accessors are added to the current class declaration, and the new field declaration (with its initialization block) is stored into the input field declaration for later pretty-printing in the proper order.

 also
   requires fieldDecl != null;
   modifies modelMethods, classDecl.*;
 

Overrides:
translateField in class TransType
See Also:
#translateRepresents(JmlRepresentsDecl[]), #modelMethods

translateInvariant

protected void translateInvariant()
Translates invariant clauses of this class declaration. This method produces a couple of invariant check methods, one for the static invariants and the other for instance invariants.

 also
   modifies classDecl.*;
 


translateConstraint

protected void translateConstraint()
Translates constraint clauses of the target class. This method produces constraint check methods, old expression evaluation methods, and old expression fields, to be added to the translated class.

 also
   assignable classDecl.*;
 

See Also:
TransConstraint

translateBody

protected void translateBody(ArrayList inners,
                             ArrayList methods,
                             JPhylum[] fieldsAndInits)
Translates a class body of the target class declaration. This method is overridden here to generate a default constructor with assertion checking capability if the class has no constructor.

Overrides:
translateBody in class TransType
Parameters:
inners - inner classes
methods - mthod declarations
fieldsAndInits - field declarations

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

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:


createMethodTranslator

protected TransMethod createMethodTranslator(JmlMethodDeclaration mdecl)
Creates a method translator for the given method declaration.


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();
 


specPublicConstructorAccessor

private JmlMethodDeclaration specPublicConstructorAccessor(JmlConstructorDeclaration mdecl)
Returns an access method for the given spec_public (or spec_protected) constructor declaration. The returned method has the following code structure.
 public static T specPublic$$init$(x1, ..., xn) {
   return new T(x1, ..., xn);
 }
 
where T is the name of type currently being translated.

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


finalizeTranslation

protected void finalizeTranslation()
Performs a finialization of translation, e.g., generation of spec inheritance mechanism.

Overrides:
finalizeTranslation in class TransType

staticInvariantCheckInitializer

protected JmlMethodDeclaration staticInvariantCheckInitializer()
Returns a static initializer that checks whether static invariants are established by the initialization of this class. The returned static initializer simply calls the static invariant check method of this class.


constructionStatusAccessor

protected JmlMethodDeclaration constructionStatusAccessor()
Returns declarations of a private instance field and a protected access method for storing and accessing the status of an instance construction. The returned field and method are used to disable assertion checks while the "this" object is being constructed by the constructor.


generateAccessorsForInterfaceModelFields

private boolean generateAccessorsForInterfaceModelFields()
Generates access methods for all the model fields inherited from the interfaces of this class. The generated access method is either a default access method or a dynamic delegation method. If the inherited model field has no represents clauses in the interface hiearchy, a default access method is generated; otherwise, a dynamic delegation method is generated which makes a dynamic call to the corresponding access method of the interfeace's surrogate class.

See Also:
defaultModelFieldAccessor(CField), modelFieldDelegationMethod(CField, JmlTypeDeclaration)

interfaceModelFields

private JFieldDeclarationType[] interfaceModelFields()
Returns all model fields inherited from the interfaces of this class, but excluding those also inherited from the superclass chain.


toSet

private Set toSet(JFieldDeclarationType[] fdecls)
Returns a set containing elements from the given array.


defaultModelFieldAccessor

private JmlMethodDeclaration defaultModelFieldAccessor(CField field)
Returns a default accessor method for a model field. The returned method has the following form:
  public [static] T model$n() {
    throw new JMLNonExecutableException();
  }
 


modelFieldDelegationMethod

private JmlMethodDeclaration modelFieldDelegationMethod(CField field,
                                                        JmlTypeDeclaration tdecl)
Returns a model field delegation method for model field, field, whose represents clause is found in type tdecl. The returned method has the following form:
  public [static] T model$n() {
    Object obj = dynamic_delegation_to_accessor_method_in_tdecl();
    return unwrapped_obj;
  }
 


specPublicAccessor

protected JmlMethodDeclaration specPublicAccessor(CField field)
Returns a default access method for a spec_public field. The returned method has the following form:
  public [static] T spec$n() {
    return x;
  }
 
where x is the name of the given field.


addNewMethod

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


defaultConstructor

private JmlConstructorDeclaration defaultConstructor()
Returns a default constructor for the target class declaration.


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;
 


surrogateCacheDeclaration

protected JmlMethodDeclaration surrogateCacheDeclaration()
Returns a field declaration for an interface surroagte cache with a cache lookup method and a cache update method. The returned value is of type JmlMethodDeclaration so that it can be added to the current type declaration by using addMember method.


dynamicInvocationMethod

protected JmlMethodDeclaration dynamicInvocationMethod()
Returns a method declaration that makes a dynamic call to the given method using the Java's reflection facility. The inheritance method makes dynamic invocations to a target method to 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.

Overrides:
dynamicInvocationMethod in class TransType

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("rac$receiver(" +clsName+ ", " +receiver+ ")");
 

See Also:
TransType.dynamicInvocationMethod()

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.