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

as the remaining arguments; axioms for others are less restrictive, allowing them to be
expressed in terms of their application to constructors or variables as first argument and
without restriction for the remaining arguments.
Because operations can be partial, specifications also define the domain condition
of every partial operation, i.e, the situations in which the operation is required to be
defined. For instance, in ListWM , get is declared to be partial (as indicated by the
partial arrow -->? ) and its domain condition defines that get(L , I)

must be defined if I

is indeed an index of list L .
As shown in Figure 1, specifications are put together using specifications modules .
Specifications identified as core define the data types that need to be implemented while
theroleof parameter specifications is simply to impose constraints over their admissi-
ble instantiations. Now, suppose we have a candidate implementation for module LWM
and that we would like to check its conformance against what was specified. First we
need to establish a correspondence between each core sort s of the module LWM and
aJavatype T defined by one of our classes. Moreover, we need to establish a corre-
spondence between the operations and predicates of the specification that introduces s
and the methods and constructors of T .InC ON G U , this correspondence is defined by
means of a refinement mapping . In order to capture the role of parameter specifications,
these mappings also allow to link parameter specifications with the type variables of
generic classes. More concretely, a refinement mapping also defines a correspondence
between each parameter sort s and a Java type variable E and also a method signature
for each operation/predicate of the specification that introduces s .
Suppose that our candidate implementation for LWM consists of the generic class
MyListWMerge and the generic interface Mergeable presented in Figure 2. The cor-
respondence between LWM and this candidate implementation is defined in the refine-
ment mapping presented in Figure 3. It maps the compound sort ListWM[Mergeable]
(Figure 1) into the generic type MyListWMerge<E extends Mergeable<E>> (Fig-
ure 2) and the operations and predicates of the former into methods and constructors
of the latter. For instance, we can see that operation add is mapped into the method
void addFirst(E e) . The first argument of an operation always correspond to ob-
ject this and, hence, an operation with n arguments is mapped into a method with arity
n . Only operations declared constructors whose first argument is not the sort being

specified can be mapped into class constructors. Predicates are necessarily mapped into
boolean methods. For operations that produce elements of the sort being specified, the
corresponding method can either be void or of the corresponding type. In this way,
it is possible to deal with different implementation styles, namely immutable and mu-
table implementations. In our example, the class MyListWMerge provides a mutable
implementation of lists and, hence, all operations in this situation are mapped to void
methods.
The mapping in Figure 3 also establishes a correspondence between sort Mergeable
and thetype variable E . It is defined that the operation merge corresponds to the method
signature E merge(E e) . As we will explain in the next section, this refinement map-
ping is only correct if the instantiation of E in MyListWMerge<E> is limited to classes
C that have a method with signature C merge(C e) (which is indeed the case because
E has Mergeable<E> as an upper bound).

− 1