JML

org.jmlspecs.jmlrac
Class TransInterface

java.lang.Object
  extended byorg.multijava.util.Utils
      extended byorg.jmlspecs.jmlrac.TransUtils
          extended byorg.jmlspecs.jmlrac.TransType
              extended byorg.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.

Constructor Detail

TransInterface

public TransInterface(JmlInterfaceDeclaration interfaceDecl)
Construct a TransInterface object.

Parameters:
interfaceDecl - target interface declaration to be translated
Method Detail

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:


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;
 


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.