基于表达式类型的程序验证方法及其在编程环境中的应用探索

理论计算机科学电子笔记174（2007）129-147www.elsevier.com/locate/entcs基于表达式类型的Martin Sulzmann1新加坡国立大学计算机学院S16 Level 5，3 Science Drive 2邮编：117543Razvan Voicu2新加坡国立大学计算机学院S16 Level 5，3 Science Drive 2邮编：117543摘要表达类型领域的最新发展有望为普通程序员提供一种足够丰富的编程语言来验证复杂的程序属性。程序验证可以通过易处理的类型检查来实现。我们通过考虑两个具体的例子来探索这种可能性：验证排序和资源使用验证。我们表明，先进的类型错误诊断方法成为必不可少的，以协助用户在类型检查失败的情况下。我们的研究结果指出了新的研究方向，开发的编程环境中，用户可以编写和验证他们的程序。关键词：类型推断，类型错误报告，验证排序，资源使用验证1引言程序验证是一个成熟的研究领域，包括大量的方法和技术来保证有用的，有时甚至是关键的程序属性。然而，到目前为止，似乎还没有一个很好的解决方案，将程序验证技术应用到工业级软件开发过程中。造成这种情况的主要原因之一是程序员必须切换到外部工具，例如证明助手，以执行经常交互的验证过程，例如。考虑基于类型的形式化推理工具，如Coq [3]，LF [10]和第1Email:sulzmann@comp.nus.edu.sg2Email:razvan@comp.nus.edu.sg1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.041130M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129[22].到目前为止，它们集成到编程语言中只达到了编程语言的用户不能直接从她最喜欢的编程语言中访问它们。另一方面，基于类型的自动检查方法已经进入了今天的现代编程语言。到目前为止，类型已成为程序设计和实现中不可或缺的一部分，并被用户广泛接受。有许多作品展示了如何通过ML [19]和Haskell [20]等语言中的一些巧妙的类型编码来捕获数据不变量。特别是，表达类型扩展，如具有函数依赖关系的类型类[13]（或变体[6]）和广义代数数据类型（GADT）[5，40]3，表明有可能为普通程序员提供足够丰富的类型语言来指定任何感兴趣的属性在本文中，我们探讨了EADT（扩展代数数据类型）[32]，一个以前介绍的扩展GADT与用户可定制的约束域，可以用作一个系统的方法，程序验证。有很多其他作品[7，16，25，39]共享相同的目标。我们的工作是不同的，我们应用先进的类型检查和类型错误诊断方法的组合来验证（或反驳）复杂的程序属性。具体而言，我们的贡献包括：• 我们探索类型错误诊断方法，以帮助用户在类型检查失败的情况下（第2.3节）。• 我们探索通过几次试验和（类型检查）错误来验证排序（第3节）。• 我们用EADT为一个简单的while语言实现了一个静态的资源使用验证分析。此外，我们应用类型类解析机制来支持静态和动态验证的混合（第4节）。在第2节中，我们提供了EADT的背景材料。我们将在第5节结束，并讨论相关的工作。我们假设对类型类有一定的了解[38，11]。在本文中，我们将在示例中使用Haskell风格的语法我们将看到一些使用现有实现（如GHC [9]）的类型检查示例其他的则需要一种实验性的语言，比如Chameleon [31]，或者仅仅在纸上进行类型检查。我们希望在不久的将来，本文中的所有示例都能被Chameleon的修订实现所接受2扩展代数数据类型我们给出了一个简短的概述Hindley/Milner的扩展与用户可定义的原始约束，类型注释和代数数据类型的扩展形式（松散地称为EADT）。我们这里的重点是如何声明EADT以及如何执行类型检查[32]。[33]中给出了程序的语义描述及其类型可靠性证明3 GADT也被称为守护递归数据类型或第一类幻影类型。M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）1291312.1扩展数据类型声明为了说明EADT，我们考虑经典的append程序。我们的目标是表达这样一个性质，即两个列表相加产生一个长度为两个输入列表之和的列表。特殊用途的系统，如Xi的DependentML [ 42 ]或Zenger的索引类型[ 43 ]可以很容易地我们表明，我们可以通过EADT模仿这样的系统。在第一步中，我们引入GADT来建模长度索引列表。我们遵循GHC中的GADT符号[9]。dataZ = Z -- singleton类型Zero和dataS x= Sx-- SuccessordataList a n whereNil：：List aZ缺点：：a-> List am-> List a（Sm）GADT是（盒装）存在类型的扩展[14]，并允许通过语法类型等式来细化构造函数然后，这些类型假设可以用于对模式子句的主体进行更准确地说，给定一个表达式我们可以将e的类型更改为tJ，如果我们可以验证在类型假设C（即类型等式和诸如类型类之类的其他原语约束的结合）类型t和tJ相等。我们将很快看到应用这种推理的例子。我们的下一个任务是找到一个合适的（类型）加法编码。为此，我们引入了一个三元（类型）约束符号和表示类型级别数之间的加法。在EADT系统中，约束的含义是用户可通过约束处理规则（Constraint Handling Rules）定义的[8]例如，以下规则编码了一些常见的算术定律。规则Sum a bc，Sum a b d ==> c=d--（FD）规则Sum Z a b ==> a=b--（I1）规则Sum（Sa）b d ==> d=Sc，Sum a b c--（I2）逻辑上，==>表示布尔蕴涵，<==>表示布尔等价。规则头（右侧）中的变量是普遍量化的，而右侧的所有剩余变量都是存在性量化的。CHR也在约束之间的重写方面具有简单的可执行语义（从左到右）。规则==>传播信息，而规则<==>执行简化。下一节中给出了计算器推导步骤的示例规则（FD）规定Sum必须表现得像一个函数。也就是说，它的前两个（输入）参数唯一确定最后一个（输出）参数。规则（I1）有效地说明0+a=a，而规则（I2）说明（a+1）+b=（a+b）+1。 这些规则实际上就是皮亚诺公理，因此提供了类型加法的完备公理化。我们将在接下来的2.3节中回到这个问题。我们将现有的部分粘合在一起，并按如下方式细化append的类型append：：Suml mn =>List al-> List a m-> List a n132M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129追加Nil ys = ysappend（Cons x xs）ys = Cons x（append xs ys）实际上，我们已经通过GADT和CHR的组合编码了索引类型但是，程序文本似乎与类型注释相例如，在第一个子句中，我们返回类型为Lista m的ys。 这与annotation声明结果值的类型为Lista n。重要观察到的是，我们需要考虑由模式匹配Nil产生的总之，Sumlmn和l=Z意味着m=n通过规则（I1）。因此，我们可以将ys的类型更改为Lista n。关键点在于，因此，第一个子句类型正确。类似的推理也适用于到第二条。根据我们的经验，CHR对于表示约束属性非常有用文献[41，7]中提出了类似的机制。例如，在Omega语言[24]中，上述CHR可以使用相关的类型表示法[6]类型sum：：*->*->*sumZm=msum（Sl）m= S（sumlm）也就是说，Omega使用函数而不是关系样式来指定类型条件。我们可以很容易地通过适当的编码来支持这样的源代码级符号到我们的内部编译器语言（这是图灵完备的）。此外，我们可以通过指定规则（如规则SumInta b ==>False）和其他更复杂的改进条件来强制执行总体性。一些不可能的事情当使用函数式书写类型条件时。此外，通过CHR，我们可以表达具有扩展的类型类，例如多参数类型类和函数依赖[26]，这些在其他系统中没有处理[41，24]。2.2类型检查我们简要地看一下如何对EADT执行类型检查。 我们假设函数都提供了类型注释。标准的方法是将类型问题转化为约束问题。与标准Hindley/Milner相比，我们需要更丰富的蕴涵约束集。这样的约束是必要的，因为我们需要在不同的局部类型假设（由GADT和类型注释上的模式匹配引起）下对不同的程序部分进行类型化例如，如果append：：Suml mn =>List al-> List a m-> Lista n append Nil ys =ysappend（Cons x xs）ys = Cons x（append xs ys）M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129133.我们生成以下内容拉，l，m，n。不客气。 （Sum l m n t = List a l → List a m → List a n） （1）！（l=Zt=List a l→List a m→List a m）吉尔·J （l=Slj（SumlJmnjt=Listal→Listam→Lista（SnJ））这里我们使用一些标准的一阶逻辑符号，例如：布尔合取（Boolean conjunction）和布尔蕴涵（Boolean implications）。外部含义的（下划线）右侧对应于注释，而（双下划线）右侧对应于注释。内部含义的两侧对应于由模式匹配产生的GADT类型方程。上面的隐含约束可以通过使用以下定律进一步简化： C1<$（ C2<$C3）i<$C1<$C2<$C3：（Leba，l，m，n. 不客气。（（Sum l m n，t = List a l→List a m→List anl = Z）t=List a l→List a m→List a m））（Leba，l，m，n. 不客气。吉尔·J （（Sumlmn，t=Listal→Listam→Listanl=SlJ）（Sum lJm njt=Listal→Listam→Lista（S nJ）一般来说，类型化问题可以表示为一个表达式1的蕴涵constra ints的连接。一号... a;[咒语] （C1<$C2）其中C1和C2是基元约束的集合。泛量化产生于多态类型，不 适 用 （ 例 如 ，m ， n ） ， 并 且 存 在 所 有 的 数 据 类 型 （ 例 如 ，（ J ） 。Existentialquantification的出现是为了表示类型注释的类型组件（例如，xdt）和Hindley/Milner约束产生的中间变量（我们将看到在本节末尾有这样一个例子）。我们的任务是检查在给定的CHR下每个单独的约束是否成立（与类型推断相反，我们可能需要计算一些缺失的假设）。利用C1<$C2i <$C1ParticipateC1<$C2的规律，将蕴涵检验问题转化为等价性检验问题。我们可以通过对C1和C1<$C2穷尽地应用CHR来测试C1ParticipC1<$C2是否成立，并检查所得到的约束是否具有相同的对于M。 因此，我们需要确保满足以下条件：1. 一号... a; 你不受人尊敬。这个过程如何工作的确切细节在[32]中给出例如，考虑上面的以下含义约束（Leba，l，m，n. 不客气。（（Sum l m n，t=List a l→List a m→Listanl=Z）t=List a l→List a m→List a m））（一）我们发现，Sum l m n，t=List a l→List a m→List anl=Z>I1t=List a Z→List a m→List aml=Zm=n⑵134M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129也就是说，我们应用上面的I1，并通过构建最一般的unier来规范化约束同样，我们得出结论，Sum l m n，t=List a l→List a m→List anl=Zt=List a l→List a m→List a m>I1t=List a Z→List a m→List aml=Zm=n（3）因此，最终约束（2）和（3）是等价的。 因此，陈述（1）成立。这种类型检查程序是合理的。如果我们能保证CHR被终止，那么决定性就随之而来。也就是说，在每个（初始）约束上，我们只能应用有限数量的约束重写。在传播规则的情况下，我们通过小心不要在相同的约束上两次应用传播规则来避免无限的重新传播。有关避免重新传播的更多详细信息，请参见例如[1]的文件。完整性取决于两个因素。首先，我们需要保证每个约束都有一个规范范式。对于任意的人权中心来说，情况不一定如此例如，考虑一组非连续的CHR，其中对同一约束的不同规则应用导致不可连接的约束。其次，我们需要防止约束求解器猜测类型。这可能发生，因为一些变量是存在性量化的。这里是一个（人为的）例子，我们使用多参数类型类[21]，这是EADT系统的一个实例。classBar ab where bar：： b->IntdataFoo awhereMk：：Bar a b =>Fooa g：： Fooa->Intg（Mk x）= bar x类型检查器面临以下隐含约束。你好不客气。（t = Foo a→Intt t）（酒吧a bb bc。横杠c（b））约束条件是：Bar c b在我们为bar：：bar a，b构建一个（通用）类型实例时，由程序文本bar x产生。Bar abb→Int. x的参数类型绑定到a。但是，类型类Bar中的第一个参数不受任何给定的类型。根据Hindley/Milner的推论，这些类型是存在约束的。为了验证上面的隐含约束，我们需要猜测c等价于a。但是，猜测正确的类型通常可能是不平凡的类型检查器，分别是它们的底层约束求解器，都是确定性过程。因此，我们永远不必猜测类型。事实上，在类型类上下文中，上述程序被认为是非法的。在那里，猜测类型可能意味着程序的语义含义是模糊的（例如，[12，26]更详细。以上说明，猜测类型也很难得到一个完整的类型检查程序。我们可以通过强制执行M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129135一些（保守的）模糊性检查，因此，拒绝bar：：a，b。因为变量a不受类型b→Int的约束。或者，我们可以应用一个更自由的策略，并运行蕴涵求解器，直到我们达到一个在这种情况下，我们需要猜测类型。本质上，类型系统是由类型检查算法定义的。2.3类型错误诊断虽然从理论上讲，研究类型检查完成的程序类是很有趣的，但在实践中，向用户提供详细的反馈更重要，为什么程序没有通过类型检查器。类型检查失败可能有几个原因。例如，考虑程序文本头True，它导致不满足的约束th= [a]→a[a]=Bool。在以前的工作[28，29]中，我们已经展示了如何从最小的不可满足约束中生成类型错误消息这些约束可以是追溯到它们产生的特定来源位置。因此，一个最小的不可满足约束代表了一个类型错误的可能（最小）解释。在EADT的情况下，可能会出现故障，因为我们无法验证隐含约束是否成立。在上面的例子中，我们无法验证B. （酒吧a bb bc。条形图cb）实际上，约束Bar c b保持“不匹配”。在这里，我们将看看在应用EADT进行程序验证的背景下，隐含失败的原因。我们的讨论大多是非正式的。在[37]中给出了我们的类型错误诊断方法的技术方面的综合说明考虑一下我们前面看到的一个例子的变化。规则Sum a bc，Sum a b d ==> c=d--（FD）规则Sum Z a b ==> a=b--（I1）规则Sum（Sa）b d ==> d=Sc，Sum a b c--（I2）append：：Sum l m n => Listal->Lista m->Lista n appendNil ys = Nil--wrong！append（Cons x xs）ys = Cons x（append xs ys）请注意，在第一个子句中，我们错误地返回Nil而不是ys。这是无法验证的结果蕴涵约束。（ Leba ，l， m ，n. 不 客气。（（ Sum l m n， t=List a l→List a m→Listanl=Z）t=List a l→List a m→List a Z））问题的要点是，对于某个m（1），Sum l m n<$l=Z/<$n=Z。我们显然违反了类型注释，除非第二个列表为空。也就是说，136M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129Sum l mnl=Zm=Zn=Z成立（2），但Sum lmnl=Zm=S mJ/n=Z成立（3）。根据这些信息，我们可以立即报告静态类型错误。Chameleon类型的调试器[27]将大致报告以下内容错误：多态类型变量由数据List a n实例化，其中Nil：：List aZ...append：：Sumlmn =>List al-> List a m-> Listan append Nil ys =Nilappend（Cons x xs）ys = Cons x（append xs ys）将突出显示错误中涉及的程序部分此错误消息提供了程序文本违反注释的详细线索。如果CHR“不完整”，也可能出现静态故障。这里是我们运行示例的另一个变体，我们将规则（I1）替换为（规则Sum a bc，Sum a b d ==> c=d--（FD）规则Sum a Z b ==> a=b--（List al-> List a m-> Lista n append Nil ys =ysappend（Cons x xs）ys = Cons x（append xs ys）第一个子句产生（简化的）蕴涵约束Sum l mnl=Zm=n（4）。这里的问题是规则（一个可能的解决办法是把（4）变成一个“公理”。也就是说，我们引入额外的ruleSum Zmn ==> m=n--（I1）然后，对上述程序进行文本类型检查。当然，我们需要确保规则（I2）的添加不会违反CHR结果集的一致性对于CHR，我们可以通过检查CHR是否一致来测试一致性。连续性保证了任何顺序的重复应用都将达到相同的最终约束。在终止CHR的情况下，存在可判定的一致性检查[1]。因此，我们可以验证规则（FD）、（I1）、（如果我们不能确定CHR的终止，我们不能应用机械连续性检查，必须依赖3分类我们的目标是使用EADT系统来表达和验证排序使用插入排序算法。我们把注意力集中在整数列表整数有单例类型，例如。1类型为Int（1）等等。我们假设底层约束求解器M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129137的基本约束（.& lt;=.）、（.& lt;.）在类型级别上比较整数。4GADT测试和原始函数测试允许我们“测试”比较两个数据测试a b =（a< b）=> Le|（a>=b）=> Gt test：：Int（a）->Int（b）->Test a b3.1第一次尝试我们引入了一个GADTSList来描述排序列表，以最直接的方式。--singletonlistsdataN数据Ca作为--排序性质rule SortedN ==> TrueruleSorted（C a N）<==> Truerule Sorted（C a（C b bs））<==>a =b，Sorted（C b bs）--sortedlistsdataSList as where无：列表N缺点：：Int（b）-> SList bs -> SList（C bbs）插入排序算法是根据下面给出的插入操作定义的。insert：： Int（a）->SListbs->SList插入x无=缺点x无CSinsertx（Cons y ys）=case（testx y）ofLe -> Cons x（Cons y ys）（一）Gt-> Cons y（插入 x和ys）（二）注释声称，给定一个有序列表，我们将返回一个有序列表。但是，上述程序不会进行类型检查。为了理解为什么，让我们考虑由最后一个子句（1）和最后一个情况（2）产生的蕴涵约束。我们用注释对公式进行注释，以显示哪个约束来自哪个程序138M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129[4]或者，我们可以添加一组全面的约束规则来指定这些约束的含义M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129139⎜⎝⊃⎜⎟⎜⎝⎠⎟⊃⎜⎟⎜⎟⎟⎟⎜⎟⎟⎜⎟⎜⎟⎟零件.A，B，C，S不客气。b.s.J.⎛⎛ ⎞⎞Int=Int（a）→SList bs→SListcs⎜⎜ ⎟⎟插入- - insert：：Int（a）->SList bs->SList cs插入⎜ ⎟⎜⎜J J⎟⎟bs=C b bs⎜排序的bs-- insertx（Cons yys）排序⎠⎟a>=bJ-- Gt->⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟是的，是的。（t=Int（a）→SList ds→SListes⎝ ⎠es=C bJ DS（已排序的es）--Cons y（插入x ys）问题现在变得很清楚了。注释声明输出列表可以是任何排序列表（甚至是空列表），而程序文本的约束声明这个列表是非空的。以下是此错误涉及的（最小）约束。阿利茨湾J.J.tJ= SL是tcs，tJ=SL ist（ConsbJds）显然，对于任何cs和bJ以及某些ds，cs不等于Cons bJds。 在类型错误诊断方面，上述情况可能被报告为输出列表的类型过于多态。纠正这个错误的一种方法是将cs约束为非空。插入的签名变为：insert：： Int（a）->SList bs->SList（C c cs）程序的其余部分保持不变。但是，类型检查仍然失败。这里是更新后的隐含约束。 更改将突出显示。a，b，s，c，c，s. 不客气。b.s.J.⎛⎛ ⎞ ⎞⎜⎜t=Int(a)→Slist bs→SList(C c cs)∧ ⎟⎟⎜⎜ ⎟ ⎟插入- -insert：： Int（a）->SList bs->SList（C c cs）插入⎜ ⎟⎜⎜J J ⎟ ⎟⎜⎜bs= C b bs∧ Sorted bs-- insertx(Cons （y yy）⎜ ⎟a>=bJ-- Gt->⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟是的，是的。（t=Int（a）→SList ds→SList（C e es））⎝ ⎠e=bjSorted（C e es）--Cons y（insertx ys）问题是我们还需要声明cs的第一个元素是bJ。140M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129⎝⎜⎠⎟⊃⎜⎜⎜⎟⎟3.2第二次尝试在前面的例子中，排序列表类型定义无法捕获插入结果的第一个元素是插入元素a和数组bs的第一个元素之间的最小值。 我们在下面给出的SList--k-sortedlistsdataSList k其中无：：SList k缺点：：k =b =>Int（k）-> SList b-> SList kinsert：： Int（a）->SList b ->SList（min a b）insert的新签名声明它的参数是一个整数和一个第一个元素为b的有序列表，结果是一个非空的有序列表，其第一个元素是a和b的最小值。这个程序进行类型检查。为了理解这是如何发生的，让我们看看由最后一个再一次的条款和案例a，b，bs，cs. 不客气。⎛⎛ ⎞⎞⎜⎜t=Int(a)→Slist b→SList(min a b)∧ ⎟⎟⎜⎜ ⎟⎟--insert：： Int（a）->SList b->SList（min a b）⎜ ⎟a>=b-- Gt的case（testx y）->⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟（t=Int（a）→SList b→SListb⎝ ⎠--Cons y（插入xys）这个公式显然是正确的。然而，insert的签名并没有指定它的确切行为;它只声明输出是一个排序列表，其第一个元素具有特定属性。一个更强、更精确的签名还将指定一个集合保留属性：输入参数中存在的元素集合正好insert返回的结果中存在的元素集。此属性将在以下程序中捕获。data SList as whereNil：：SListN缺点：：Sorted（C bbs） =>Int（b）-> SList bs -> SList（Cbbs）--Permutation relationship，用于证明集合保持规则PermutationN N =>Truerule Permutation（C a as）bs =>（Delete a bs zs），（Permutationas zs）rule Delete a（C a as）as => TrueM. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129141规则Delete a（C b bs）（C bcs）<=>Delete a bs csinsert：： Permutation（C a as）bs=> a -> SList as -> SList bs--程序文本保持不变这个程序不会进行类型检查。仔细看看将类型检查算法应用于这个程序的过程，我们注意到这个过程在以下证明义务不能进一步履行时停止。a b，Permutation（C a（C b as））（C b bs）<$Permutation（C a（b as））（Ca bs）a≥b，Permutation（C a as）（C b bs）<$Permutationas bs虽然这些隐含约束显然是正确的，但它们并不直接遵循排列规则。上述未履行的证明义务建议以下替代规则的排列。规则排列（Ca（C b bs））cs<==>aa>= b |cs = C b ds，置换（C a bs）ds--（**）这里，守卫a b和a >= b选择了一个规则来进行约束简化。事实上，上面给出的规则定义了一个置换关系，只有当两个参数是彼此的置换但这里需要解决以下问题• 从类型检查的失败中推断出的替代规则（**）限制性太强;确定它们需要置换关系（正如通常的数学意义上所理解的那样）并不是微不足道的。• 规则（**）与insert的定义非常相似。可以说，我们正在重写类型级别的插入定义，这将使程序验证变得超级简单。这强调了通过表达类型进行程序验证所面临的挑战一般来说，很难提出有意义的程序属性，这些属性的表达方式使它们能够通过对手头程序的类型检查进行自动验证。这样的属性通常不是很有意义（例如在类型级别重写程序），或者太弱而无法建立。克服这些极端是进一步研究的主题。然而，另一个挑战是提出一组一致的类型检查规则，以确保类型检查对于特定应用程序域中的一组全面的良好类型程序是成功的。在排序程序的情况下，我们需要一个能够处理不等式约束和列表排列的完整理论。在我们的例子中，我们假设这样的规则在需要时随时可用。根据以前对排序算法的自动化证明的经验，候选规则的列表将是相当简单的142M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129编译。然而，证明这样一个规则系统是一致的（或者更好的是一致的）、完整的和终止的，是进一步研究的主题4资源使用验证程序的资源使用行为的静态验证是文献[36，34]中研究得很好的问题。任务是确保程序符合资源使用策略，例如文件关闭后不能访问，写入后不能读取我们的目标是实现这样的资源使用分析与EADT。4.1EADT实施在第一步中，我们需要预测程序的运行时资源使用行为标准的解决方案[18]是根据类型和输出系统[35]来抽象程序的资源使用行为。下面是一个简单while语言的可能EADT实现，其中对象由正则表达式表示。dataOR r1 r2--选择dataSTARr-- Kleenestar--singleton types/effectsdataO--open数据W--写数据R--读数据 C--关闭--EADT表示类型和效果规则数据Cmdr，其中Seq：： Cmdr1 -> Cmdr2 -> Cmd（r1，r2）当前值：：Bool ->Cmdr1->Cmd r2->Cmd（ORr1 r2）While：：Bool ->Cmdr1->Cmd（STARr1）打开：：Cmd O写入：： CmdW读取：：Cmd R关闭：：Cmd C构造函数对类型和输出系统的类型规则进行编码。例如，在if-then-else的情况下，我们使用“choice”来表示结果结果可以是两个分支的结果之一。在while的情况下，我们使用对于每个资源原语，我们引入一个原语资源对象。这里M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129143是用更熟悉的符号表示的类型和输出规则。（Ite）► exp：布尔函数Cmd（r1）Cmd（r2）► If exp then c1else c2：Cmd（r1|r2）（While）► exp：Bool函数c：Cmd（r）► While exp c：Cmd（r）（Open）Open：Cmd（O）因此，我们可以分析，someBoolean：： Boolprog = Seq Open（Seq（Ite someBoolean Write Read）Close）具有Cmd（O，（（OR W R），C））类型。为了检查资源使用的正确性，我们需要验证来自程序的结果是资源使用策略所允许的结果的子类型在我们的设置中，结果是轨迹的集合，其中轨迹是常规语言的单词。为了在对象之间实现子类型化，我们引入了一个二进制约束Sub和一些适当的CHR来编程Sub r1 r2保持iL（r1）L（r2）的属性。我们省去了读者的细节，并参考[15]，我们已经展示了如何使用类型类/CHR实现正则表达式语言包含。我们考虑一个特定的程序，我们对它施加这样的策略：在打开一个文件之后，我们可以写和读任意次数，然后关闭文件。check：：Subr（O，（STAR（OR WR），C）） => Cmdrprog = check（Seq Open（Seq（Ite someBoolean Write Read）Close））原语检查验证程序是否符合策略。这是另一个例子，我们强加的政策，写入文件后，我们不允许再次阅读。check1：： Subr（O，（STAR R，（STAR W，C）=>Cmdr1 = check1（序列打开（序列写入（序列读取关闭）上面的程序不进行类型检查，因为类型类约束Sub RW（由“目标”Sub（O，（W，（R，C）（O，（STAR R，（STAR W，C））产生）不能被验证。在Haskell中，Sub R W是一个未解决的实例/约束。这为我们提供了一些重要的线索，我们的程序可能会在哪里以及为什么资源使用政策。下一个例子显示了我们的静态验证方法的局限性。check2：：SubrW=> Cmdr验证码2：： check2（Ite True Write Read）该程序产生了未解决的类型类约束Sub W R。因此，类型检查失败。另一方面，程序不会违反资源使用策略，因为在运行时我们永远不会进入关键是我们基于静态类型检查的验证是不完整的，因为某些安全的程序会被拒绝。这并不奇怪，144M. 苏尔茨曼河Voicu/Electronic Notes in Theoretical Computer Science 174（2007）129静态分析以保持可判定性。另一种选择是切换到动态检查方法，如合同[17]或其他形式[23]监视程序的运行时行为在这两个极端中，我们寻求一个折衷方案，即尝试执行尽可能多的静态检查，并将任何未解决的证明义务转换为运行时检查。4.2混合静态和动态验证我们将静态验证与动态验证相结合。为此，我们使用类型类解析机制[11]来对程序进行运行时检查。这个想法是，每当我们遇到一个程序部分，它引起了一个未解决的约束，我们用一个错误语句替换这个程序部分（即我们提出一个异常）。首先，我们介绍目标语言。数据Cmd2r=对于所有的R1 R2。（Sub（r1，r2）r）=> Seq2（Cmd2r1）（Cmd2r2）| 对于所有的R1 R2。（Sub（ORr1 r2）r）=>Ite2Bool（Cmd2r1）（Cmd2r2）| 对于所有R1。（Sub（STARr1）r）=> While2 Bool（Cmd2r1）| （SubOr）=> Open2|（SubWr）=> Write2| （SubRr）=> Read2|（SubCr）=>关闭2从本质上讲，这是以前的while语言。唯一的区别是资源效果不准确。它们可以是实际效果的超集接下来，我们引入一组类型类实例，在满足Sub r1 r2的条件下，将Cmd r1类型的表达式转换为Cmd 2 r2类型的表达式。翻译由输入程序的资源类型Cmd r1驱动。回想一下，类型Cmd r1是精确的。每个r1唯一地确定实际命令。下面是类和实例声明。Co r1 r2类|r1-> r2其中强制：：Cmd r1 -> Cmd 2 r2实例（Cor1 r3，Co r2 r4，Sub（r3，r4）r5）--（Seq）=> Co（r1，r2） r5，其中coerce（Seq c1 c2）= Seq2（coerce c1）（coerce c2）instance（Co r1 r3，Cor2 r4，Sub（ORr3 r4）r5）--（Ite）=> Co（ORr1 r2）r5，其中coerce（Ite exp c1 c2）=Ite 2 exp（coerce c1）（coerce c2）instance（Co r1 r2，（Sub（STAR r2）r3））--（While）=>（Co（STARr1）r3）其中coerce（While exp c）= While 2 exp（coerce c）instance SubOr=> Co Orwhere coerceOpen = Open2--（Open）instance SubRr=> Co Rrwhere coerce Read=Read2--（Read）instance SubWr=> Co Wrwhere coerce Write=Write2 --（Write）instance SubCr=> Co Crwhere coerce Close=Close2--（Close）我们确信instance（Seq）是正确的。实例上下文提供了Cor1 r3、Cor2 r4和Sub（r3，r4）r5。Seq（c1）上的模式匹配M. 苏尔茨曼河Voicu/E