An unfold/fold transformation framework for definite logic programs
An unfold/fold transformation framework for definite logic programs
复制标题
确定逻辑程序的展开/折叠变换框架
DOI：
10.1145/982158.982160
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
I. Ramakrishnan
中科院分区：
文献类型：
--
作者：
Abhik Roychoudhury;K. Kumar;C. Ramakrishnan;I. Ramakrishnan
给定逻辑程序 P，展开/折叠程序转换系统导出程序序列 P = P0、P1、…、Pn，使得 Pi+1 通过应用展开或折叠步骤从 Pi 导出。展开/折叠变换已广泛用于提高程序效率和程序推理。展开对应于解析步骤，因此是语义保留的。另一方面，折叠用子句的头部替换了子句右侧的出现，可能会产生语义上不同的程序。现有的逻辑程序展开/折叠转换系统通过放置足以保证折叠正确性的（通常是语法上的）条件来限制折叠的应用。这些限制通常太强，尤其是当转换用于程序推理时。在本文中，我们为确定的逻辑程序开发了一个转换系统（称为 SCOUT），它被证明比现有的转换系统更强大（就允许的转换序列而言）。逻辑程序转换的新颖用途需要这种额外的能力：用于验证特定类别的并发系统，称为参数化并发系统。我们的转换系统是通过开发一个框架来构建的，该框架由“测量空间”和相关的测量函数参数化。该框架对折叠的应用没有语法限制，并且可以用于导出变换系统（通过固定测度空间和函数）。系统的威力由测度空间和功能的选择决定；因此，可以通过考虑不同变换系统的测度空间和函数来比较它们的相对能力。这些转换系统的正确性来自于框架的正确性。我们展示了各种现有的转换系统可以作为我们框架的实例。我们通过目标替换变换扩展展开/折叠变换框架，该目标替换变换允许原子的语义等价连接被互换。然后，我们派生出一个新的转换系统 SCOUT 作为该框架的实例，并展示其相对于现有转换系统的强大功能。 SCOUT 已用于归纳证明参数化并发系统（有限状态并发系统的无限族）的时间属性。我们演示了在构建此类归纳证明时如何使用 SCOUT 的附加功能。
Given a logic program P, an unfold/fold program transformation system derives a sequence of programs P = P0, P1, …, Pn, such that Pi+1 is derived from Pi by application of either an unfolding or a folding step. Unfold/fold transformations have been widely used for improving program efficiency and for reasoning about programs. Unfolding corresponds to a resolution step and hence is semantics-preserving. Folding, which replaces an occurrence of the right hand side 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 (called SCOUT) for definite logic programs 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 transformations: for the verification of a specific class of concurrent systems, called parameterized concurrent systems.Our transformation system is constructed by developing a framework, which is parameterized by a "measure space" and associated measure functions. This framework places no syntactic restriction on the application of folding, and it can be used to derive transformation systems (by fixing the measure space and functions). The power of the system is determined by the choice of the measure space and functions; thus the relative power of different transformation systems can be compared by considering their measure spaces and functions. The correctness of these transformation systems follows from the correctness of the framework. We show that various existing transformation systems can be obtained as instances of our framework. We extend the unfold/fold transformation framework with a goal replacement transformation that allows semantically equivalent conjunctions of atoms to be interchanged. We then derive a new transformation system SCOUT as an instance of the framework and show its power relative to the existing transformation systems. SCOUT has been used to inductively prove temporal properties of parameterized concurrent systems (infinite families of finite state concurrent systems). We demonstrate the use of the additional power of SCOUT in constructing such induction proofs.