形式验证方法在计算机科学中的应用-Isabelle/HOL共归纳证明的形式化和比较

理论计算机科学电子笔记176（2007）61-77www.elsevier.com/locate/entcs基于相似关系Sabine Glesner Johannes Leitner Jan Olaf Blech软件工程和理论计算机科学研究所，FR 5-6，柏林工业大学，10587Berlin，Germany电子邮件：{glesner|Leitner|blech}@ cs.tu-berlin.de网址：http：//pes.cs。 tu-berlin.de/摘要形式验证方法由于其能够保证系统正确性和提高可靠性而变得越来越重要。然而，如何在定理证明器中形式化证明的问题远非微不足道，但非常重要，因为如果形式化没有巧妙地选择，则需要花费更多的时间进行验证。在本文中，我们开发和比较两种不同的可能性，以表达共归纳证明的定理证明器Isabelle/HOL。共归纳是一种证明方法，允许验证非终止状态转移系统的属性。 由于共归纳不像其他证明技术那样广泛使用，例如归纳，因此如何形式化相应的证明的“配方”要少得多，并且在定理证明器中实现的共归纳证明策略也更少。 本文研究状态转移序列性质的共归纳证明的形式化。特别是，我们比较了两种不同的可能性，他们的形式化，并显示其等价性。这两种形式化中的第一种抓住了数学直觉，而第二种可以更容易地在定理证明器中使用。 我们已经在Isabelle/HOL中正式验证了这些准则的等价性，从而建立了一个共代数验证框架。 为了证明我们的验证框架适用于编译器优化的验证，我们引入了三种不同的、相当简单的转换，这些转换捕捉了优化编译器验证中的典型问题，即使是对于非终止源程序。保留字：共归纳，操作语义，编译器验证，定理证明器，Isabelle/HOL1介绍在过去的十年中，交互式或自动定理证明器中的形式验证变得越来越重要，原因有几个：首先，机器证明保证没有特殊情况被忽略，因此，被验证的属性在所有特定情况下都确实成立其次，机械化定理证明器允许管理大型系统的大型正确性证明，这些大型系统由于复杂性而无法在没有机器帮助的情况下由人类管理。最后但并非最不重要的是，在过去的几年里，定理证明器的效率和用户友好性已经有了很大的提高，它们可以用于现实生活中的验证问题。尽管如此，仍然有许多问题没有解决。尤其是如何将证明形式化为定理的问题1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.02.03762S. Glesner等人理论计算机科学电子笔记176（2007）61prover一点也不简单。一个不聪明的形式化可能会导致笨拙的证明，从而使证明不必要地复杂化。在本文中，我们研究了变换的正确性证明，即证明变换保持了被它们修改的系统的语义。特别是，我们解决了不保留程序语法结构的非细化转换。如果一个变换不改变程序的结构，而只是更详细地说明如何执行各个计算，那么它就被称为精化非精化转换在优化编译器中很重要，因为它们允许不遵循原始程序结构的代码转换整个程序的非精化变换的正确性证明提出了一个问题，即它们不能直接由其部分的正确性证明此外，我们解决的问题，验证变换的非终止程序。出于这些目的，我们需要一个正确性的概念，它捕获程序的状态转换行为作为我们方法的应用示例，我们考虑优化编译器，这些编译器通常需要通过非细化优化来转换程序，以实现最佳的加速。在过去的十年中，编译器验证一直是一个重要的研究领域。尽管如此，大多数研究都集中在相当简单的细化变换上，这些变换既保留了程序的结构，又终止了程序。特别是对于编译器，限制终止程序是不够的，因为存在许多非终止程序（例如操作系统，数据库，反应式系统中的软件），这些程序需要正确编译，以保持其状态转换行为。我们的方法是基于这样的观察，即每个程序定义了一个状态转移系统，并且可以被认为是一个合适的final余代数的元素。我们提出了一个定义编程语言语义的框架，通过为每个程序分配一个这样的余代数元素，即一个将输入状态转换为后继状态的函数。对于每个初始状态和程序，这种语义指定了这样一个最终余代数的一个元素，即一个可能无限数量的程序执行状态的共归纳定义（懒惰）列表。我们还提出了我们的形式化的共代数语义在Isabelle/HOL。此外，我们表明，这种概念的编程语言语义是succiently强大的验证也非细化程序transformation。一般来说，我们认为两个程序在语义上是等价的，只要它们的语义相同，即它们对应的一个合适的余代数的元素是相同的。然而，在许多情况下，人们希望将两个程序视为语义等价的，即使它们的状态转换序列（对于任意但固定的初始状态）不完全相同，而只是相似。为了能够捕捉到这些情况，我们定义了两个关于状态转换序列的相似关系：抽象和抽象。对于后者，我们陈述了两个不同的定义，并在定理证明器Isabelle/HOL中证明了它们的等价性第一个定义很好地捕捉了数学直觉，而第二个定义更适合在Isabelle/HOL中使用这是一个典型的例子S. Glesner等人理论计算机科学电子笔记176（2007）6163i：= 1;whiletruedoi：=i+1odi：= 1;whiletruedoi：=i+ 1od;i：= 5Fig. 1. 消除无法访问的代码经验表明，在定理证明器中形式化的选择是极其重要的。与我们的等价证明，我们弥合了一个直观的概念和一个有效的使用定理证明之间的差距，从而大大简化了机械化证明的建设。我们已经形式化了我们的框架，用于程序语言语义的共归纳定义，以及定理证明器Isabelle/HOL [15]中两个定义的等价性证明。此外，也在伊莎贝尔/HOL，我们已经实例化我们的框架与一个简单的命令式编程语言一起的例子证明程序等价的典型情况下。通过这些示例证明，我们证明了我们的框架对于在没有细化的编译器中验证各种优化程序转换是足够灵活的。本文的结构如下：在第2节中，作为动机，我们讨论了编译器转换的典型例子及其验证中出现的问题我们还指出，本文中引入的程序语义的共代数定义在第3节中，我们给出了一个简短的介绍，理论（共）代数和（共）归纳适合我们的需要。在第4节中，我们通过为每个程序和每个初始状态分配一个合适的最终余代数的元素，来定义命令式编程语言的余代数语义。相似关系的概念在第5节中给出。我们将在第6节中演示它们在程序转换验证中的应用。最后，我们在第7节讨论了相关工作，并在第8节总结。我们的Isabelle形式化在本文中一直在进行。2动机：更快的转型作为编译器转换验证中出现的简单但典型的例子，让我们考虑三个程序及其优化。第一个例子，cf。图1处理一个包含不可访问代码的非终止程序（在while循环之后）。由于while循环不会终止，最后一个赋值i：= 5将永远不会到达，并且可以被消除。为了证明以这种方式修剪的程序表现为原始程序，我们需要共归纳地表明它们两者的语义处于互模拟关系中，这意味着它们是相等的（参见。第6节）。归纳法作为证明原则是不成立的，因为它只允许我们证明有限状态转移序列上的陈述，参见。我们在第7节中也详细讨论了归纳法的不充分性。第二个例子涉及将循环不变代码移出循环体，参见。图2.由于赋值l：= 0不依赖于在循环体中计算或修改的任何值，因此该赋值已经可以执行64S. Glesner等人理论计算机科学电子笔记176（2007）61i：= 0;s：= 0;当i<=N时s：=s+i;i：=i+1od;总和：=s总和：=N<$（N+ 1）/2inti = 0;虽然我1000做return 0;int[i]：i;i：=i+1odinti = 0;return 0;虽然我1000做int[i]：i;i：=i+1od图二. 循环不变码图三. 两个计算高斯和的在进入循环之前，因此只计算一次，而不是在循环的每次迭代这种变换的验证不像第一个例子那样直接，因为状态转换序列不完全相等，而是可能在相同状态的重复次数上有所不同。我们显然不想区分这两个序列，而是希望能够坍缩任何有限数量的相同状态。这一想法是捕捉在概念的基础上，比照。第5款.最后，考虑图3中的两个程序（N是非负整数），它们都计算高斯和。它们的语义，即它们的状态转移序列，是不同的，因为第一个程序包含涉及变量i和s的计算，而第二个程序不需要任何辅助变量。因此，从严格的语义角度来看，这两个程序在语义上不可能相同。然而，如果我们忘记了变量i和s，即，如果将每个状态仅投射到感兴趣的部分上，则所得到的状态转换序列是相似的，并且可以被折叠成相同的在第5节中，特别是在5.2小节中，我们通过引入模抽象函数相似的概念来3（Co）代数与（Co）归纳近年来，共代数方法，特别是共归纳法，在基于状态的系统的规范和推理中获得了越来越多的兴趣和重要性[10]。在第3.1小节中，我们总结了这个领域中最重要的概念。在3.2小节中，我们展示了如何在定理证明器Isabelle/HOL [15]中使用共归纳定义和证明原理。3.1余代数与余归纳证明原理代数和余代数是关于函子定义的。给定函子T对于集合X，T-代数是具有T-结构的集合，即. 被定义为S. Glesner等人理论计算机科学电子笔记176（2007）6165函数a：T（X）→X。例如，自然数的结构被定义为T-代数[0，S]：1 + IN→ IN，其中函子T（X）= 1 +X。 初始T-代数的特征是存在唯一的从初始T-代数到任何其他T-代数的同态f初始T-代数是函子T的不动点对偶地，T-余代数被定义为函数c：X→T（X）。如果我们认为X中的元素是状态，那么余代数将给定的状态x∈X映射成一个或多个后继状态，以及可以在该状态X.在这种情况下，基于状态的系统的特征在于在其运行期间可以进行的观察。例如，一个确定性的、不一定终止的变迁系统可以用T-余代数[stop，value，next，value]来描述：X→T（X），函子T（X）= 1+A×X，其中A是任意非空观测集给定一个状态x∈X，[stop，nvalue，nextn]（x）要么是终止状态stop，其中不可能有观测，要么存在后继状态next（x）和观测值（x）∈A。最终T-余代数作为初始代数的对偶概念，其特征在于存在从任何其他T-余代数到最终T-余代数的唯一同态。对于函子T（X）= 1 + A×X，最终余代数是[empty，historical，tail]：A∞→ A × A∞。 A∞是包含所有元素来自A的有限和无限序列的集合。最终T-余代数，如果它们存在，是最大函子T的不动点对于多项式函子，甚至对于有限幂集函子，存在最终余代数。多项式函子对于我们的目的是完全足够的。同归纳一样，共归纳也是定义原理利用了从任意T-余代数到最终T-余代数的同态存在这一事实互模拟是一个重要的共归纳证明规则。它说，最终余代数上的每个二元关系，在余代数的运算下是封闭的，都包含在等式关系中。3.2Isabelle/HOL中的余代数与余诱导在[17]中描述的扩展中，Isabelle/HOL中的余代数类型是可用的。这个扩展使用了共归纳定义的集合，这是Isabelle/HOL中可用的定义原则，并使用它来定义懒惰列表。 作为一个例子，考虑可能无限列表的共归纳定义，如[17]所述。下面的定义指定了给定集合A上的懒惰列表集合llist（A）。共诱导列表（A）引导页NIL I：NIL∈llist（A）CONS I：[a∈A;M∈llist（A）]=<$CONSa M∈llist（A）基于这个定义，导出了共归纳数据类型llist。有关此规范的详细信息，请参阅[17]。66S. Glesner等人理论计算机科学电子笔记176（2007）61对于关于余代数类型上的等式的推理，我们使用双模拟的概念。互模拟是在余代数类型上的二元关系，它在余代数的运算下是封闭的。对于懒惰列表，这意味着从CONSa l<$CONSaJlJ，我们可以推导出a=aJ和l<$lJ。 在Isabelle/HOL中，我们已经说明了这个定义，其中我们使用符号来表示空列表，x~L作为CONSx L的缩写（在一种状态转换为另一种状态的意义上，将“~“读互模拟：：“（'a llist × 'a llist）set bool”互模拟R == x∈ R。（x=（，）（ x1 x2 L1 L2. x =（x1~L1，x2~L2）<$x1 =x2 <$（L1，L2）∈ R））Isabelle [17]的lazy list包提供了一种稍微不同的bisimulation形式：llist_equalityI：[[（l1，l2）∈r; r∈D_Fun（r）∈ range（λx.（x，x）]]=0.01= 1.02因为我们的定义更接近于[10]中介绍的定义，所以我们在证明中更喜欢它我们已经很容易地证明了它意味着应用llist等式I所需的等式（关于详细的Isabelle证明，我们参考[12]）：pauls_equiv：互模拟r = λr互模拟D_Fun（r）（x，x）为了使用余代数定义的类型，我们需要能够定义不一定终止的递归函数。对于懒惰列表，llist corec允许我们定义函数Ja−→Jb llist如下，其中f是部分定义的函数f：Ja~Jb×Ja和1和2通常的投影函数：⎧如果fx=0，llist corec xf=0（f x）2felse这些定义是我们的强制性编程语言的语义和编译器transformations的正确性证明4作为余代数命令式编程语言的形式语义的操作方法通常将给定程序的语义定义为程序运行期间达到的状态序列，或者更一般地，在不确定性的情况因此，将程序视为合适的余代数的元素是一个自然的结果，即作为函数，将状态作为输入并输出新的状态以及可能的观察结果。这种观点与操作语义的两种经典方法的意图是一致的，这两种方法是抽象状态机（ASMs）[6]和结构操作语义（SOS）[18]。我们在这里集中讨论SOS，但我们所有的发展也可以应用于ASMs。这是因为每个SOS语义都可以转换为等效的ASM语义，反之亦然[4]。S. Glesner等人理论计算机科学电子笔记176（2007）6167114.1结构操作语义学结构操作语义（SOS），也称为小步骤语义，关注程序执行的各个步骤以及这些单个步骤如何集成到整个执行中。推理规则的假设形式化了较小的步骤，而它们嵌入到较大的程序上下文中则在结论中定义。各个步骤由公理描述。这样一个单独的步骤是执行p的终止，在最终状态σJ中<σ >→σJ，或者它是一个状态transi，步骤→表示在状态σ中执行p产生要在后续状态σJ中执行的新程序pJ。pJ通常被称为连续。推理规则的结论定义了将这些程序部分嵌入到其更大的上下文中。作为小步长定义的典型例子，考虑这些推理规则：→S′，σ′>→S′;S2，σ′>Eval（cond）=true<如果cond则S1elseS2，σ>→S1，σ>→σ′→S2，σ′>→S2，σ><跳跃，σ >→σ→ifcondthen（S;whileconddoS）else skip，σ><左栏中的前两个推理规则描述了如何将语句序列S1的执行集成到更大的上下文中，即语句序列S1;S2。右边的前两个规则指定了if语句的执行。第一个公理定义了skip语句的效果。最后一条公理通过将while循环的语义简化为if语句的语义来描述while循环。这种语义是确定性的，作为一个简单的情况下可能的状态和延续程序的区别显示。在小步语义中，要执行的程序是状态的显式部分。 每个状态包含一个连续程序p。 在初始状态，p是原始程序，而在最终状态，p只是空程序。小步语义的公理和推理规则定义了如何在每个状态转换期间重写4.2SOS的余代数语义我们通过一个函数来定义编程语言的操作语义，该函数将每个程序连同初始状态一起映射到函子T（X）= 1 +A×X的最终组合的元素，其中A是计算期间达到的状态集。这个余代数的载体集是A∞。这意味着，如果程序执行，则程序的语义由有限状态转换列表描述。68S. Glesner等人理论计算机科学电子笔记176（2007）61终止，并在非终止的情况下通过无限状态转换列表。SOS将编程语言的语义定义为映射元组的函数到元组的映射，从而表示在状态a中执行p产生要在后续状态aJ中执行的新程序pJ，或者在程序执行终止的情况下，作为到作为最终状态的aJ因此，每个SOS语义可以被认为是一个函数，它以程序p和初始状态a作为输入，并迭代地定义一个元素为A的有限或无限列表。因此，每个SOS语义都对应于一个具有余代数运算[stop，values，next values]的余代数。停止表示程序终止。否则，当前状态是可观察的，并由函数值表示。其余的可观察的状态转换序列是通过应用下一个当前状态的功能。给定SOS语义，我们定义一个函数[SOS]]：A×P→A∞余归纳为下图中唯一的余代数同态：A× P_[[SOS]]- -- -_A∞[停止，值，下一个值]J[空，头，尾]J1+A×（A×P）________ 1+ A × A ∞id+（id×[[SOS]]）[SOS]的定义方程为：⎧constructions（value（a，p），next（a，p））if[stop，constructions，next]（a）⎪停止jJ⎪⎨[[SOS]]（a，p）=⎪⎪即如果 →或者如果→aJif[stop，value，next]（a）=stop⎪⎪⎩如果没有继承国，这个定义赋予每个程序和每个初始状态一个最终余代数A∞的元素，A ∞是函子T（X）= 1+A×X的最终余代数。5相似关系正如第2节中的例子所证明的，我们可以认为两个不同程序的行为是等价的，即使它们的状态转换序列不相同。在本节中，我们定义了列表上的两种相似关系。第一种，我们称之为折叠，允许我们将任何有限数量的连续相同状态折叠成给定状态转换序列中的一个状态。折叠对于验证更改某个程序部分中执行步骤数量的编译器优化至关重要 一个非常简单的例子是消除no-ops或skip语句。在机器代码级别上，一个稍微复杂一点的例子是用一个简单的操作替换另一个简单的操作。⎪S. Glesner等人理论计算机科学电子笔记176（2007）6169更复杂的等效操作或简单操作的捆绑，使得它们可以在一个步骤中执行。这在验证现代VLIW（超长指令字）处理器（如Intel Itanium架构）的优化时尤为重要。这些优化可以很容易地证明是正确的概念的干扰。在5.1小节中，我们介绍了两个不同的定义，并总结了Isabelle/HOL中它们等价性的证明第二种相似关系，抽象，允许我们简化状态转换序列，通过应用抽象函数元素的方式包含的状态。抽象的定义见5.2小节。5.1崩溃的关系坍缩是序列上的二元关系，它捕捉了这样一种思想，即我们希望通过将这个有限序列坍缩为一个单一状态，将连续相等状态的任何有限子序列视为等价于该状态的仅一次出现。原则上，有两种方法来定义坍缩关系。在本小节的其余部分，我们给出了Isabelle/HOL中的两个替代的定义及其等价性证明。5.1.1使用合并函数的相似性我们的第一种方法是基于序列的唯一最小形式，称为序列的合并。这是一个序列，其中一个元素的所有有限次如果两个列表的合并包含在互模拟中，则它们被认为是相似的。合并函数的定义需要形式化有限前缀和潜在无限序列的连续性。特别地，我们需要最大有限前缀的概念，它是序列中相等元素的（长度最大）前缀。在Isabelle/HOL中，这可以通过以下谓词表示：is_max_prefix pLp前缀L你好 设p = {x}另一个（其他前缀L x。set other ={x}）−→其他尺寸≤尺寸p由于我们的序列是潜在无限的，这样的前缀不一定需要存在。例如如果我们的列表是单个状态1的无限重复，则不存在最大有限前缀在我们的形式化中，我们还定义了函数split_finite_prefix，它分割序列的最大前缀（如果它存在），返回前缀元素和列表的其余部分，或者如果列表为空则返回None分裂有限前缀case Lof无| x ~ L2 ⇒如果前缀是_max_prefix p L，则Some（x，cut_maxn（size（max_prefix L））L）else Some（x，L2）1 对于缩写，这样的列表被称为无聊。70S. Glesner等人理论计算机科学电子笔记176（2007）61如果列表中没有这样的前缀，那么只有第一个元素被拆分为前缀。将此函数以共递归方式应用于惰性列表，将产生所需的合并函数：合并L≡ llist_corec L split_finite_prefix以这种方式定义的合并函数正是我们想要的：它将相等元素的序列折叠成该元素的一个单独出现。如果列表是某个x的无限重复，那么合并函数就像一个简单的复制函数，因为最大前缀永远不存在。请注意，合并函数不可计算，因为split_finite_prefix不可计算。这也是为什么两个列表相似的证明不能自动化的原因对于这样的证明，需要找到一个包含它们的合并对的互模拟在具体情况下，这可能是一项乏味的任务。对于有限列表，我们可以显式地命名所有最大的简单前缀，以便将它们折叠成单个（相等）元素。 对于无限列表，我们必须在我们的列表中展示某种结构，使得每当我们从两个列表中删除一个最大简单前缀时，我们可以再次这样做，等等。 当使用直接定义的关系时，关于无限列表的相似性的推理变得更容易，如下所述。5.1.2直接定义相似关系或者，我们使用以下引入规则共归纳地定义一个关系，其中r=pdenteste a tet e.finite元素x的重复次数：2共归纳“absRel”引导页nil：“无意义的“步骤：“[[ p=q ; LM]]=p@Lq@M”这个定义表达了空列表与空列表相似，如果两个列表相似，那么我们可以在两个简单的x前缀前面加上两个不同长度但元素x相同的前缀。 虽然这个定义简短、简洁，而且--正如我们稍后将看到的--易于在证明中使用，但人们不能立即看出它等价于我们基于合并函数的第一个对双列数的定义。最突出的问题是我们不能“走回头路这意味着当对于某些P和Q成立，我们只知道存在P的某些分裂，Q使得P和Q的各自前缀对于某个x是有限x-前缀，并且后缀也是相似的，但是没有办法构造性地确定这个前缀-后缀-对。对于共归纳集和归纳集的这些性质的证明经常使用事例规则，逻辑上等价于回”的介绍步骤。 将这一规则应用于格式为A-B的陈述只产生这样的分裂存在的弱声明，这对于大多数用途是不足够的。为了使这个定义仍然有用，我们证明了一个加强的案例规则：我们表明，每当我们在第一个变化的位置分裂序列时也就是说，在最后一节定义的最大前缀之后，我们保持相似性：lemmacase_strong：“[[p@L q@M; is_max_prefix p p@L; is_max_prefix q q@M]]=LM“2 符号@表示列表上的追加操作。S. Glesner等人理论计算机科学电子笔记176（2007）6171利用这个引理，我们证明了我们的关系的抽象性质（如传递性），参见。[12]详情此外，这条规则是我们两个相似性定义之间的重要桥梁，我们需要证明它们的等价性。5.1.3证明等价性这两个定义是等价的：merging（L1）=merging（L2）合并L1合并L2证明的一个方向是简单的。我们证明了每个懒惰列表都类似于它自己的合并。这个证明方向的简化版本在这里以ISAR [20]符号给出：引理abs_sim：显示“A合并A”证明-S让？X =“L.{（L，合并L）}”有“X”。x∈？X−→（x =（，）（2000年） x=（p@L，q@M）<$p<$= q<$（L，M）∈？XabsRel））”证明-{fix xassume“x∈？X”然后通过auto获得L，其中x_form：“x =（L，合并L）”因此，“x =（，）（2000年） x=（p@L，q@M）<$p<$= q<$（L，M）∈？XabsRel）”证明案例假设“L=0“显示？作者：lnil_abs_invariant下假设L_not_empty：“L空“然后通过简单相加得到l和M，其中L_form：“L=l~M”：因此？论文证明案例假设“boring L”，因此“x =（[l]@M，[l]@M）”通过自动因此？thesis by（unfold sameRel_def，auto intro：sim_refl）下假设“<$boring L”然后获得pmax，其中is_mp：“is_max_prefixpmaxL”. 此外，然后获得后缀，其中lsplit：“L=（pmax@suffix）”. 此外，从is_mp和L_form具有pml：“setpmax={l}”. 最终具有“合并L =1~合并后缀”...因此“x =（pmax@suffix，[l]@（merging suffix））”. 通过简单地添加：sameRel_def最终显示，您是否会看到“pmax_def=[l]”？汽车（Auto）qedqed}因此？blast文章QED而且有“（A，merging A）∈？X自动最终显示？thesis by（rule_tac X="？X”in absRel.coinduct，simp）QED这样证明了L等于merging（L），我们就可以完成一个方向的证明，即merging（L1）=merging（L2）=<$L1<$L 2，因为merging是一个等价关系。另一个方向带来更多的困难。幸运的是，我们有我们的“强化案件规则”。使用它，我们表明，X={（merging（x），merging（y））|x y}72S. Glesner等人理论计算机科学电子笔记176（2007）61⎪是一种互模拟，它要求⎧⎪⎪⎪⎨（，）或（merging（x），merging（y））=（a~merging（xJ），a~merging（yJ））⎪其中xJ<$yJ由于我们现在知道我们可以移除最大有限个α-前缀，并且列表保持相似，我们分别选择相应的子集为xJ和yJ（α为a）。由于合并函数的定义是只删除这个最大前缀，第二个要求也是正确的。这两个定义之间的等价性证明是非常有用的。在我们的实验中，我们发现，虽然使用相似关系的共归纳规则（第二种定义变体）相对简单，但要证明两个不同的惰性列表在核心递归定义的函数（第一种定义变体中的合并函数）下的图像是相等的，则要困难得多5.2从无关细节中抽象重新考虑图3中计算高斯和的两个程序，它们在语义上并不相同，但如果忽略变量i和s并将每个状态仅投影到感兴趣的部分上，则它们是相似的。在本小节中，我们正式介绍了通过抽象函数简化状态的思想定义5.1[序列上的抽象]设f：A→A是一个修改A中状态的函数。然后我们定义一个共归纳函数Tf：A∞→A∞，head（Tf（l））=Tf（head（l））和tail（Tf（l））=Tf（tail（l））。Tf通过将f应用于原始序列中的每个元素来变换给定序列Tf（l）称为l关于f的抽象。⬦定义5.2 [语义等价模抽象]设l和k是状态转移序列，l，k∈A∞。如果Tf（l）和Tg（k）相似，则l在语义上等价于k模抽象函数f和g⬦有了这个定义，我们在6.3小节中证明，如果忘记了辅助变量i和s的值，那么图3中的两个程序的语义在语义上是相等的。6程序转换在这一节中，我们证明了我们的共同代数方法的有用性，程序语言的语义和正确性证明程序转换验证的转换讨论的激励例子在第2节。S. Glesner等人理论计算机科学电子笔记176（2007）6173S为此，我们通过形式化4.1小节中给出的规则，在Is- abelle/HOL中指定了一个简单while语言的语义。一个国家被定义为作为函数State：Var→N，将变量映射到自然数。此外，我们还指定了函数step，它形式化了单个状态的执行，并返回新语句和新状态，其中计算继续进行：step：（Statement，State）~（Statement，State）。如果没有继承国，其结果是无效的这个转换函数允许我们通过为每个配置（每个状态和延续程序）分配一个潜在的无限状态转换序列，来以共递归的方式定义示例语言中程序state_sequence：：“配置文件状态项llist”state_sequence_def：“state_sequence C == llist_corec Cstep”在这一节中，我们证明了第2节中介绍的变换可以基于这种共代数语义并通过使用第5节中定义的相似关系来验证。在6.1小节中，我们从一个标准的互模拟证明开始，证明不可达代码可以被消除，参见。图1.我们在6.2小节中继续使用循环验证将循环不变代码移出循环，参见。图2.最后，在6.3小节中，我们演示了当转换涉及消除程序变量时如何使用抽象，参见。图3.6.1涉及经典共归纳情形的正确性证明考虑以下程序模板：PS：=whiletruedoi：=i+1od;S其中S是一个显然从未达到的任意陈述。因此，PS的语义应该独立于S。我们通过验证S的任意实例化S1和S2的两个状态转移序列相等来证明这一点：<$S1，S2，σ∈State. seq（P S1，σ）= seq（P S2，σ）通过证明两个状态转移序列处于互模拟关系来证明这一陈述是简单的。PS的配置只能有两个延续之一：PS本身，当循环体刚刚被求值时，以及PE：=（i：=i+1;whiletruedoi：=i+1od;S），当总是为真的条件已经在前一步中被检查时。在程序执行过程中，这个程序的延续在这两个延续之间无限地交替，由此定义的状态转换序列与S无关。关于Isabelle/HOL中seq（PS1，σ）=seq（PS2，σ）的共归纳证明的细节，参见。[12 ]第10段。6.2涉及折叠的正确在前面的小节中，两个程序的状态序列实际上是相等的。显然，情况并非总是如此。 作为示例，考虑图2中的循环不变代码的提取。为了验证它，我们需要证明（其中P174S. Glesner等人理论计算机科学电子笔记176（2007）61和P2是图2中的两个程序）：<$σ ∈状态seq（P1，σ）<$seq（P2，σ）在Isabelle/HOL中的程序转换的正确性证明中，关系式（cf.第5.1节）派上用场。为了证明两个懒惰列表是相似的，它可以证明存在一组包含（x，y）的懒惰列表对，使得关系式的共归纳规则成立：V相关系数：[[（a，b）∈ X;z. z∈X =<$z =（<$，<$）Themostimportanttechnologiesforthedevelopmentofthetechnologiesarethemostimportanttechnologies. z=（p@L，q@M）<$p<$= q<$（（L，M）∈X<$L<$M））]]=ab通常很容易找到这样一个集合X。在大多数情况下，由两个程序的迹组成的对被证明是等价的（程序通过的所有状态列表）可以被构造性地指定，并且具有所需的属性，即使它们是无限的。这些证明通常利用一个人可以“永远留在X中”的事实在我们的示例验证中，我们选择：X={（seq（P1，σ），seq（P2，σ）}σ在Isabelle/HOL中，我们已经验证了<$（x，y）∈Xx <$y，这是我们想要的结果。关于证明的细节，我们参考[12]。6.3涉及抽象的通过定义语义等价模抽象，cf。在定义5.2中，我们有一种方法可以将不同的状态转移序列相互联系起来。所使用的抽象函数可以重命名变量，仅投影到感兴趣的它们与非线性函数一起，使我们能够将有限状态的跃迁序列联系起来。例6.1再次考虑图3中的程序。它们的语义由A∞中的有限和无限状态转换序列来描述，其中每个状态都是程序中包含的变量到其当前值的映射（如果还没有定义，则为undef我们定义一个抽象函数f：A→A，f（a）={（x = v）|（x = v）∈ a<$ x/∈ {i，s}}这个函数通过忽略不感兴趣的变量i和s的当前值，将每个状态投影到其相关部分。定义一个包含（Tf（l），Tid（k））的坍缩很简单，其中id：A→A表示A上的恒等函数，l表示第一个程序的语义，k表示图3中第二个程序的语义。⬦S. Glesner等人理论计算机科学电子笔记176（2007）61757相关工作分别证明程序和系统的语义等价，已经在编译器验证领域进行了深入的研究。关于编译器验证的早期研究是在考虑编程语言Piton的翻译的Boyer-Moore定理证明器中进行的[14]。德国Verifix项目研究了在没有性能损失的情况下构建正确的编译器，参见[3]以获得概述。最近的工作集中在编译器前端的转换上。从Java到Java字节码的转换的形式验证和形式字节码验证在[11]中进行了研究。后者的工作是由Java的形式化工作和在定理证明器Isabelle/HOL中证明其类型安全的工作所预示的[16]。最近，共代数方法也被成功地用于编程语言和系统的规范和推理。在[7，9]中，面向对象编程语言的语义已经被共代数地定义VFiasco项目[8]的目标是验证一个具有煤炭地质方法的操作系统。[19]描述了共代数类规范语言CCSL。余代数证明方法不是唯一的形式主义捕捉的字符的语义non-terminating也可以使用标记的转换系统[13]。互模拟可以在两种形式主义中使用。我们的互模拟概念（操作于共代数数据集）和弱互模拟概念[13]（操作于标记转移系统）可以用于相同的目的：定义程序等价性直到可观察的步骤。在我们自己的工作[1]中，我们已经证明了一个死代码消除算法，用于编译器正确使用Kripke结构上的互模拟。在[5]中，我们描述了如何在编译器验证中使用余代数和余归纳。最后，我们在形式化和转换数据流相关计算方面的工作[2]也表明，正如本文所提出的工作，形式化的选择对于使用定理证明器时的证明成功至关重要。8结论我们已经提出了一个新的框架，程序等价的共代数验证。通过给每个程序分配一个合适的终结余代数的元素，我们也为非终结程序定义了语义。通过验证编译器中简单但典型的非细化优化，我们已经表明，我们的框架能够形式化在现代优化编译器中发现的转换的正确性证明我们还展示了我们如何将这个框架与定理证明器Isabelle/HOL中的正确性证明一起特别是，我们提出了两个不同的概念的正确性，并证明了它们的等价性在伊莎贝尔/HOL。虽然第一个概念很好地捕捉了数学直觉，但第二个概念更适合于机械化证明。有了这些结果，我们有助于如何在theo-rem证明器的形式化的问题，以简化机械化的证明，并减少76S. Glesner等人理论计算机科学电子笔记176（2007）61核查费用。为了能够也与不完全相同的状态转换行为的程序，我们引入了两种相似性关系（抽象和语义等价模抽象）。我们把状态转移序列对与连续状态的概念联系起来，这些状态转移序列对包含可能具有不同长度的连续相同状态的相应有限连续在一个坍缩中，我们把每一个这样的具有相同状态的有限子序列看作一个单一的状态。此外，语义等价模抽象的概念使我们能够将状态转换序列对，这两者都可以通过在它们上应用抽象函数元素来降低到一个共同的分母。这两个概念，再加上对状态转移序列的抽象，是验证语义等价的有力工具。有了它们，我们对语义对等的定义完全基于语义方面，而不是基于任何句法标准。如果原始程序和变换程序的状态转移序列的抽象包含在一个适当的折叠中，则每个变换都是正确的（相对于某些抽象函数）甚至两个语法上完全无关的程序在给定的抽象上也可以是语义等价的。如何选择抽象函数的问题取决于上下文，也就是说，取决于我们想要考虑什么是语义等价的问题。我们相信，这一框架的验证程序或系统转换，分别，也可以应用于软件工程的其他领域。今后工作的主题是进一步探讨这一点。引用[1] Jan Olaf Blech，Lars Gesellensetter，and Sabine Glesner. Isabelle/HOL中死代码消除的正式验证。第三届IEEE国际软件工程与形式化方法会议论文集IEEE Comp. Soc. Pr