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

Java programs and algebraic specifications. This work paved the way for the extension
of runtime conformance checking to a more comprehensive range of situations. In this
paper, we present a new approach to runtime conformance checking of Java implemen-
tations against specifications (applicable to parameterized specifications) and discuss
how this solution is realized in the new version of C ON G U tool.
The solution for runtime checking that was developed in order to accommodate
generics is substantially different from that used before in C ON G U [17]. Therein, the
strategy was to replace the original classes by proxy classes and generate further classes
annotated with monitorable contracts, written in JML [14]. The main innovative aspects
of the solution adopted in C ON G U 2 are the following:
- Introduction of new mechanisms that allow to deal with generics, namely to check
whether classes used to instantiate the parameters of generic classes conform to
what was specified in the parameter specifications.
- Original classes are not replaced by generated proxy classes. Instead, the solution
now relies on the instrumentation of the bytecode of original classes, overcoming
the difficulties on the generation of appropriate proxy classes for classes making
use of, e.g., public fields or inner classes.
- JML, which does not support generics (among other features introduced in Java
1.5 [9]), is no longer used. Instead, runtime checking of the specified properties at
specific execution points is now achieved directly by the generated code, relying
only on Java assertions. The compilation with jmlc of contract annotated classes
was a bottleneck in terms of performance and, with the new solution, we were able
to substantially reduce the compile time.
The remainder of the paper is organised as follows. In Section 2 we provide an overview
of the C ON G U approach, namely we introduce specifications and refinement mappings
adopted in C ON G U . Then, Section 3 presents the notion of conformance between spec-
ifications and Java classes and discusses the properties induced by specifications that
are monitored at runtime. The solution for the monitoring of these properties that is
realized in C ON G U 2 is presented in Section 4. Section 5 concludes the paper.
2OvewoftheC ON G U Approach
As mentioned before, C ON G U supports the runtime conformance checking of Java pro-
grams against algebraic specifications. In this section we provide an overview of the
C ON G U approach, focusing on some of the aspects that are visible to users: the specifi-
cation language and the notions of specification modules and refinement mapping (see
[16] for details). This is achieved by means of an example around a simple ADT — lists
with merge .
This ADT represents lists composed of “mergeable” elements and that have an op-
eration — mergeInRange — that merges the elements of the list in a given range i...j
(the resulting element is placed in the position i of the list). Figure 1 shows the three
elements involved in the specification of this ADT using C ON G U 's specification lan-
guage. In most aspects the language closely follows C ASL [4], which is considered a
standard for algebraic specification.