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

correctness of boolean equals(Object other) in MyListWMerge includes the
below code for the get operation.
if (result)
for ( int i: rangeOfInt)
if (i>=0 && i<thisOld.clone().size()
&& i<otherOld.clone().size()) {
E e1 = thisOld.clone().get(i);
E e2 = otherOld.clone().get(i);
assert(e1!= null && e2!= null && e1.equals(e2));
}
In addition, at the end of method clone() , it is checked that the returned object is equal
to the original. Additional properties such as symmetry and transitivity of equals()
can also be checked, in a similar way, at this point.
Finally, checking that client classes are well-behaved, i.e., do not invoke a method
that refines an operation when its domain condition does not hold and also do not pass
null as argument, can be easily performed at the beginning of the method. For instance,
in the case of method void set( int i,E e) , this is checked by:
assert(e != null &&i>=0&&i< this .clone().size());
4TheNewC ON G U Tool
The new C ON G U tool, which we named C ON G U 2, implements the runtime checking
approach conformance of Java classes against specifications described in the previous
section. As shown in Figure 4, the tool takes as input a specification module, a set
of specifications, a refinement mapping and a Java program (in bytecode form). The
program is then transformed so that, when executed under C ON G U , the behavior of
each class is checked against the corresponding specification. This is achieved by inter-
cepting the calls to all methods that, according to the refinement mapping, refine some
operation, and dispatching them to property-monitoring classes generated by the tool.
As mentioned in the introduction, in the previous version of C ON G U , the intercep-
tion of methods was accomplished by proxy classes that wrapped and mimicked the
original class's interface as close as possible, capturing the client method calls and di-
verting them to classes annotated with JML contracts. These contracts were checked at
runtime with resort to JML's Runtime Assertion Checker. In order to overcome the dif-
ficulties on the generation of appropriate proxy classes for classes making use of more
advanced features of the Java language, such as public fields or inner classes, C ON G U 2
intercepts client method calls through bytecode instrumentation. On the other hand,
JML is no longer used and, instead, properties to be checked are now encoded using
Java assertions. In this way, C ON G U was released from several limitations imposed by
the use of JML, namely the lack of support for features introduced in Java 1.5 (generics
included), the long compilation times imposed by jmlc (namely, because of the compi-
lation of the JML models of the Java API) and the poor and unstable information about
assertion violations that hindered the connection of errors with the axioms of specifi-
cations (the C ON G U solution for this problem, developed for JML 5.4 quickly became
obsolete).