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

Fig. 3. A refinement mapping from LWM to { MyListWMerge<E> , Mergeable<E> }

specifications and classes is established through the use of refinement mappings. In the
previous section we have already mentioned some conditions required by refinement
mappings, namely those concerning the matching of method signatures with operations
and predicates. The complete set of conditions that a mapping has to meet in order to
define a refinement mapping is defined below.
A refinement mapping consists of a set V (of type variables) equipped with a pre-
order < and a refinement function R that maps:

1. each core simple specification to a non-generic type defined by a Java class;
2. each core parameterized specification to a generic class, with the same arity;
3. each core specification that defines a sort s<s , to a subtype of

R ( S ) ,where S

is the specification defining s ;
4. each parameter specification to a type variable in V ;
5. each operation of a core specification to a method of the corresponding Java type
with a matching signature;
6. each operation of a parameter specification to a matching method signature.
Additionally:
7. if a parameter specification S defines a subsort of the sort defined in another pa-
rameter specification S , then it must be the case that S )

holds;
8. if S is a parameterized specification with parameter S , it must be possible to ensure
that any type C that can be used to instantiate the parameter of the generic type
R (

R ( < R ( S )

S ) S ) possesses all methods defined by R for type variable R ( after replacing

R ( S )

by C . all instances of the type variable