Runtime Verification for Generic Classes with CONGU2 - Formal Methods: Foundations and Applications - page 43

types and, hence, a new strategy for verifying that generic classes possess the methods
mentioned in the refinement is needed.
Although information about generics is not used at runtime by the JVM, this infor-
mation is still retained in the bytecode, in the form of metadata and can be queried
through Java's reflection API. The strategy to verify that a generic class has the meth-
ods mentioned in the refinement mapping involves retrieving its methods, getting the
generic parameter types and generic return type of each one and then comparing with
what was expected (a recursive process on the structure of the types).
The second phase of the refinement analysis addresses the verification of the condi-
tions concerning the parameter specifications. Recall that, in this case, specifications
are not refined into concrete Java types and what is necessary ensuring is that the
classes that can be used to instantiate the corresponding type variable have the right
methods. For instance, in our example, in this phase it is verified that every class C
that can be used to instantiate E in MyListWMerge<E> possesses a method with sig-
nature C merge(C e) . This is achieved by going through the upper bounds of E in
MyListWMerge (in our case there is a single upper bound but in general types may
have more than one). Methods whose signature depends somehow on type E (in our
case, E merge(E e) ) need only to be searched on the upper bounds types that are
themselves generic and dependent of E (in our case, Mergeable<E> ) while the re-
mainder methods are searched on all upper bounds types. Searching for these methods
in generic types follows the strategy described before.
Additionally, the analysis of the refinement mapping also involves ensuring that hi-
erarchy relationships established for specification sorts are maintained when refining
to Java types. This is directly accomplished again making use of Java reflection API,
which enables us to query a type for its super class and/or implemented interfaces.
4.2 Bytecode Instrumentation
For monitoring the behaviour of Java programs, C ON G U relies on the interception of
method calls by client classes. In C ON G U 2, this is achieved with method call inter-
ception through bytecode instrumentation of a copy of the original class (the original
bytecode remains unchanged so that the program can also be executed normally). The
objective of this instrumentation is to inject bytecode instructions in the methods to for-
ward the call to a corresponding method in a property-monitoring class. From the start,
the goal was to minimise the impact on the original bytecode, avoiding any undesir-
able side effects of its faulty manipulation as much as possible, preferring to generate
Java code and rely on the compiler for type safety. Realising this new strategy posed
interesting challenges, namely:
Inner calls. How to avoid interception of intra-class method calls? Intra-class calls can
not be monitored otherwise we obtain a non-terminating program.
Calls from within superclasses. How to prevent interception of calls from within a
superclass? Such calls cannot be monitored for the reason above.
Constructors. How to intercept calls to object constructors and redirect them?
Clone and equals. What to do when these methods are not overriden in the class?
(Recall that C ON G U relies on these methods and there are properties that have to
be monitored when they are invoked.)