静态切片方法的程序依赖性研究：重写系统表示的一阶函数程序的静态切片

理论计算机科学电子笔记177（2007）123-136www.elsevier.com/locate/entcs重写系统的静态切片1DiegoCheda2JosepSilva2Germ'anVidal2DSIC，瓦伦西亚技术大学Camino de VeraS/N，46022瓦伦西亚，西班牙摘要程序切片是一种通过分析程序的数据流和控制流来分解程序的方法。基于切片的技术在软件工程领域有许多应用（如程序调试、测试、代码重用、维护等）。切片在命令式编程范式中得到了广泛的研究，其中它通常基于所谓的程序依赖图，这是一种数据结构，明确的数据和控制的依赖性为每个操作在一个程序。不幸的是，“依赖性”的概念在这项工作中，我们定义了一种新的静态切片方法独立于特定的输入数据），用于通过重写系统表示的一阶函数程序。为此，我们引入了一个适当的概念，可用于计算程序切片的依赖。此外，由于静态切片的概念是一般不可判定的，我们介绍了一个完整的近似计算静态切片的基础上建设的长期依赖图，对应的程序依赖图。关键词：程序切片，重写系统1介绍程序切片[13]是一种通过分析程序的数据和控制流程来分解程序的方法。粗略地说，一个程序切片由那些程序状态组成，这些状态（潜在地）与在某个程序点和/或变量处计算的值相关，称为切片准则。在命令式编程中，切片标准通常由一对（程序行，变量）给出例1.1考虑图1中的程序来计算文本的字符数和行数。这个程序的一部分w.r.t.切片标准（12，chars）将包含黑色句子（而灰色句子被丢弃）。 这个切片包含了计算第12行变量chars值所需的所有程序部分。1这项工作得到了欧盟（FEDER）和西班牙教育和文化部（MEC）的部分支持，赠款为TIN 2005 - 09207-C 03 -02，信息和通信技术促进欧盟-印度跨文化传播项目ALA/95/23/2003/077-054，由LERNetAML/19提供。0902/97/0666/II-0472-FA，并由项目TAMAT参考下的VicerrectoradodeInnovacio'nyDesarolodela UPV57712电子邮件：{dcheda，jsilva，gvidal}@dsic.upv.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.010124D. Cheda等人/理论计算机科学电子笔记177（2007）123（九）（六）（七）（八）（十）开始（一）（二）（三）（四）（五）（十一）（十二）停止（一）lineCharCount（str）（二）i：=1;（三）return 0;（四）return 0;（五）while（i length（str））做（六）if（string [i]==0）(7)然后lines：= lines+ 1;(8)chars：= chars +1;(9)return chars：= chars +1;(10)i=i+1;(11)回流管线;(12)return chars;Fig. 1. 示例程序lineCharCount图二. lineCharCount的控制流程图为了从程序中提取一个切片，必须首先计算其语句之间的依赖关系。控制流图（CFG）是一种数据结构，它使程序中每个操作的控制依赖关系显式化。例如，图中程序的CFG图1中描绘了二、然而，CFG一般不支持计算程序片，因为它只存储控制依赖，对于许多应用（如调试），数据依赖也是必要的。由于这个原因，在命令式编程中，程序片通常从程序依赖图（PDG）[4，6]中计算，该程序依赖图明确了程序中每个操作的数据和控制依赖性。PDG是一个有向图，其中节点表示源代码中的语句，边表示数据和控制依赖。作为示例，图3中描绘了图1中的程序的PDG，其中实线箭头表示控制依赖性，虚线箭头表示数据依赖性。程序依赖性可以向后或向前（从切片标准）遍历，这分别被称为向后或向前此外，切片可以是动态的或静态的，这取决于是否提供了具体程序可以找到关于切片D. Cheda等人/理论计算机科学电子笔记177（2007）123125的完整调查，例如，在[12]中。虽然PDG很好地表示数据和控制重要程序的数据流行为，但它们的粒度级别（即，将所有函数体作为一个整体考虑）不适合于表示函数式编程中的依赖性在这项工作中，我们提出了一个新的依赖项重写概念，可以用来给静态切片一个适当的定义可惜126D. Cheda等人/理论计算机科学电子笔记177（2007）123（一）（二）（三）（四）（五）（十一）（十二）（六）（十）（七）（八）（九）图三. lineCharCount的程序依赖图静态切片的计算通常是不可判定的，因为应该考虑给定程序的所有可能的计算，因此，我们还引入了一个完整的算法来计算静态切片，该算法基于项依赖图的构造，项依赖图是一种新的形式主义，用于表示由项重写系统表示的一阶函数程序的本文的其余部分组织如下。在下一节中，我们将回顾一些关于术语重写的概念，这些概念将在整个论文中使用。然后，在第3节中，我们将介绍在函数上下文中进行静态切片的方法。第4节介绍了一种新的数据结构，称为术语依赖图，可以用来计算静态切片。最后，第5节讨论了一些相关的工作和结论。2预赛为了完整起见，我们在这里回顾一些术语重写的基本概念我们请读者参阅[3]以了解详细情况。一组重写规则（或有向方程）l→r使得l是不变项，r是其变量出现在l中的项，称为项重写系统(TRS简称）;项L和R分别称为规则的左手侧和右手侧。 我们假设所有规则的编号都是唯一的。给定签名F上的TRSR，定义的符号D是根规则和构造函数左侧的符号是C=F\D。我们限制我们自己有限的签名和TRS。我们分别用T（F，V）和T（C，V）来表示项和构造项的定义域，其中V是一个variables的集合，满足h F<$V=H。一个TRS R是基于构造器的，如果它的规则的左手边具有f（s1，. 其中si是构造器项，即， si∈T（C，V），对所有i = 1，. ，n.项t的根符号由root（t）表示。项t是操作根的（分别为构造根），如果根（t）∈ D（分别root（t）∈C）。出现在项t中的变量的集合由Var（t）表示。一个项t是线性的，如果V的每个变量在t中至多出现一次。R是左线性的（分别为右线性），如果l（resp.r）对所有规则l→r∈R是线性的。在本文中，我们将自己限制在基于左线性构造器的TRS，我们通常称之为程序。D. Cheda等人/理论计算机科学电子笔记177（2007）123127作为惯例，项t中的位置p由自然数序列表示，其中Λ表示根位置。位置用于处理被视为树的术语的节点：|p表示t在位置p处的子项而t [s] p表示替换子项t的结果|P的项S。 项t是如果Var（t）=0，则g r u nd i。 一个空间σ是一个可由任意给定条件构成的函数，使得它的定义域Dom（σ）={x∈ V|x/= σ（x）}是有限的。 标识替换由id表示。 项tJ是项t的instance，如果有替换σ，tJ=σ（t）。两项s和t的单位元是用σ（s）=σ（t）替换σ。 在下文中，我们将对象序列o1，.，on.重写步骤是将重写规则应用于术语，即，t→p，Rs，如果存在t中的位置p，重写规则R =（l → r）和用t替换σ |p= σ（l），s = t [σ（r）] p（p和R在约化步骤的符号中经常被省略）。实例化的左手边σ（l）称为redex。一个项t称为不可约的或标准形式的，如果没有项s满足t→s。我们用→+表示→的传递闭包，用→ +表示→的自反和传递闭包。给定一个TRSR和一个项t，我们说t的求值结果是sit→s，并且s是正规形式。3重写系统在本节中，我们将介绍术语重写中的依赖概念，然后使用它来给出静态切片的适当定义。首先，我们定义一个术语的程序位置，它唯一地确定它在程序中的位置。定义3.1（位置，程序位置）位置由自然数的序列表示，其中Λ表示空序列（即，根位置）。它们用于处理被视为树的术语的子术语不|Λ= t，对于所有项t∈T（F，V）d（tn）|i.w= ti|W 如果 i∈ {1，.，n}，d/n ∈F一个程序位置是一个对（k，w），它寻址（可能是可变的）子项r|w在P的第k个规则l→r的右手边r。给定一个程序P，Pos（P）表示P 右 边 项 的 所有程序位置的集合。定义3.2（标记项）给定一个程序P，一个标记项是一个项，其中每个（构造函数或定义的）函数或变量符号被标记为一组来自Pos（P）的程序位置。标记项的域可以归纳定义如下：• aP是标号项，a∈F <$V且P<$Pos（P）;• 若d/n∈ F，P∈Pos（P）且t1，.，tn是标记项，则dP（t1，.，tn）也是标记项。在本文的其余部分，我们假设以下考虑：• 程序规则的右侧被标记。• 标签不干扰模式匹配、实例、替换、重写步骤、推导等的标准定义（即，标签被忽略）。128D. Cheda等人/理论计算机科学电子笔记177（2007）1230M• 重新定义了一个（标记的）替换σ对项t的应用，使得对于每个结合x<$→dP0（tP1，.，tPn），如果变量xP出现在t中，则它是1N替换为dPP0（tP1，. ，tPn）的关系。1N下一个例子说明了为什么我们需要将一组程序位置与每个术语相关联，而不仅仅是一个位置：例3.3考虑以下带标签的程序：3（R1） main→g{（R1，Λ）}（f{（R1，1）}（Z{（R1，1. 1）}））（R2）g（x）→x{（R2，Λ）}（R3）f（x）→x{（R3，Λ）}连同推导：main {} →Λ，R1g {（R1，Λ）}（f {（R1，1）}（Z {（R1，1. （1）→1，R3 g {（R1，A）}（Z {（R3，A），（R1，1. （1））-Λ，R2Z {（R2，Λ），（R3，Λ），（R1，1. 1）}在这里，我们可能会争辩说，在推导的最后一项中Z的程序位置列表应该只包含对（R1，1。1）（即，Z唯一出现在第一条规则的右侧）。然而，对于程序切片，还需要知道Z已经通过出现在第二和第三规则右侧的变量x传播。注意main被标记为一组空的程序位置，因为它没有出现在任何程序规则的右侧。在介绍“依赖”的概念之前，我们需要以下定义。4这里，我们让“·”是一个新的构造函数符号，它没有出现在F中（没有标记）。我们用这个符号表示缺少的子项。定义3.4（次约化）设D：t0→p1，R1 ... →pn，Rn tn是一个导子对于t0，其中tn∈T（C，V）. 我们说D J：tJ→pJ，RJ... →pJ，RJtJ，011m≤n，是 D的一个次约化，如果下列条件成立：MMm(i) TJ(ii) TJ=t0[·]p对于某个位置p，是标准形式，并且(iii) 序列（pJ，RJ）中的所有元素，.，（pJ，RJ）也出现在SE-1 1m m序列（p1，R1），.，（pn，Rn），且顺序相同。粗略地说，我们说一个导子是另一个导子的子约化，如果• 初始项是相等的除了可能有一些缺失的子项，3在示例中，数据构造器符号以小写字母开头，而定义的函数和变量以小写字母开头此外，我们强调了在每个还原步骤中选择的redexD. Cheda等人/理论计算机科学电子笔记177（2007）123129[4]在[5]中可以找到一个类似但更一般的子约简概念130D. Cheda等人/理论计算机科学电子笔记177（2007）123• 两个推导都以标准形式结束（即，不可约项），以及• 除了由于初始项（及其后代）中缺少子项而不能执行的某些步骤之外，在两个推导中以相同的顺序执行相同的步骤。例3.5考虑下面的标记程序：（R1）main→C{（R1，Λ）}（f{（R1，1）}（A{（R1，1.1）}），g{（R1，2）}（B{（R1，2. （R2）f（A）→D{（R2，A）}（R3）g（x）→x{（R3，Λ）}连同推导D：C{（R1，1）}（f{（R1，1）}（A{（R1，1）}）1）}），g{（R1，2）}（B{（R1，2. （1）→1，R2 C{（R1，Λ）}（D{（R2，Λ）}，g{（R1，2）}（B{（R1，2. （1）→2，R3 C{（R1，A）}（D{（R2，A）}，B{（R3，A），（R1，2. （1））然后，例如，以下推导：D1：C{（R1，1）}（f{（R1，1）}（A{（R1，1）}）1）}），g{（R1，2）}（·））→1，R2 C{（R1，Λ）}（D{（R2，Λ）}，g{（R1，2）}（·））→2，R3 C{（R1，Λ）}（D{（R2，Λ）}，·）D2：C{（R1，1）}（f{（R1，1）}（A{（R1，1）}）1）），·）→1，R2 C{（R1，Λ）}（D{（R2，Λ）}，·）D3：C{（R1，A）}（f{（R1，1）}（·），g{（R1，2）}（B{（R1，2）}）。（1）→2，R3 C{（R1，Λ）}（f{（R1，1）}（·），B{（R3，Λ），（R1，2.（1））是D的次约化。现在，我们可以在项重写中引入依赖的概念。非正式地说，给定一个函数调用f（vn），它的计算结果是一个构造函数项v，我们说v的一个子项，比如s2，依赖于一个项s1（出现在程序中），如果• 存在形式为f（vn）→tt→tv的导数，其中s1是t和• 如果s1在t中被新符号·替换，则在所考虑的值v中不再计算s2的根符号。D. Cheda等人/理论计算机科学电子笔记177（2007）123131定义3.6（依赖性）给定一个程序P，构造函数项s2依赖于项s1w.r.t. P 的 函数f，在符号s1~fs2中，i ≠存在a132D. Cheda等人/理论计算机科学电子笔记177（2007）123X`形式f（vn）→t→ tv的推导，其中vn和v是构造项，t|p= s1，v|q= s2，且存在导数f（v n）→ t → v的一个子集tJ→vJ，其中tJ= t[·]p，使得根（vJ|q）/= root（s2）.例3.7再考虑例3.5的程序。这里，A~mainD，因为我们有一个推导¸D˛main→C（f（A），g（B））→C（D，g（B））→C（D，B）withC（D，B）|1= D，C（f（A），g（B））|1 .一、1=A，并且在D的下一个子节点中：C（f（·），g（B））→C（f（·），B）we具有（C（f（·），B））|1）=f D.请注意，我们在定义依赖性时并没有固定任何特定的策略。我们的目标是产生独立于任何评估策略的静态切片现在，我们介绍我们的静态切片方法的基本概念对于切片标准的定义，我们回顾切片模式的概念：定义3.8（切片模式[8]）切片模式的域Pat定义如下：π∈Pat ：：= ⊥ |不|c（πk）其中c/k∈C是元数k ≥ 0的构造器符号，k表示其计算不相关的值的子表达式，T表示相关的子表达式.切片模式类似于[7]中用于执行死代码消除的活性模式。基本上，它们是抽象的术语，可以用来表示构造函数术语的形状，忽略其术语结构的一部分。例如，给定构造函数项C（A，B），我们可以使用（除其他外）以下切片模式T，C（T，T），C（T，B），C（T，B），C（A，T），C（A，B），C（A，B），C（B，B），C（A，B），这取决于可用的信息和C（A，B）的相关片段给定切片模式π，抽象项的具体化通过函数γ形式化，使得γ（π）返回可以被从π通过替换所有出现的T和π由任何π- tor项。这通常会导致无限集，例如， γ（C（A，T））=γ（C（A，T））={C（A，A），C（A，B），C（A，D），C（A，C（A，A）），C（A，C（A，B）），. . }。定义3.9（切片准则）给定一个程序P，P的切片准则是一对（f，π），其中f是函数符号，π是切片模式。现在，我们引入静态切片的概念。 基本上，给定一个切片标准 （f，π），程序片是由程序中那些项的程序位置的集合给出的，这些项根据函数f的可能值的π来选择相关部分的计算。从形式上讲，定义3.10（切片）设P是一个程序，（f，π）是P的切片准则。设Pπ是π的位置的集合，其不寻址符号π。然后，切片D. Cheda等人/理论计算机科学电子笔记177（2007）123133关于Pw.r.t. （f，π）由以下程序位置集合给出：{（k，w）|（k，w）∈P，tP~fv|q，v∈γ（π）且q∈ Pπ}观察到切片是原始程序的程序位置的子集，其唯一地标识属于切片的程序（子）项例3.11再次考虑例3.5的程序和切片模式（main，C（T，C））.• C（T，B）的具体化为γ（C（T，B））={C（A，A），C（A，B），C（A，D），C（B，A），C（B，B），C（B，D），C（D，A），C（D，B），C（D，D），. . }。• C（T，n）的不寻址符号n的位置的集合是Pπ={Λ，1}。• 显然，只有C（D，B）∈γ（C（T，γ））的值可以从main中计算。• 因此，我们对这些项的程序位置感兴趣，使得C（D，B）（即，C（D，B）|A）或D（即，C（D，B）|（1）依靠他们。• 从main到C（T，T）的具体化的唯一计算（即，因此，从γ（C（T，γ））到 一 个 项 如下：D1：main{}→A，R1C{（R1，A）}（f{（R1，1）}（A{（R1，1）}）。1）}），g{（R1，2）}（B{（R1，2. （1）→1，R2C{（R1，Λ）}（D{（R2，Λ）}，g{（R1，2）}（B{（R1，2.（1）→2，R3C{（R1，A）}（D{（R2，A）}，B{（R3，A），（R1，2.（1））D2：main{}→A，R1C{（R1，A）}（f{（R1，1）}（A{（R1，1）}）。1）}），g{（R1，2）}（B{（R1，2. （1）→2，R3C{（R1，1）}（f{（R1，1）}（A{（R1，1. 1）}），B{（R3，A），（R1，2. （1））→1，R2C{（R1，Λ）}（D{（R2，Λ）}，B{（R3，Λ），（R1，2.（1））134D. Cheda等人/理论计算机科学电子笔记177（2007）123在该示例中，仅考虑其中之一，例如，第一个。 现在我想，为了计算现有的依赖关系，我们给出了D1的可能子集及其相关的子约简（这里，为了清楚起见，我们忽略了D. Cheda等人/理论计算机科学电子笔记177（2007）123135程序位置）：Su_x：C（f（A），g（B））→1，R2C（D，g（B））→2，R3C（D，B）细分：·C（f（·），g（B））→2，R3C（f（·），B）C（·，g（B））→2，R3C（·，B）C（f（A），g（·））→1，R2C（D，g（·））→2，R3C（D，·）C（f（A），·）→1，R2C（D，·）Su_x：C（D，g（B））→2，R3C（D，B）细分：·C（·，g（B））→2，R3C（·，B）C（D，g（·））→2，R3C（D，·）C（D，·）苏：C（D，B）细分：·C（·，B）C（D，·）因此，我们有以下依赖关系（我们只显示根符号的程序位置，因为这些是计算切片的唯一相关程序位置）：· 从第一个苏富比及其子约简：C{（R1，A）}（f（A），g（B））~mainC（D，B）A{（R1，1. 1）}~mainDf{（R1，1）}（A）~mainD· 从第二个苏富比和它的subreductions：136D. Cheda等人/理论计算机科学电子笔记177（2007）123C{（R1，A）}（D，g（B））~mainC（D，B）D{（R2，Λ）}~mainDD. Cheda等人/理论计算机科学电子笔记177（2007）123137FC一BFCG一BBBFIG。 四、f（C（A，B））与f（C（A，B），g（B，B））的定理·从第三个子集及其子约简：C{（R1，A）}（D，B）~mainC（D，B）D{（R2，Λ）} ~mainD因此，程序的切片w.r.t. （main，C（T，N））返回以下程序位置集 合{（R1，N），（R1，1），（R1，1. 1），（R2，N）}。显然，依赖于给定构造函数项的所有项的计算都是不可判定的。在下一节中，我们提出了一个可判定的近似的基础上构建一个图，近似的计算程序。4项依赖图在本节中，我们将概述一种新的方法，用于近似程序的依赖性，该方法基于称为术语依赖图的数据结构的构造。我们首先介绍一些辅助定义。定义4.1（树项）我们认为项通常用树来表示。形式上，项t的树项T是一棵树，其节点用t的符号标记，并且有向边从每个符号到其参数的根符号（如果有的话）。在此基础上，给出了f（C（A，B））和f（C（A，B），g（B，B））的关系。四、我们引入两个有用的函数来操作树项。首先，使用函数Termfrom nodes toterms来提取与子树相关联的项，该子树的根是树项的给定节点术语（T，n）=⎧nn，如果n在T⎩n（Term（T，nk）） 如果n在T中有k个孩子nk138D. Cheda等人/理论计算机科学电子笔记177（2007）123ABS主要(R1，/\）CF(R2，/\）G(R3，/\）(R1（1） F(R1（2）G一X(R1，(R1，A B图五、例3.5中程序的项依赖图现在，函数Termabs类似于函数Term，但用新的变量替换内部操作根的子项：⎧nn，如果n在T术语abs（T，n）=中文（简体）（T，nk）） 如果n在T中有k个孩子nk⎧如果你是一个功能强大的人，项Jabs（T，n）= ⎪其中x是新变量否则，术语abs（T，n）现在，我们可以最后介绍这一部分的主要定义。定义4.2（项依赖图）设P是一个程序。P的项依赖图构建如下：(i) P的所有左侧和右侧的树项属于项依赖图，其中这些树中的边用S标记（表示结构）;(ii) 我们从每个左手边的根符号到相应右手边的根符号添加标记为C(iii) 最后，我们添加一条边，标记为C，从规则右侧的树项Tr的每个节点n到规则左侧的树项Tl的最高节点m ，只要Termabs（Tr，n）和Term（Tl，m）统一。直观地说，术语依赖图为程序中的每个可能的计算存储了一条路径。 在[1]中引入了类似的数据结构，其中它被称为函数依赖图，用于检测不满意的[11 ]第11话，例4.3例3.5的程序的项依赖图如图4所示。五、 5在这里，我们将C箭头描绘为实线箭头，将S箭头描绘为虚线箭头。注意，只有规则右侧的符号标有程序位置。显然，对项依赖图的兴趣在于我们可以计算一个完整的从程序的项依赖图中提取程序切片通常，切片将5为了简单起见，我们不区分节点和这个节点的标签D. Cheda等人/理论计算机科学电子笔记177（2007）123139因为图是程序计算的近似，并且因此图中的一些路径在程序的实际计算中将不具有对应物。算法1给定程序P和切片准则（f，π），P的一个切片w.r.t.（f，π）计算如下：(i) 首先，根据Def计算P的项依赖图。4.2.例如，我们从图1的项依赖图开始5的程序。(ii) 然后，我们在图中识别对应于不寻址符号π的程序位置Pπ的节点N。为此，我们从标记有符号f的规则的左手侧的节点开始，并遵循其C路径（即，由C箭头构成的路径）。如果这条路径的最后一个节点是一个构造函数常数c，并且π=c或π=T，那么这个节点属于N。否则（即，它是一个以构造器为根的项），我们收集与π一致的所有最上面的构造器符号，并遵循从每个以最大运算为根的子项开始的C -路径，以便继续检查相关联的值。例如，给定图5的切片准则（main，C（T，N））和项依赖性图，对应于C（T，N）的不寻址符号N的程序位置的节点N在图5中用粗体框示出。六、(iii) 最后，我们收集• 在每个C路径中的节点的程序位置（与程序规则的右手侧相关联），该C路径结束于N的节点并且开始于f或者在路径中没有标记有f的节点• 上述节点的后代M的程序位置（即，沿着S箭头可到达的所有节点），以及• 从M可到达的节点的程序位置，C箭头、它的后代，依此类推，直到没有新的节点被收集。因此，在上面的示例中，切片将包含以下程序位置：• 与结束于具有粗体框的节点的路径相关联的编程位置（R1，Λ）、（R1，1）、（R2，Λ）• 其后代的程序位置，即，（R1，1. 1）;• 并且没有更多的程序位置，因为没有从标记为A的节点可到达的节点。简单地说，这个算法总是会终止。算法的完整性（即，根据定义3.10，切片的所有程序位置都被收集）可以通过显示所有可能的计算都可以使用项依赖图来跟踪来证明。然而，上述用于计算静态切片的算法是不正确的，因为在术语依赖图中可能存在C-路径，其在术语依赖图中没有对应物。140D. Cheda等人/理论计算机科学电子笔记177（2007）123主要GGBFF AB一一(R1，/\）C(R2，主要FDG(R3，/\）(R1，1）（R1，2）f g AX(R1，(R1，A B见图6。示例3.5中的程序切片图7.第一次会议。例4.4中程序的项依赖图原始程序的计算。下面的例子说明了这一点。例4.4考虑以下程序：（R1）main→g（f（A））（R2）g（B）→B（R3）f（A）→A图7中示出了相关联的术语依赖图。从这个项依赖图中，我们可以推断存在从main到B的计算，但这不是真的。5相关工作和讨论最近Rodrigues和Barbosa首次尝试将PDGs应用于功能范式[10]。他们定义了函数依赖图（FDG），它表示函数程序中的控制关系。然而，FDG的最初目的是在功能上程序并且因此它们仅考虑高级功能程序实体（即，他们考虑的最低粒度级别是函数）。在FDG中，单个节点通常表示一个复杂项（实际上是一个完整的函数定义），因此，关于其子项的控制依赖性的信息不存储在图中我们对术语依赖图的定义解决了这个问题，它将术语表示为树，从而考虑了较低级别的D. Cheda等人/理论计算机科学电子笔记177（2007）123141子项之间的控制依赖性的粒度如前所述，我们的术语依赖图与[1]的循环检查有许多相似之处粗略地说，[1]将函数依赖的有向图定义如下：对于每个规则l→r，存在从l到每个r的子项（其中内部参数被新变量替换）;还有，u箭头从R -箭头右侧的每一项添加到R-箭头左侧的每一项，并与之统一。通过这种方式，计算路径可以在函数依赖的有向图中遵循后来，[2]引入了相似关系（所谓的依赖对）的计算来分析项重写系统的终止性。至于未来的工作，我们计划正式证明算法1计算的切片的完整性。我们还希望在术语依赖图中识别和定义更多的依赖关系，以提高其精度w.r.t.定义3.6.然后，我们希望扩展框架以覆盖高阶特征。最后，我们计划实现切片算法，并将其集成到Curry切片器中[9]执行函数和函数逻辑程序的静态切片。引用[1] M.阿尔蓬特湾Falaschi，M.J. Ramis，and G.维达尔作为方程逻辑程序优化的窄化近似。Penjam和M.Bruynooghe，editors，Proc. of PLILPSpringer LNCS 714，1993年。[2] T. Arts和J. Giesl使用依赖对终止项重写。Theoretical Computer Science，236（1-2）：133[3] F. Baader和T.尼普科 重写和所有这一切。 剑桥大学出版社，1998年。[4] J. Ferrante、K.J. Ottero和J.D.沃伦程序依赖图及其在优化中的应用。ACM Transactions on ProgrammingLanguages and Systems，9（3）：319[5] J. Field和F. Tip.项重写系统的动态依赖性及其在程序切片中的应用。信息与软件技术，40（11-12）：609[6] D.J. Kuck，R.H. Kuhn，D. A. Padua，B. Leasure和M.沃尔夫依赖图和最优化。在第八届Symp。《程序设计语言原理》（POPL' 8 1 ） ， S I G P L A N 通 告 ， 第 2 0 7 - 2 1 8 页 ， 1 9 8 1 年 。[7] 是的Liu和S.D.斯托勒消除递归数据上的死代码。计算机程序设计科学，47：221[8] C. Ochoa，J. Silva，and G.维达尔基于Redex Trails的动态切片。在ACM SIGPLAN 2004年部分求值和程序操作研讨会（PEPM'04）134. ACM Press，2004.[9] C. Ochoa，J.Silva和G.维达尔通过动态切片实现轻量级程序专业化Curry和函数式逻辑编程研讨会（WCFLP2005），第1-7页。ACM Press，2005.[10] N.罗德里格斯和L.S.巴博萨通过程序切片进行组件识别。组件软件的形式方面（FACS 2005）。ElsevierENTCS，2005年。[11] J.R.斯莱格尔自动定理证明理论与简化，交换性和结合性。Journal of the ACM，21（4）：622[12] F. Tip. 程序切片技术综述Journal of Programming Languages，3：121[13] M.D.威瑟程序切片。IEEE软件工程学报，10（4）：352