Abstract:
Given a logic program P, an unfold/fold program transformation system derives a sequence of programs P = P(0), P(1), ..., P(n), such that P(i+1) is derived from P(i) by application of either an unfolding or a folding step. Unfold/fold transformations have been used widely for program improvement and for reasoning about programs. Unfolding corresponds to a resolution step and hence is semantics-preserving. Folding, which replaces an occurrence of the r.h.s. of a clause with its head, may on the other hand produce a semantically different program. Existing unfold/fold transformation systems for logic programs restrict the application of folding by placing (usually syntactic) conditions that are sufficient to guarantee the correctness of folding. These restrictions are often too strong, especially when the transformations are used for reasoning about programs. In this article we develop a transformation system for definite logic programs (called SCOUT) that is provably more powerful (in terms of transformation sequences allowed) than existing transformation systems. This extra power is needed for a novel use of logic program transformation systems: for the the verification of parameterized concurrent systems.Our transformation system is constructed by first developing a framework, which is parameterized by a ``measure space'' and associated measure functions, that places no syntactic restriction on the application of folding. The power of the system is determined by the choice of the measure space and functions, and the correctness of the transformations follows from the correctness of the framework. An important aspect of the framework is that the power of different transformation systems can be compared by considering their measure spaces and functions. We extend the unfold/fold transformation framework with a goal replacement transformation which allows semantically equivalent conjunctions of atoms to be interchanged. We show that various existing transformation systems can be obtained as instances of our framework. We then derive SCOUT as another instance of the framework and show its power relative to the existing transformation systems.
The transformation framework and SCOUT are described in this article by considering only definite logic programs; the framework has been extended to handle normal logic programs (programs with negation) as well. The transformation system, SCOUT, has been used for automated generation of induction proofs to establish temporal properties of infinite families of concurrent systems. We describe the application in this article and demonstrate the use of the additional power of SCOUT in constructing induction proofs.
Bibtex Entry:
@article{RKRR:TOPLAS04, author = {Abhik Roychoudhury and K. Narayan Kumar and C. R. Ramakrishnan and I. V. Ramakrishnan}, title = {An unfold/fold transformation framework for definite logic programs}, journal = {ACM Transactions on Programming Languages and Systems ({TOPLAS})}, volume = {26}, number = {3}, pages = {464--509}, year = {2004} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)