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

call is intercepted and forwarded to ColorPMonitoring in order for the properties of
this operation to be checked.

5 Conclusions

The importance of tools that support runtime conformance checking of implementa-
tions against formal specifications has long been recognised. In the last decade, many
approaches have been developed for monitoring the correctness of OO programs w.r.t.
formal specifications (e.g., [1,3,7,8,12,15]). However, despite the actual popularity of
generics in mainstream OO languages [5], current approaches still lack support such a
feature. This was also a limitation C ON G U that was overcome in C ON G U 2.
In this paper we showed how the C ON G U approach and the corresponding tool were
extended in order to support the specification of parametrized data types and their im-
plementation in terms of generic classes. The extension of the specification language
in order to support the description of generic data types was relatively simple. Given
that C ON G U relies on property-driven specifications, this mainly required the adoption
of parameterized specifications available in conventional algebraic specification lan-
guages. In order to bridge the gap between parameterized specifications and generic
classes we proposed a new notion of refinement mapping around which a new notion of
conformance between specifications and OO programs was defined. To the best of our
knowledge, this issue has not yet been addressed in other contexts. Other approaches
exist that deal with the problem of the implementation of architectural specifications
including parameterized specifications as, for example [2], but the target are ML pro-
grams. Relationships between algebraic specification and OO programs that we are
aware of, namely those that address runtime conformance checking or testing, exclu-
sively consider flat and non-parameterized specifications (e.g., [1,12,18]).
C ON G U 2 implements the runtime monitoring of this new notion of conformance
which, in the case of generic data types, involves checking that both the class that im-
plements the data type and the Java types used to instantiate it conform with what
was specified. With C ON G U 2, runtime conformance checking becomes applicable to
a range of situations in which automatic support for detection of errors becomes more
relevant. Generics are known to be difficult to grasp and, hence, with generics in action,
obtaining correct implementations becomes more challenging. For us, it is particularly
important to be able to use C ON G U with the generic data types that appear in the context
of a typical Algorithms and Data Structures course: we believe this course constitutes
an excellent opportunity for exposing undergraduate students to formal methods. As
discussed by Hu [13], accurate descriptions of abstract data types, agnostic w.r.t. pro-
gramming paradigms and languages, are important for teaching these concepts. From
our experience in teaching this course for several years (initially without tool support
and, more recently, using C ON G U ), we are convinced that, from an educational an mo-
tivational point of view, it is quite important that students experience, in their practice,
that they can take real advantage of formal descriptions. The use of a simple tool that
allows them to gain confidence that their classes correctly implement a given data type
has shown to be a good starting point. The extension of the tool to support generics will
contribute to the success and effectiveness of the C ON G U approach to the introduction
to formal methods in the computer science curriculum.