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

types. In addition it features an argument callee of type C (a reference to original
method callee) and a boolean argument monitoring (signalling whether monitoring
should be performed or not). When invoked from the instrumented bytecode, this flag
is set to true ; when the invocation is realised in the context of a property monitoring it
is set to false .
These static methods are responsible for the monitoring of the relevant object prop-
erties following a general pattern:
1. At the entry of the method, store all elements that, later, are needed for checking
some property (these elements are stored in variables starting with old ).
2. Verify that the client is well-behaved, namely that the domain condition holds (only
applicable in the case of strong conformance) and the values passed as arguments
are non null ;
3. Call the original method upon callee and keep its return value;
4. Check the properties defined by the axioms.
5. Return the original method return value.
The execution of steps 2 and 4 for method m (which are only executed if flag
monitoring is true) rely on two separate static methods: mPre and mPos . These test
callee for the object properties induced by the specification as described in 3.2 but,
instead of calling the methods of the original class, they call the method of the corre-
sponding PM-class with monitoring set to false.
More concretely, the method mPre receives the same arguments as the original one,
plus a boolean flag signalling whether to break on a violation, and returning a boolean
value, corresponding to whether or not the respective domain condition is satisfied.
Method mPos is void and takes as arguments: (i) two references to the callee (one before
application of the original method, i.e., its old value, and another after the original
method call); (ii) the arguments of the respective method in the PM-class and (iii) a
boolean flag signalling whether to break on a violation.
Figure 5 presents a sequence diagram that illustrates the flow of execution in the
concrete case of a call to method mergeInRange( int , int ) .

:Client :M y ListWMer g e :M y ListWMer g ePMonitorin g

mergeInRange(i, j)

mergeInRange(this, i, j, true)

thisOld = clone(this, false)

clone_Original()

mergeInRangePre(this, i, j, false)

mergeInRange_Original(i, j)

mergeInRangePos(this, thisOld, i, j, false)

Fig. 5. The property-monitoring process