函数式逻辑程序调试的一种方法及其实现

18理论计算机科学电子笔记64（2002）网址：http://www.elsevier.nl/locate/entcs/volume64.html38页函数式逻辑程序的一种编译方案1M. 阿尔蓬特2DepartamentodeSistemasInform'aticosyComputaci'on-DSIC瓦伦西亚技术大学，Camino de Vera s/n，46022 Valencia，Spain。F. J. Correa3信息系统和信息系统的合作伙伴UniversityEAFIT，Car re ra497S ur 50，3300M ede ll'ın，Colombia.M. Falaschi4数学和信息学系乌迪内大学，Via delle Scienze 206，33100 Udine，Italy。摘要我们提出了一个通用的计划，说明性调试的功能逻辑程序，这是有效的渴望以及懒惰的程序。 特别是，我们显示 该框架自然地扩展了以前的一些工作，并适用于最现代的懒惰策略，例如需要缩小。首先，我们关联到我们的亲-克语义的基础上（连续）的直接后果运营商，TR，模型计算的答案。 我们证明，给定程序R的预期规格，有可能通过TR的单个步骤来检查R的正确性。然后，我们考虑一种基于抽象解释的更有效的方法：通过近似成功集的预期规范，我们导出了一种有限终止的诊断方法，该方法可以静态使用，并且是参数w.r.t.选择的近似值。为了纠正错误，我们勾勒出一个初步的演绎方法，使用示例引导展开。我们专门研究w.r.t.的错误规则。在诊断过程中（自下而上）收集的肯定和否定示例的集合，从而排除否定示例的所有反驳和肯定示例的无反驳。我们的调试框架不需要用户提供错误症状提前或回答有关程序正确性的困难问题。我们扩展了我们的系统的实现需要缩小的情况下，并说明它通过一些例子，证明了我们的方法的实用性。1这项工作得到了CICYT的部分资助，资助号为TIC 2001 -2705-C 03 -01，由西班牙语-意大利语-西班牙语-西班牙 语-意大利语-西班牙语-2 电子邮件地址：alpuente@dsic.upv.es3电子邮件地址：fcorrea@eafit.edu.co4电子邮件地址：falaschi@dimi.uniud.it2002年2月出版，电子科学和B。 V. 操作访问根据C CB Y-NC-N D许可证进行。ALPUENTE，CORREA，FALASCHI19RIR1介绍函数式逻辑编程结合了函数式语言（高效，对于特定子类，最优求值策略）和逻辑语言（逻辑变量，内置搜索）的优点。集成语言的操作语义通常基于窄化，这是参数传递的统一和归约的组合，作为包含重写和SLD解析的评估机制。本质上，缩小由目标变量的实例化组成，然后是对实例化目标的缩减步骤。缩小在函数式编程（范式的计算）和逻辑编程（答案的计算）的意义上是完整的由于不受限制的缩小搜索空间巨大，已经提出了稳步改进的策略（参见[34]的调查）。发现程序错误是软件开发中一个长期存在的问题。然而，当前的调试工具不能充分地强制程序正确性，因为它们不提供在源代码中发现错误的手段w.r.t.预定的程序语义。在纯逻辑编程中，[24，23]定义了一个用于调试的声明式框架，它扩展了[29，47]中的方法，基于使用直接后果运算符TP来识别程序错误，诊断w.r.t.。计算答案该框架是独立于目标的在本文中，贡献之一是进一步发展的声明性诊断方法w.r.t.计算答案，将[24]的思想推广到函数逻辑程序的诊断[2]。我们还讨论了修改初始程序的错误组件的问题，形成实用的调试系统。[24]的推广远不是微不足道的，因为我们必须处理在处理（可能是非严格和部分）函数、嵌套调用和惰性求值时从建模计算答案中产生的额外复杂性。与[32]类似，处理部分函数和无限数据结构的可能性导致引入两个相等的概念，其特征在于两套程序规则。从语义的角度来看，与[24]中提出的声明性诊断方案相比，所得到的构造变得更加精细。我们将一个（连续）直接后果算子与我们的程序相关联，该程序模拟计算的答案，并使用两种等式。然后，我们表明，给定一个程序的预期规格，，我们可以检查（w.r.t.）计算的答案）通过单个步骤这个操作员。 我们对那些我们认为允许我们定义一个声明式调试的框架，它既适用于渴望（我们扩展了我们的系统的实现，并展示了如何将这种方法应用于现代非严格函数逻辑语言中的错误调试ALPUENTE，CORREA，FALASCHI20我我R将模式匹配编译成case表达式，并给出了一些实验基准。我们还提出了一个有效的方法，这是基于抽象的解释。我们近似成功集的预期规格。根据[24，23，20]中的启发，我们使用over和under规范+和−正确地超过-（分别为under-）近似于预期的语义。然后，我们将这两个集合分别用于函数在直接结果算子的前提和结果中，通过一个简单的静态测试，我们可以确定某些子句是否错误。最后，我们讨论了一个（初步）的方法来修复一些错误，这是基于程序专业化的例子引导展开。这项工作的初步版本出现在[2]。 本文推广和改进了文[2]中的结果。作为第一个改进，我们使我们的抽象诊断方法成为参数w.r.t.。评估策略，它可以是急切的（最里面的收缩）或懒惰的（最外面的收缩）。我们还更正了一些印刷错误，并澄清了一些要点w.r.t以前的版本。我们展示了我们的方法如何扩展到最佳评估策略，例如通过使用[36]中的Hanus和Prehofer我们的原型调试系统BUGGY已被扩展为与本文讨论的框架的不同实例一起工作，我们通过足够的例子来说明。该实现具有初步的归纳学习能力，我们的想法展开为此目的所需的正面和负面的例子是自动从预期的程序语义，其计算是我们的抽象诊断方法的一部分的过近似文件计划本文的其余部分组织如下。第2节简要介绍了一些初步的定义和符号，并回顾了实现所需缩窄的一些技术。第3节回顾了一个一般性的直接后果算子TR 对于函数逻辑程序R，它是参数w.r.t.的缩小战略范围，可以是渴望的，也可以是懒惰的，并制定了一个计划，一个允许定义一个实现的过程，需要缩小。然后，我们定义了一个基于T的定点语义R 这正确地模拟答案和值计算的窄，其中使用缩小战略范围。 我们还制定了一个操作语义，我们展示了与最小定点语义的对应关系。在第4节中，我们介绍了不正确和不安全症状以及未覆盖呼叫的必要一般概念。第5节提供了一个抽象语义，它正确地近似了的定点语义。在第6节中，我们介绍了我们的抽象诊断方法。第7节讨论了如何在我们的框架中加入一些纠正错误的初步技术。第8节描述了该方法的原型实现。 第9节结束ALPUENTE，CORREA，FALASCHI21∪{|∈}T≡我们还包括一个附录，在那里我们展示了我们的pro-totype实现，Buggy的调试会话。更多的细节和缺失的证据可以在[3]中找到。2预赛让我们简要回顾一下关于重写系统[13，38]和函数逻辑编程的一些已知结果（参见[34，37]进行广泛的调查）。为了简单起见，定义是在单排序的情况下给出的。对多排序签名的扩展很简单，参见[45]。在本文中，V将表示一个可数无限的变量集，而X表示一组函数符号或签名，每个符号都有一个固定的关联元。τ（τV）和τ（τ V）表示非基字（或项）代数和建立在其上的字代数分别为0.05和0.05τ（τ）通常称为τ上的Herbrand宇宙（Hτ），记为H。B表示Herbrand基，即可以用H的元素建立的所有基础方程的集合。一个π-方程s=t是一对项s，t∈τ（ππV）或真。术语通常被看作是有标签的树。位置由表示项中的访问路径的自然数序列表示，其中Λ表示空序列。O（t）表示项t的不变位置的集合。 不|u是t的位置u处的子项。 t[r]u是术语t，其中位置u处的子项替换为r。这些概念延伸到一系列自然的方程式。例如，方程序列g（ e1，.，可以这样定义：O（g）= i.uO（e i），i = 1，.，n.我们用这个符号作为通用表示形式为true，...， 真的我们用V ar（s）表示语法对象s中出现的变量的集合，而[s]表示集合s的地面实例。一个新的变量是一个在其他地方都没有出现的变量。一个代换是从变量V的集合到项τ（V）的集合的映射。换元θ比σ更一般，记为θ≤σ，如果对某些换元γ，σ = θ γ。 我们写θ|s表示替换θ对语法对象s中变量集的限制。的空替换由k表示。一个重命名是一个置换ρ，其中存在逆ρ−1，使得ρρ−1=ρ−1ρ=ρ。 一个集合方程E是可唯一化的，如果存在使得对于E中的所有s=t，我们有s t，并且称为E的唯一化器。我们让mgu（E）表示方程组E的最一般单位元[41]。我们写mgu（{s1= t1，.，Sn= tn}，{sJ1 =tJ1， . ，sJn=tJn}）来表示方程组的最一般单位{s1= sJ1，t1= tJ1， .. . ，sn= sJn，tn= tJn}。条件项重写系统（简称CTRS）是一个对（R，R），其中R是一组有限的归约（或重写）规则方案，其形式为（λ→ρ∈C），λ，ρ∈τ（τ∈V），λ/∈V和Var（ρ）<$Var（λ）。条件C是一个（可能是空的）序列e1，...， e n，n ≥ 0，我们处理的方程ALPUENTE，CORREA，FALASCHI22RR∈ D萨尔河⇐R→RC\DC V→ R ∈R}RR∈不当我们发现它是方便的时候， C中的变量， 不出现在λ中的变量称为额外变量。我们经常会用（）来代替（），）.如果重写规则没有条件，我们写λρ.一个目标是一个方程C的序列，也就是一个没有头（结果）的规则。我们通常会忽略当我 们 写 进球时，我会很高兴。对于CTRS，r<<表示r是规则的新变体，使得r仅包含新变量，即不包含先前在计算期间遇到的变量（标准化分开）。给定一个CTRS（R，R），我们假设签名R被分成两部分，不交集n=C ≤ D，其中D={f|（f（t1，.，t n）RC）和= Σ. 符号中称为构造函数和符号，被称为定义的功能。τ（）的元素称为构造函数项。模式是f（d <$）形式的项，其中f/n和d<$是构造函数项。我们说CTRS是基于构造器的（CB），重写步骤是将重写规则应用于表达式。如果存在u∈O（s），（λ→ρ∈s1= t1，.，Sn= tn）∈ R，和置换σ使得s|uλ σ，t∈s [ρσ] u，且对于所有i∈ {1，.，n}存在项wi使得si→wi而ti→wi，其中→是→RR. 当为了避免混淆，我们省略下标R。项s是一个标准形式，如果没有项t，则s→Rt。 如果由R定义的二元一步重写关系→R是诺特的且是连续的，则称程序R是规范的[38]。一个CTRS R是诺特的，如果不存在形式为t1→Rt2→Rt3→R.的无穷序列。一个CTRSR是连续的，如果当一个项s减少到两个项t1和t2时，t1和t2都减少到同一项。函数逻辑语言是函数语言的扩展，其原理来自逻辑编程[46]。函数逻辑语言的计算机制基于窄化，这是项重写的一种推广，其中统一取代了匹配：重写规则和要重写的项都可以实例化。由于不受限制的缩小有相当大的搜索空间，已经开发了几种控制Redexs选择的策略。缩小策略（或位置约束）是任何定义良好的标准，通过允许缩小以减少某些选定的位置来获得更小的搜索空间。缩小策略可以形式化为一个映射，该映射将O（g）的子集f（g）标记为每个目标g（与之不同），使得对于 所有uf（g），则目标g在位置u处是可缩窄的。 一个重要性质收缩策略的关键是完整性，这意味着由收缩约束的收缩仍然是完整的。函数式编程中有一个继承的权衡，在由外而内的正交、非终止规则的求值和由内而外的非终止规则的求值之间。关于缩小策略完整性的结果调查见[12，11，25，26，34]。为了简化我们的符号，我们让IR表示满足条件ALPUENTE，CORREA，FALASCHI23++≈R∈{}--∈ F ∈ C为了战略的完整性，我们让客栈（g）（resp. out（g））表示窄化策略，该窄化策略分配最左边-最里面（resp.最左-最外）将g的redex缩小到目标g。5我们用策略n，n∈ {inn，out}制定一个条件窄化，作为满足以下条件的最小关系n，u=<$（g）<$（λ→ρ<$C）R<$ σ=m gu（{g|u=λ}） .g<$σ（C，g[ρ]）σ拉乌对于R∈ {inn，out}，R∈=R ∈ {Eq∈}，其中Eq∈是建模的规则条件上的平等也就是说，Eqout是一套规则，它将方程的有效性定义为：当计算可能不会终止时，项之间可能存在严格的相等[43]：cc→true%c/0 ∈Cc（x1，...，x n）{\displaystyle\sqrt（y1，.，y n）→（x1<$y1）<$. n（xn<$yn）%c/n∈ C真x→ x而Eqinn是标准等式，定义为：x=x→true%x∈ V我们还假设，当我们考虑n=inn时，g和C中的方程具有s = t的形式，而当我们考虑n = out时，方程具有s t的形式。注意，当f（a）=out时，像f（a）= g（a）这样的非严格方程是不可接受的目标。在下文中，这种区别将通过使用=来表示当= inn时项的标准相等性=来明确，而当不存在时，=是。对g的一个成功的推导是推导g计算的答案替换（对于R中的g）。❀θ∗ θ被称为a在[49]中，它表明，无论是内部还是外部一般都不是完全的。例如，考虑R={f（y，a）→true，f（c，b）→true，g（b）→c}，其中输入目标f（g（x），x）= 0. 然后最里面的窄化只计算f（g（x），x）= true的答案x / b，而最外面的窄化只计算所考虑的目标f（g（x），x）true的x / a。对于在策略n=inn，out下的缩窄的完全性，需要以下一致性条件[25，26，31，34，45]：当n选择的位置对于应用于它的所有正规形式的替换都是n的有效缩窄位置时，一个连续程序是一致的。注意，上面的程序不满足一致性原则，因为f（g（x），x）项的顶部位置不是一个有效的缩窄位置。5最里面的项是应用于构造器项的操作，即，形式f（d1， . ，dk）， wheref并且对于所有i=1， . ，k，di（（五）。g的最左-最内位置是指g的最左位置指向最内的子项。一个位置p是一组位置O中的最左最外位置，如果不存在p′O，且p′前缀为p，或p′= q.i.q′和p = q.j.q′′和0。ALPUENTE，CORREA，FALASCHI30Rϕϕϕ⊥⊥ϕFRϕRFRFROR出来FRϕORRϕR1nn+1个1nϕn+1个ϕ其中n∈ω。 给定目标g <$（first（from（s（x）<$z），最外层窄化只计算答案{z/s（x）}，这也是唯一可以通过在F ca（R）中统一目标g<$（from（s（x））= y，first（y）=w，w<$z）来计算的替换。根据定理3.9，ca（）可以用来模拟任何（非平凡的）目标g的执行还要注意的是，在我们的表示法中，等式l=r的正确语义只有在r是全的情况下才是相等的，即，而不发生任何故障。粗略地说，在我们的方法中，k被用作伪像，以允许任何方程g（x1，...， x n）= x以“成功”（在表示中“计算”时）。 这通过简单地将其与额外的（“假”）方程g（x1，.，x n）= .这确保了每个在其rhs中有纯变量的（非严格）方程都是可解的，这是完备性所必需的。例如，考虑下面的例子[32]。令f（t1，..，t m）是出现在规则体或目标中的项，并假设f不依赖于（不严格）第i个参数。根据定义，如果t i是函数项g（x1，...，xn），则该方法引入方程g（x1，...，xn）=目标中的x（并且在f（t1，...，t m））。我们必须允许这个方程g（x1，...，x n）= x，当x的值不需要时，其他方程，因为它代表f的第i个参数。粗略地说，通过规则g（x1，.，xn）=具有“反转”否则将强制对调用g（x1，...，x n）并且可能失败（例如，如果g是unfined），而f不需要求值，并且是不期望的。在下文中，我们示出语义ca（）和新的操作3.2成功集语义一个程序的操作成功集语义ca（）w.r.t.如以下定义所示，通过考虑为“最一般的调用”计算的答案来定义窄化语义定义3.11设R是IR中的一个程序。然后，θ∗Oca（R）= O {f（x，...，x）= x）θ| (f (x ,..., x）=x）T其中f/n∈ D，xn+1和xi是不同的变量，对于i = 1，.，n}。下面的辅助操作员正在进行中（S）是有帮助的。inprogress（S）选择S的那些不对成功计算建模的方程，即仍然不完整或不终止的ALPUENTE，CORREA，FALASCHI31ϕϕORFRϕϕϕ拉克索河FRF R FRϕ我ϕϕϕϕϕϕϕCA定义3.12设S是一组方程，λ是所考虑的信号。我们定义：inprogress（S）={λ = ρ∈S| ρ出现在ρ中，或ρ包含定义的函数符号根据定义，inprogress（ca（））=。下面的结果总结了程序的操作表示和定点表示之间的关系定理3.13下列关系成立：Oca（R）=F（R）−inprogress（F（R））为了清楚起见，让我们总结一下本文中引入的三种不同的程序表示F_n（R），F_ca（R）和O_ca（R）科.通过计算直接结果运算符T的lfp，可以获得对成功和部分（中间和非终止）计算进行建模的组合定点语义（）。R表示F_∞（R））是计算答案（fixpoint）语义ca（），它是通过删除模拟中间计算的方程（即那些方程f（t<$）=s，其中s“尚未达到其值”）而从f（）获得的，并且是唯一允许我们通过简单地将flat（g）与表示中的方程统一来运行（非平凡）目标g的语义。请注意，01- 02 ）仍然对非终止函数建模，表示为。最后，操作成功集语义ca（）只捕获成功的派生，也就是说，它只对计算出的可观察答案进行建模。因此，我们有Oca（R）<$Fca（R）<$F<$（R）。4函数逻辑程序的声明式诊断我们现在介绍一些关于陈述性程序诊断的基本定义[24]。作为操作语义，我们考虑成功集语义。由于我们考虑了两个不同的语义Oca（R）和F_（R）， 我们还区分了两种不同的意图语义：Ica和IF。 虽然我可以是从程序员的角度来看的引用语义，F适合于技术原因[20]，我们在下面解释下图1总结了我们的第一个定义。定义4.1设I可以是R的预期成功集语义的规范。(i) R是部分正确的w.r.t. Ica，ifO（R）Ica.(ii) R是完全的W. R. T。我可以，如果我可以的话。(iii) R是完全正确的。Ica，如果Oca（R）= Ica.如果一个程序包含错误，这些错误将由相应的符号发出信号。ALPUENTE，CORREA，FALASCHI32ϕϕϕII II I− IRRR的部分正确R的完备性Oca（R）Ica图1.一、 R w.r.t. 计算答案一个原子方程的一个简单的语义学。定义4.2设I可以是R的预期成功集语义的规范。一个不正确的征兆是方程e使得e∈Oca（R）和e/∈ Ica。一个不完全征兆是一个方程e使得e∈Ica和e/∈Oca（R）。然而，为了诊断，我们需要考虑一个“良好提供的”意图语义F（例如ca F），它对成功的和“进行中的”计算进行建模，并享有定义3.7中形式化的指称的语义属性，即I F应该对应于正确程序的定点语义，ca = F inprogress（F）。在实践中-当然，这些描述不会由用户提供但它会自动从一组有限的输入方程中推断出来例如，程序的可能不正确（正确）版本，或（可执行）规范。这就是我们在第5节提出的抽象诊断方法学中所遵循的方法。在错误的情况下，为了确定错误的规则，以下定义将是有用的。定义4.3设IF是预定定点语义的具体化对R.若存在方程e∈T∈（IF）且e/∈IF，则规则r∈ R不正确的是e。 我们还说，{r}不正确地被R覆盖。因此，规则r的不正确性通过意图语义IF的简单变换来表示。定义4.4设IF是R的预定定点语义的规范。如果e∈IF且e/∈T∈（IF），则方程e是未解的.通过上述定义，如果方程e不能通过任何使用预定定点语义的程序规则导出，则方程e是未覆盖的。然而，我们通常感兴趣的是未被揭示的IcaIF的方程，即。e∈ Ica和e/∈ T（IF）。IcaO（CAϕ 右）ALPUENTE，CORREA，FALASCHI33RRIIFFO出来F R FRderivR命题4.5如果在指定预定的定点语义时没有不正确的规则，那么在指定定点语义时是部分正确的。预期的成功集语义。命题4.5给出了一个简单的方法来证明部分正确性。完整性更难：一些不完整性不能通过比较预定定点语义和T_n（）的指定来检测。的是的，没有未转换的方程并不意味着我们都e表示程序已完成。让我们考虑下面的反例：例4.6考虑f（x）= out，程序R ={f（x）→ a f（x）=a}和规范IF={af（x）=f（x），f（x）= a，f（x）=a}。则R是不完全的，因为Ica∈ Oca（R）={}。然而，IFTout（IF）={aa，f（x）=f（x），f（x）=f（x），f（x）=a}，并且没有未覆盖的方程。这个问题与TR的多个不动点的存在性有关操作符. 详情请参见[24]5抽象语义在本节中，从第3节中的定点语义开始，我们开发了一个抽象语义，它近似于程序的可观察行为，并且足以进行模块化数据流分析，例如方程组的不满足性分析或任何基于程序成功集的分析。我们假设[5]中定义的分析方程不满足性的抽象解释框架另一种构造抽象项重写系统的方法在[16]中遵循。我们认为，上一节中给出的定点语义的另一种近似与我们在本节中描述的不同，可以通过遵循类似于[16]中的方法我们回忆一下以前关于抽象域和相关