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

3.2 Checking Object Properties

In C ON G U , the strategy for runtime checking the conformance of a program against a
specification module consists in checking the properties induced by the axioms at the
end of specific methods, determined by the structure of the axioms. Let us first consider
the axioms with a left-hand side expressed in terms of the application of operations or
predicates to constructors as first argument and variables as the remaining arguments.
In this case, the property induced by the axiom is checked at the end of the method that
refines the referred constructor. All method invocations that are performed in order to
check a property make use of clones, whenever cloning is possible. Otherwise, the side
effects of these methods would affect the monitored objects (if method clone() is not
available, it is assumed that the class's objects are immutable). For instance, the property
induced by the first axiom for get is checked at the end of void addFirst(E e)
through the execution of the following code, where eOld is a copy of e obtained at the
entry of the method.
if (eOld != null ){
Ee2= this .clone().get(0);
assert(e2 != null && e2.equals(eOld));

}
Similarly, the second axiom of the get operation is checked by the below code, where
rangeOfInt , of type Collection<Integer> , is populated with integers that cross
the boundary (either as parameters or as returned values) of some method in class
MyListWMerge .
if (eOld ! = null )
for ( int i: rangeOfInt)
if (i>0 && i< this .clone().size()) {
Ee2= this .clone().get(i);
assert((i-1)>=0 && (i-1)<thisOld.clone().size());
E e3 = thisOld.clone().get(i-1);
assert(e2!= null && e3!= null && e2.equals(e3));

}
On the other hand, the properties induced by axioms that feature a variable as first
argument are checked at the end of the method that refines the corresponding opera-
tion/predicate. For instance, the last axiom for isEmpty is checked at the end of method
boolean isEmpty() by:
if (result) assert(thisOld.clone().size()==0);
where result is the return value of method isEmpty() .
Equality of integers and booleans is translated into comparisons with == whereas
the equality of terms of a non-primitive sort, say s , is translated into invocation of
method equals of the class T S . Therefore, it is essential that all involved classes define
a proper implementation of equals . Namely, because equality of terms is a congruence,
equals should be defined in such a way objects are considered equal only if they are
behaviourally equivalent with respect to the methods that refine some operation of s
(i.e., calling these methods over equal objects must produce equal results).
Correctness of equals is checked at runtime as follows. At the end of the method,
if the return value is true, then it is checked that by applying the method that refines
each observer to the two objects, we obtain equal results. For instance, checking the