Abstract:
We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static veri.cation and static debugging). A key contribution of our approach is that a uni.ed assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional post-conditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimization to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of di.erent types of bugs in the Ciao system source code. Several experimental results are presented that illustrate di.erent trade-o.s among program size, running time, or levels of verbosity of the messages shown to the user.
Introduction:
We present a framework (and its implementation) that uni.es unit testing and run- time veri.cation (as well as static veri.cation and static debugging). Our approach builds on [BDD+97,HPB99,PBH00a,HPBLG05], where an approach to program devel- opment has been designed and implemented whose objective is to on one hand validate and on the other .nd bugs in programs with respect to speci.cations that are given in terms of assertions. The approach is based on a novel and expressive language of assertions for describing safety policies and, in general, very general program proper- ties [PBH97,PBH00b][CLI97,BCC+06].We have also proposed strategies for static (i.e., compile-time) checking of such policies as well as techniques for reducing at compile- time, using information from static analysis, the number of checks that have to be done dynamically (i.e., at run time) [PBH98,PBH99,HPBLG05]. Using these techniques, any assertions present in the program are falsi.ed or veri.ed as completely as possible dur- ing the compilation phase, since compile-time checking is always preferable to run-time, which is necessarily always incomplete as a means of veri.cation. However the existence in all practical programs of parameters and data only known at run-time and the rich nature of the properties that we are interested in determine that a certain degree of run-time checking is inevitable. In return the approach allows using very expressive safety policies with reduced overhead.
While the static checking part of this model has been the subject of considerable work, in this paper we shift to the actual run-time checking of safety policies, which has received little previous attention. Our aim is to a) develop e.ective implementation techniques for run-time checking that integrate seamlessly into our combined compile- time/run-time framework and b) to also develop integrated facilities for unit testing. To this end, we have .rst developed an implementation of run-time checks based on transforming the program into a new one which at the same time preserves the semantics of the original program and also checks during its execution the assertions present in it, and thus the safety policy. The transformation allows checking precon- ditions and postconditions, including conditional postconditions, i.e., postconditions that must hold only when certain preconditions hold. It also allows checking properties at arbitrary program points (i.e., between any two literals in a body clause) as well as checking certain computational properties, i.e., properties that are not speci.c to a program point but rather to whole computations, such as, for example, determinism, non-failure, or use of resources (steps, time, memory, etc.).
Our transformation also addresses to some extent one of the main drawbacks of run-time checking (in addition to incompleteness): the overhead introduced during execution of the program. The proposed transformation reduces run-time overhead by avoiding meta-interpretation whenever possible and by using special features of the low-level language when appropriate. Also, run-time checks can be compiled inline as opposed to calling a library, which introduces overhead due to additional (meta-)calls. Another relevant issue addressed by our transformation is being able to provide messages to the user which are as informative as possible when a violation of the safety policy is found, i.e., when a run-time check fails. To this end, the transformation saves appropriate information at source code level in the transformed .le. Depending on the level of code instrumentation selected, increasingly more accurate information about the assertions will be saved, and, thus, presented, o.ering di.erent trade-offs between information level and program size.
With respect to the closely related subject of testing, we require only a minimal extension to the assertion language in order to be able to de.ne unit tests [ER96]. The resulting language can express for example the input data for performing such unit tests, the expected output, the number of times that the unit tests should be repeated, etc. In contrast to previous work in this area (e.g., [BJ93], [ZGQC08], or the unit-test framework recently included in SWI-Prolog), a key contribution of our approach is that these unit tests blend in with and reuse the assertion language and the overall framework. In particular, only test drivers need to be added because the assertions and their run-time tests act as the checkers for the cases de.ned by the unit tests.
Both the run-time check generation and the unit testing approaches proposed have been implemented within the CiaoPP/Ciao system. We provide some experimental results which illustrate the implementation trade-offs involved. The integration with the CiaoPP/Ciao compile-time checking allows reducing run-time overhead to checking only those aspects of the safety policy that could not be determined statically. I.e., only the checks in assertions (including \tests") which cannot be verified at compile-time are converted into run-time checks. Note that since in our approach unit tests are also assertions, static analysis this also eliminates parts of or whole unit tests which may have been veri.ed statically. At the same time, the tight integration also allows using the unit test drivers to exercise run-time checks corresponding to those parts of assertions that could not be checked at compile-time, even if they were not conceived as tests. Finally, properties inferred by static analysis (e.g., types) can also be used for automatically generating input data for the unit tests (see [GZAP08] for a technique for this purpose).
Conclusions:
We have described our design and implementation of a framework that uni.es unit testing and run-time veri.cation (as well as static veri.cation and static debugging). A key contribution of our approach is that a uni.ed assertion language is used for all of these tasks. This has allowed us to propose and implement unit testing via a minimal addition to the assertion language. We have proposed methods for compil- ing run-time checks for (parts of) assertions which cannot be veri.ed at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional post-conditions, properties at arbitrary program points, and certain computational properties. We also have proposed a minimal addition to the assertion language which allows de.ning unit tests to be run in order to detect possible violations of the (partial) speci.cations expressed by the assertions. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the veri.cation of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results have been presented to illustrate di.erent trade-offs among program size, running time, or levels of verbosity of the messages shown to the user. The experimental results con.rm our expectations regarding these trade-offs: run-time checks do not pose an excessive amount of overhead, except with high levels of instrumentation (e.g., gathering information on the call stack). However, this is due to the simplistic way in which this type of instrumentation is implemented, which can be optimized using lower-level primitives. For example, it prevents the compiler from performing some classical optimizations like tail recursion. We also plan to further extend the assertion language with more primitives such as time out(T), which can be used to express that a test should finish in less than T milliseconds, user error(Str) which expresses that a predicate should write the string Str into the current error stream, or to add more properties for generating random input data values with a given probability distribution. We plan to study how the multiple specialization present in CiaoPP can further reduce run-time over- head. Finally, we are also working on an improved and more compositional strategy to defining computational properties.