基于不变量的程序构造和机械验证

理论计算机科学电子笔记259（2009）143-163www.elsevier.com/locate/entcs基于不变量的程序Viorel Preoteasa1和Rend-Johan Back2博山学术大学信息技术系芬兰图尔库摘要基于不变量的编程是一种方法，我们首先通过识别在算法执行过程中可能出现的基本情况（前置条件和后置条件以及不变量）来开始构建程序。这些情况在编写任何代码之前就已经被识别出来了。在那之后，我们确定了情况之间的转换，这将给我们程序中的控制流程。 数据精化（Data Refinement）是一种构建正确的程序的技术，该程序在具体的数据结构上工作，作为对抽象数据类型的抽象程序的精化。 我们在本文中研究基于不变式程序的数据精化，并将其应用于经典的Deutsch-Schorr-Waite图标记算法的构造中。我们的结果是形式化和机械证明的Isabelle/HOL定理证明。关键词：基于不变式的编程，数据精化，机械验证1引言基于不变量的编程[3，4，5，8]是一种构造正确程序的方法，我们从识别所有基本情况（前置和后置条件，循环不变量等）开始。在算法执行过程中可能出现的问题。这些情况在编写任何代码之前就已经确定和描述了。在此之后，我们确定的情况下，这共同决定了程序中的控制流程之间的转换。 这些过渡在被验证的同时，是建造的。因此，程序的正确性是作为构建过程的一部分而建立的。我们使用一种图解方法来描述基于不变的程序，（嵌套）不变图，其中情况显示为（可能嵌套）框和transition是这些框之间的箭头我们将约束的集合与每个情况框相关联，并将简单语句的序列与每个转换箭头相关联。嵌套表示情况的信息内容：如果情况B是嵌套的，1电子邮件：viorel. abo.fi2 电子邮件地址：backrj@abo.fi1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.12.022144诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143≥−≤在情况A中，则B继承A的约束。控制结构是情境结构的第二位，通常不是经典意义上的良好结构，即，控制不一定可以用单入口单出口结构来表示。不变式图明确地显示了验证程序正确所需的所有信息：前置和后置条件、不变式、转换和终止函数。多年来，我们一直在尝试使用基于不变式的编程来教授形式化方法这些经验是很好的，学生们很容易学会如何用这种方法构造正确的程序，并欣赏这种方法带来的对程序如何工作的额外理解。遇到的问题与不变量第一方法的关系不大，而与如何形式化地描述（在谓词演算中）直观上很好理解的情况的一般问题有关[5]。下面显示了一个基于不变式的程序的简单示例，阶乘函数，表示为不变式图。这里有三种情况，初始，不变和最终。初始情况声明了程序变量n和x，并将它们限制在整数范围内此外，我们还要求n0。其他两种情况嵌套在In-variant中，这意味着它们从外部情况继承程序变量和约束。最后一种情况表明，在终止时，x=n！必须持有。中间情况Invariant声明了一个额外的程序变量i，并将其限制在1到n+ 1的整数范围内。此外，它还要求x=（i1）！在这种情况下保持。图中有三个转换，一个是从Initial到Invariant的转换，提供x和i的初始值，一个是从Invariant回到自身的转换，当i n成立时更新变量x和i，还有一个是从Invariant到Final的转换，当i > n成立时，但不改变任何程序变量。不变量情形也给出了终止函数，形式为终止函数∈W，其中W是某个良基集。在这种情况下，良基集是自然数nat的集合，终止函数是n+1−i。性质n+1−i∈nat必须能从在情境不变中成立的约束中证明（在这种情况下，这相当于证明0≤n+1−i成立）。诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143145基于不变式的程序的执行可以在任何情况下（不一定是初始情况），在满足情况约束的状态下开始。将选择在此情况下启用的转换之一。然后执行transition，导致（可能）另一种情况下的新状态。再次选择一个已启用的转换，并执行，以此类推。这样，执行从一种情况到另一种情况。 当在没有启用转换的状态下达到一种情况（不一定是最终情况）时，执行终止。因为执行可以在任何情况下开始和终止，基于不变式的程序可以被认为是多入口，多出口程序。我们可以选择将基于不变式的程序中的某些情况识别为初始情况，而将其他一些情况识别为最终情况，其想法是执行应该在某些初始情况下开始，并且应该在某些最终情况下结束。基于不变式的程序是一致的，如果每个转换都保持了位置约束。这意味着，如果我们在情况A和满足A的约束的状态下开始执行，并选择在A中启用的转换，那么执行转换将导致某种情况B（可能再次是A），从而产生的状态满足与B相关的约束。一个基于不变式的程序是终止的，如果程序的每次执行最终终止。对于一个给定的最终情况的集合，一个基于不变式的程序被称为活的，如果终止只发生在某些最终情况下。在[8]中详细研究了基于不变式的程序的语义和证明理论本文的目的是研究在构建基于不变式的程序时使用数据精化。数据精化[12，2，10，11]是一种构建正确的程序的技术，它在具体的数据结构上工作，作为对抽象数据结构上工作的更抽象程序的精化最终程序的正确性来自抽象程序的正确性和数据细化的正确性。正确性证明的总体复杂性通常在使用数据精化时比直接在具体数据结构上开发最终程序时要我们将展示如何将数据细化的基本思想同时，我们将以一种易于描述数据细化的方式扩展嵌套不变图的概念。在理论方面，本文通过包括进行数据修正的方法来扩展[8]中描述的工作。我们在这里提出的数据精化定理都在Isabelle/HOL [15]中得到了机械证明。我们将我们的技术应用于一个更大的案例研究，为任意图构建经典的Deutsch- Schorr-Waite（DSW）[16，13DSW算法标记图中从根节点可到达的所有节点。每个节点只使用一个额外的内存位来实现标记。图由两个指针函数给出，左和右，对于任何给定的节点，它们分别返回其左和右后继在标记时，左和右函数被改变以表示描述从图中的根到当前节点的路径的堆栈。完成后，恢复原始图形结构。我们通过三个连续的数据细化步骤的序列来构造DSW算法的146诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143∈±H→∈→∈ ∈∈→⊆ ∪∩± HH→ →→在我们的开发过程中产生的证明义务都在Isabelle/HOL中被形式化和机械地证明。我们案例研究的主要区别是，与以前的研究[14，1]不同的是，整个细化过程是使用不变图进行的。我们还相信，我们通过首先证明算法的泛化来开发算法的方式大大减少了整体证明的难度。本文的结构如下。第2节介绍了基于不变量的程序的证明理论第三节展示了如何对不变图进行数据精化。DSW算法在第4节中构造第5节提出了一些结论性意见。2不变图我们在这里更精确地描述如何证明不变图的正确性我们首先定义单调谓词变换器的概念，基于不变式的程序的语义是基于它的，然后继续定义不变图正确性的不同方面。2.1单调谓词变换我们假设一个给定的状态空间。 状态σ是一个元组，每个程序变量都有一个分量，它表示程序变量在计算的某个时刻的值。我们假设程序变量x的值由投影函数x：n→T给出，其中T是x的类型。谓词（或集合），表示为pred，是从bool→bool的函数。 我们表示为分别表示谓词的并集、交集和包含我们为所有单调谓词变换器的类型编写mtran，即，从pred pred的单音调功能。程序被建模为mtran的元素。如果Smtran和ppred，则S.p pred是S的执行在满足后置条件p的状态中终止的所有状态。程序的顺序组合，记作S;T，被定义为单调预测变换器的函数组合，即： （S; T）.p = S.（T.p）。我们分别用、和表示、和的逐点扩展类型mtran，连同谓词上的操作的逐点扩展，形成了一个完整的格。mtran上的偏序是精化关系[9，2]。谓词TransformerS T模拟了恶魔的选择--在执行S或T之间的选择是任意的，不能被从外面包围。某些类型T的程序表达式被看作是来自函数的函数。T. 如果e：T和σσ是表达式e在状态σ中的值，其中e中的自由变量的值由σ给出。 例如，表达式x+y在状态σ中的值为7，其中x.σ= 3，y.σ= 4。 在Isabelle/HOL，我们实施一个程序表达式（谓词）e，它包含自由变量xi：Ti作为函数e：T1...TnT. 那么E.A1.... an n是表达式e在状态σ中的值，其中x i.σ=ai。如果e，f是程序表达式，x是程序变量，那么我们用e[x：=f]表示e中f对x的替换。诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143147{|个 文件夹|.我们介绍了一些基本的单调谓词变换器，我们使用在构建不变的程序。这些是赋值语句x：= e，假设语句[p]，恶魔赋值语句[x：= xJb]，天使赋值语句x：=xJb和魔术语句magic。我们将其定义如下：赋值（x：=e）.q=q[x：=e]假设[p].q=<$p<$q恶魔分配nt[x：=xJ|b].q=（xJ·b<$q[x：=xJ]）天使指派nt{x：=xJ|b}.q=（<$xJ·b<$q[x：=xJ]）魔术魔 术 .q=true变量xJ在恶魔和天使赋值语句中是绑定的，我们假设q不包含变量xJfree。除了天使赋值之外，上述所有程序结构都可以简化为恶魔赋值。此外，恶魔分配的顺序组合和恶魔选择由于这些性质，我们将始终在定义中使用恶魔赋值，但我们将在示例中使用所有我们也可以允许断言语句，但是当我们省略它时，处理会变得简单一些（断言语句可以毫无问题地处理，如[8]所示）。对于单调谓词TransformerS∈mtran，我们引入了S的保护通过grd.S=<$（S. false）。定理2.1下列性质成立。grd. （x：=e）=true grd. [p]=pgrd. [x：= xJ|b]=（xJ·b）grd. （S1HS2）=grd.S1 grd.S2如果p和q是谓词，S是一个程序，那么一个全正确性三元组，记为p{|S|}q，为真当且仅当p≠ S.q。对于函数f：X→Y，我们用f[x：=y]：X→Y表示给定的函数，通过f[x：=y].z=yifx=zf.z否则2.2不变图不变图是一个有向图，其中节点用不变式（谓词）标记，边用程序语句（单调谓词变换器）标记。不变图的节点称为情境，边称为变迁。148诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143∈∈→ ×→·--∈∈→∈►{||}→→×→设I是一个非空集，如果索引。形式上，不变图是元组（P，T），其中P：Ipred是不变量，T：IImtran是转换。 我们也称T为转移矩阵。在情形i I，grd.T.ipred中的转移矩阵的保护是来自i的所有转移的保护的析取：grd.T.i=grd.T.i.jj∈I我们假设在本文中，边缘标记只有恶魔的赋值语句[x：=xJR.x.xJ]。一般来说，我们可以使用假设、赋值和恶魔赋值状态的顺序组合来在边缘上。然而，这些语句都可以机械地简化为一个等价的恶魔赋值语句。例如，计算一个数n的阶乘的程序被表示为一个不变图，通过选择I=Initial，Invariant，Final，并根据图给T赋值。如果没有在图中明确地画出，则假设从情况i到情况j的转换是魔术的（从未启用的转换）。例如，T（Invariant，Invariant）= [x≤i] ;x，i：=x·i，i+1和T（Invariant，Initial）=魔法。不变图的执行可以在任何情况i I中开始，并且然后非确定性地从i选择导致某个新情况jI的某个启用的转变。只要启用了转换，执行就会以这种方式继续。执行终止时，达到的情况是没有transi- tions启用。在文献[8]中，我们介绍了基于不变式程序的操作语义和谓词Transformer语义，并证明了它们的等价性。我们还介绍了正确和完整的证明规则不变图。我们在下面回顾这些证明规则。非正式地，转移矩阵T：I Imtran关于初始谓词P：Ipred和最终谓词Q：Ipred是完全正确的，表示为P T Q，如果对于所有初始状态s和P.i.s为真的情况i，执行总是终止，并且Q.j.sJ对于终止状态sJ为真，并且终止情况j.我们有下面的一般规则来证明不变图的完全正确性。 如果（W，<）是一个良基集，X w：I pred，w W，是一个谓词族，则下面的推理规则为真：哪里（（X）P）（（X）grd. TQ）（i，j，w·Xw. i{|Ti，j|}X n]|} n ≥ 0 <$x = n！图的执行可以从任何情况开始，也可以在任何情况下结束。在实践中，我们主要感兴趣的是执行150诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143⊆J在某些预定的最终情况下，它会被终止。 例如，我们希望前面给出的阶乘图总是在情况Final中终止。一个具有最终情况的不变图是一个元组（P，T，J），其中（P，T）是一个不变图，J I是最终情况的非空集合。图（P，T，J）是正确的，如果（P，T）总是终止于J中的一个情形（我们于是说图对于最终情形J是活的）。形式上，我们用三元组定义了具有最终情况的不变图► P{|不|} P（3）其中对于所有i∈IPJ.i=P.i如果i∈J否则为false如果我们只要求在阶乘例子的最终情况下终止，那么我们有两个额外的证明义务（这两个都是微不足道的）：n≥0 ≤真n≥ 0 <$x =（i − 1）！ i ≤ n +1 <$（i ≤ n <$i> n）我们在图中强调最后的情况，如阶乘示例中所示，用一条股票代码边框线来绘制它们。一个可执行不变图是一个图中的所有语句都等价于形式[p];x：=e，其中e和p是普通的程序表达式。因此，它们不应包含不符合以下条件的量化器或指定函数： 目标编程语言的一部分。在例子中，经常可以方便地在两种情况i和j之间画出一个以上的过渡。我们将这些解释为代表一个单一的转换，即i和j之间所有转换的恶魔选择。3不变图的数据精化数据精化已被证明是开发软件系统的强大工具。当编写一个复杂的程序时，从一个抽象数据结构上的抽象程序开始，并逐渐将其细化为一个在具体数据结构上工作的更具体的程序通常是有用的使用这种方法，整个证明工作被分成更小的任务[2，10，11]。3.1报表的数据细化下图描述了数据细化：.诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143151联系我们抽象语句S修改了全局变量z和抽象变量x，并从初始抽象情形.x. z引导到最终抽象情形.x. z。具体陈述SJ修改了整体变量z和具体变量y，并从初始具体情况αJ.y.z引导到最终具体情况βJ.y.z。数据抽象关系R1.x.y.z描述了在初始情况下抽象变量x与具体变量y和z之间的同样，对于最终情况下的R2.x.y.z我们可以用一个天使般的陈述D来定义数据抽象，这个陈述D为每个具体的状态计算出某种抽象的状态。让我们定义D1={x：= xJ|R1.xJ.y.z<$αJ.y.z}D2={x：= xJ|R2.xJ.y.z<$βJ.y.z}这里的抽象（解码）语句Di既包括抽象关系又包括具体不变量。我们说程序S是由SJ通过D1和D2所定义的数据，记为S±D1，D2SJ，如果D1;S±SJ;D2成立。现在让我们进一步假设抽象陈述S只是一个恶魔赋值，S = [x，z：= xJ，zJ]|[Q.x.z.xJ.zJ]我们想在初始情况.x. z成立的上下文中对抽象陈述进行细化这通过数据细化表示为：SD1，D2SJ。当且仅当αJ.y.z <$R1.x0.y.z <$α.x0.z <$z = z0{|SJ|}（<$x·R2.x.y.z <$βJ.y.z<$Q.x0.z0.x.z）3.2基于不变式程序的数据精化数据精化通常用于实现具有信息隐藏的数据模块。模块的规范定义了访问过程在抽象变量方面的效果。该模块的实现实际上是根据具体变量完成的，以实现效率。如果我们可以证明所有访问方法的数据细化，那么模块的任何用户都不会看到差异，并且可以使用模块并推理其行为，就好像它真的是根据抽象变量实现的一样。基于不变量的程序的情况是不同的。在这里，我们感兴趣的是推导出一个具体的算法，对具体的变量。抽象只有在它为我们节省了一些验证工作，或者可以简化算法的理解和/或构造时才有用。 然而，事实证明，数据精炼对于此目的也非常有用。在许多情况下，首先设计一个抽象程序，对预期状态进行某种抽象，并证明它满足我们的要求，然后将其细化为一个更具体的程序，在我们真正想要（或必须）使用的状态空间152诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143∧考虑一下上图中的情况。初始情况具有约束条件αJ.y.z，最终情况具有约束条件βJ.y.z。 现在假设我们希望具体变量y和z也满足约束D1。（.x. z），它说存在某个值x使得R1.x.y.z.x. z成立。换句话说，变量y和z也应该表示一些满足抽象情境约束的抽象变量x。这意味着初始情况具有全局约束（x·R1.x.y. z.x.z）同样，我们可以认为，最终的情况有总体约束，（x·R2.x.y. z.x.z）这就把情境的约束分为两个部分，具体的和抽象的。我们现在寻找的是一个具体的过渡SJ，当这样解释时，它从初始情况通向最终情况。我们在一个不变图中描述这一点，如下图所示左边的符号表示嵌套情况的不变量是外部情况和内部情况中的约束的结合，但是变量x通过存在性量化而被移除。右边的图等价于左边的图，但是没有数据抽象符号。左手边符号的优点是它显示了情境的结构，以及它是如何从具体和抽象的需求中建立起来的。如果满足以下条件，则过渡SJ现在是正确的D1. （.x. z）{|SJ|} D2. （x.x. y）（4）或者，明确地写出，如果（x·R1.x.y. z.x. z）{|SJ|}（. x. z）保持。我们通过证明两个较小的步骤来证明（4）(i) 抽象转换S是正确的，且(ii) 具体变迁SJ是抽象变迁S的数据细化。诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143153这在下一个定理中说明。定理3.1.x. z{|S |{\displaystyle {\frac{i}∧αJ.y.z <$R1.x0.y.z <$α.x0.z <$z = z0{|SJ|} βJ.y.z <$（<$x·R2.x.y.z<$Q.x0.z0.x.z）（ii）⇒D1. （.x. z）{|SJ|} D2. （.x. z）证明定理中的假设（i）和（ii）实际上将建立下图的正确性。这既表明了抽象的过渡，也表明了具体的过渡，并解释了具体的过渡是如何从抽象的过渡中派生出来的。抽象和具体转换的验证可以仅使用图中明确给出的3.3终止接下来我们证明抽象程序的终止性是由具体程序继承的。考虑下面的简单图表，它的控制结构类似于阶乘函数。（五）如果Si=[x，z：=xJ，zJ·Qi.x.z.xJ.zJ]，则对全部正确的证明义务154诉Preoteasa，R.J. 理论计算机科学电子笔记259（2009）143{·}抽象程序的性质是α{|S1|} pw{|S2|} p

下载后可阅读完整内容，剩余1页未读，立即下载