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

The monitoring process also heavily depends on an auxiliary method generated as
part of each PM-class, named conguAssert . This method is responsible for issuing
adequate error messages whenever a violation occurs. It takes as parameters the asser-
tion to evaluate, an enumerate value flagging what kind of property was violated (either
a domain condition or an axiom-induced property) and error description elements. The
method tests the assertion and throws an exception if it is false , detailing the violation
with the descriptive elements received as arguments. The error description elements
passed to this method are the file of the specification to which the property belongs, the
domain or axiom to which it pertains as written in the specification and its line. In this
way, it is possible to pinpoint the origin of the error, in terms of the specification, which
can be invaluable when developing in a specification guided manner.
In step 3, in addition to invocation of the original method, it is also checked that
if the domain condition holds, the invocation of the method returns normally. This is
achieved by surrounding the original method call with a try-catch statement. The catch
clause is only reached when the original method fails to return normally, in which case
a violation is issued if the domain condition was true. If the domain condition was
false, no constraints apply and, hence, the caught exception is re-thrown, allowing the
program to handle it as it would had it been executing normally.
It is worth noting that the properties monitored by each of PM-class do not neces-
sarily originate from a single specification. Refinement mappings do not restrict the
number of specifications that a Java type may implement, therefore the PM-class for a
given type is responsible for monitoring the properties arising from all the specifications
that have been refined to mentioned type.
All of the above holds true for both core and parameter specifications. However,
parameter specifications require another level of indirection. Let C be a generic class
with a parameter E that refines a core parameterized specification, say S

[ S ]

.Even
though each class that is used to instantiate E in C has a corresponding PM-class, the
code generated for monitoring the properties of S that involves to call a method over an
object e of type E , cannot commit to a specific PM-class (the actual type of e is only
known at runtime and will vary from call to call).
C ON G U 2's solution is to generate a dispatcher class associated to each type variable
of the refinement mapping. This class has the exact same methods of a PM-class, but,
instead of monitoring properties, only resolve to which PM-class should the call be
forwarded to, based on the actual type of object callee . In the PM-class for class C ,
whenever the testing of a property requires to invoke a method of E , the call is placed
to the respective dispatcher class.
Suppose that our program manipulates an object lc of type MyListWMerge<Color>
and another lt of type MyListWMerge<Text> . Monitoring the behaviour of these
objects is performed by the MyListWMergePMonitoring class. Whenever such op-
eration involves a call to method E merge(E) , we call the respective method in the
EPMonitoring dispatcher class. While monitoring lc 's behaviour, the actual type of
the callee is Color and, hence, the dispatcher forwards the invocation of merge to
ColorPMonitoring . Similarly, while monitoring lt , the calls are forwarded to class
TextPMonitoring . Notice however that when, as a result of calling mergeInRange
over lc , method E merge(E) is called (see the body of the method in Figure 2), this