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

Fig. 2. The interface Mergeable<E> and an excerpt of the Java class MyListWMerge<E>

After defining the refinement mapping from module LWM to our candidate imple-
mentation, C ON G U instruments MyListWMerge.class so that, during the execution
of any program that uses MyListWMerge , the behaviour of this class (made precise in
the next section) is checked against what was specified in ListWM[Mergeable] .More-

over, the behaviour of the classes used for instantiating E in the creation of objects
of MyListWMerge<E> is also checked against what was specified in Mergeable . Sup-
pose, for instance, that we have a program that includes a class Color that implements
Mergeable<Color> and, another class, that creates and manipulates objects of type
MyListWMerge<Color> . In this case, the behaviour of Color is checked against what
was specified in Mergeable .

3 Runtime Conformance of Programs against Modules

In this section, we present the notion of conformance of Java programs against specifi-
cation modules that is considered in C ON G U 2 and discuss some key aspects of C ON G U
approach to the runtime checking of this notion of conformance.

3.1 Object Properties Induced by Specifications

The conformance of a Java program against a specification module can only be defined
if a direct connection between the specifications of the module and the classes of the
Java program is provided. As discussed before, in C ON G U , the correspondence between