高级语言程序变换的机械化证明导论/信息科学技术学术著作丛书

第1章 机械化定理证明的原理和逻辑基础 机械化定理证明是指使用计算机，以定理证明的方式对数学定理、计算机软硬件系统进行形式验证。这种机器智能的获得可归功于20世纪下半叶形式推理系统在计算机上的实现。20世纪50年代，机械化的定理证明围绕计算机如何高度自动化地完成证明展开，旨在证明数学定理。完全自动定理证明的局限性，以及来自数学领域之外，特别是计算机领域程序和硬件设计验证的需求，催生了60年代晚期交互式定理证明技术的出现。交互式定理证明工具应该尽可能地提供强大的自动证明能力。因此，我们从一阶逻辑（first-order logic）和基于消解（resolution-based）的证明技术展开论述。 相比基于消解的证明技术，自然演绎风格的推理更加自然。大多数交互式定理证明工具可以实现自然演绎形式的推理规则。自然演绎推理与类型化.演算之间的对应关系，以及Curry-Howard同构的发现，使逻辑学家和计算机科学家基于证明和程序之间的对应关系开发了一类强大的、以类型理论为基础的交互式定理证明工具。因此，本章接下来讨论自然演绎和Curry-Howard同构。 程序验证的巨大需求极大地推动了编程逻辑的研究，以及相应工具的实现。三种具有重要影响力的编程逻辑包括一阶编程逻辑、弗洛伊德-霍尔逻辑（Floyd-Hoare logic）和可计算函数逻辑（logic for computable functions，LCF）。对程序进行推理可以直接作用在编程语言的语义上，也可以使用特定的针对程序验证而开发的逻辑，如弗洛伊德-霍尔逻辑。因此，本章还讨论编程语言的语义和编程逻辑。 Gordon曾开发了一种相当激进，却很成功的基于高阶逻辑（higher order logic，HOL）的硬件验证技术。由此产生的各种工具在硬件验证领域，甚至软件验证和数学领域都发挥了重要作用。因此，本章还讨论基于高阶逻辑的硬件设计验证。 相比程序验证的后验方式，程序构造是一种构造即正确的技术。早期机械化程序构造采用基于消解的技术，之后许多研究者探索了逐步求精的程序构造，在并发程序验证领域结合时序逻辑进行深入研究，以寻求更好的机械化支持。因此，本章*后讨论这些技术。 1.1基于消解的一阶逻辑自动定理证明 自动定理证明要解决的主要问题如下。 （1）知识如何展现，即用什么语言表述定理。 （2）如何由已有的知识推导得到新的知识，即由已有定理（公理）推导新定理的推理规则。 （3）如何找到证明，即控制推理规则的使用。 自动定理证明*初使用相对简单的命题逻辑语言，但是命题逻辑所能表述的定理具有很大的限制性。相比而言，一阶谓词逻辑（简称一阶逻辑）具有更强的表述力和理论上的完备性，因此自动定理证明转而采用一阶逻辑。 后两个问题的解决相对更困难一些。通常，经验、洞察力，甚至直觉对定理的证明都会起到很大的作用。开发自动定理证明工具需要找到适合机器推理的方法。20世纪50年代中期，Quine[1]、Beth[2]、Hintikka[3]、Schütte[4]、Kanger[5]等独立发表了他们的研究成果。这些成果直接影响定理证明工具的设计。1957年，Prawitz使用自己设计的语言编写了用于证明一阶公式的程序。其基本思想是反驳证明法，即为了证明公式F，先假定F为假，然后推出矛盾。之后，他的父亲将该程序翻译为机器码，并在计算机上进行测试[7]。几乎同一时期，Gilmore加入国际商业机器公司（International Business Machines Corporation，IBM）的欧氏几何定理证明项目。他使用汇编语言，在IBM704上实现了Beth的semantic tableaux证明过程[8]。Prawitz[9]进一步提出合一的方法，改进了常量置换的方式。此后，许多合一算法都使用类似的计算方式。Davis等[10]考虑Skolem函数，使算法可以直接处理函数符号和Herbrand域。同时，他们提出待反驳公式的子句形式。这些子句形式成为反驳证明法的标准。Davis等提出的反驳法和单文字子句的消除规则，称为单元消解法。这是一种比Gilmore程序更有效的证明技术。在这些研究成果的推动下，Robinson[11]重新发现合一和消解规则（resolution rule/principle），并以优雅的方式将这两种功能强大的技术在IBM704上实现，称为基于消解的证明技术。 1.1.1消解规则和证明 消解规则形如下式，即 该规则表示如果两个子句都为真，那么可以推出为真。Robinson证明了仅具有这样一条消解规则的一阶逻辑系统的完备性。 基于消解技术的证明基于以下事实，即是合法的，当且仅当是不可满足的。因此，基于消解技术的证明算法是一种反驳法，首先否定待证明结论，与所有前提条件用逻辑与联结，得到一个新公式，然后运用消解规则进行推导，*后证明该公式的不可满足性。 为了运用消解规则，需要将待证明不可满足的公式转换为合取范式（conjunctive normal form，CNF）。该范式的所有合取分量形成子句集。在该集合中，对所有可能的具有互补文字的子句运用消解规则，将得到的新子句（消解子）加入子句集中。该过程被重复进行，直到不能再运用消解规则产生新子句，或者运用消解规则产生空子句。空子句表示初始推测的否是矛盾式，因此初始推测就是定理。如果不能得到空子句，那么初始推测就不是定理。例如，采用基于消解的技术证明以下命题逻辑公式，即 首先对该公式取否，然后将命题演算等值式转换为CNF。转换过程如图1.1所示。为了方便，我们将CNF的9个合取分量从左至右编号为①～⑨。然后，运用消解规则进行证明。证明时，首先在子句①和⑦上运用消解规则，消去互补文字对S和.S，得到消解子P R Q，然后在消解子和子句⑥上运用消解规则，消去互补文字对R和.R，得到消解子P Q，继续运用消解规则，*后推出空子句。因此，该命题逻辑公式是永真式，证明结束。命题逻辑公式的消解证明如图1.2所示。 图1.1命题逻辑公式转换为CNF 图1.2命题逻辑公式的消解证明 基于消解的证明技术适合机器推理，但是需要开发更多的控制技术来加速空子句的产生，提高证明效率。 由于量词和变量的出现，运用消解规则证明一阶逻辑公式比命题逻辑公式更为复杂。在运用消解规则之前，为了消除量词，一般将公式转换成前束范式（prenex normal form，PNF）。消去存在量词后的PNF称为Skolem标准形。为了消除存在量词，考虑以下两种情况。 （1）独立存在量词的消除。如果存在量词不出现在任何全称量词之后，那么用某个Skolem常量替换该存在量词所量化的变量，并消除该存在量词。例如，.x （x）转换为.（a），其中a是引入的Skolem常量。 （2）依赖存在量词的消除。如果存在量词出现在i个全称量词之后，设这些全称量词量化的变量分别为，则用Skolem函数替换该存在量词量化的变量，消除该存在量词。例如，转换为，其中量化变量y1和y2出现在一个全称量词之后。该全称量词量化的变量是x1，因此引入两个Skolem函数f（x1）和g（x1），消除这两个存在量词。量化变量y3的存在量词出现在两个全称量词之后。这两个全称量词量化的变量是x1和x2，因此再引入Skolem函数h（x1，x2），消除量化在y3上的存在量词。 1.1.2置换和合一 消解规则运用到一阶逻辑公式上时，需要考虑变量的置换问题。例如，假设子句集是。为了运用消解规则，需要匹配P（x）和.P（a），因此可将x置换为a，记为。置换后，得到的新子句集为。运用消解规则消除互补谓词公式对P（a）和.P（a），可以得到新的子句集。Robinson提出的合一算法虽然被成功地实现，但是效率很低。从计算复杂度的角度考虑，一种线性时间复杂度的合一算法由Martelli等[12]于1976年提出。Paterson等[13]于1978年提出更有效的算法。Martelli等[14]针对一阶谓词演算的合一问题，于1982年提出找到*一般合一子（most general unifier），即*一般置换（most general substitution）算法，并用Pascal语言编程实现该算法。下面对该算法简单介绍。 设有一系列表达式，θ是一个置换，记Eiθ是按照θ进行置换的结果表达式，称为Ei的实例。如果，则称是的合一子。如果存在合一子，则称是可合一的。例如，令，则，因此E1和E2是可合一的。 合一子不一定唯一。例如，令，因此θ2也是一个合一子。事实上，E1和E2的合一子还可以是和等。当有多个合一子时，需要具有唯一性的*一般合一子。 为了找到*一般合一子，首先需要定义作用在两个置换上的一个运算，即置换复合。设有两个置换θ1和θ2，记θ1°θ2为置换复合，令，则。如果，则删除；如果，则删除。如果对于的每个合一子，都存在一个置换，使，则称合一子的*一般合一子。例如，和的*一般合一子，其解释都是E1和E1合一子；对于θ1，存在一个置换，存在一个置换。对于θ3和θ4等，都可以类似推出。 下面给出利用消解规则证明一阶谓词公式的简单例子。假定待证明的公式是。首先，将待证明的公式取否，得到。然后，使用命题演算等值式进行替换，可依次得到和。继续使用量词否定等值式，得到。 利用独立存在量词消除规则，引入常量替换为，因此可得。*后，进行变量置换，得到。运用消解规则进行推理，产生空子句，因此得证。 1.1.3可满足性 消解规则围绕公式的可满足性进行。Davis等在1960年的论文中定义了命题逻辑公式是否可满足（satisfiable），即布尔可满足性问题，也称SAT。SAT是首*被证明的NP完全问题，因其在理论和工业应用的重要意义受到广泛关注。之后，Davis等[15]进一步提出著名的DPLL算法，成为当前许多SAT求解器的基础算法。 在SAT基础之上，可满足性模理论（satisfiability modulo theories，SMT）集成SAT求解器和逻辑理论的判定过程，可以处理具有相等的一阶逻辑公式。在实际应用中，程序验证可能需要组合多个逻辑理论，如算术理论、实数理论、各种数据结构等。Nelson等[16]于1979年提出组合多个理论的判定方法，简称N.O.方法。他们使用该方法开发了工具Simplifer，用在斯坦福的Pascal程序验证器中。N.O.方法也是许多组合理论判定方法的基础。Bozzano等[17]于2006年提出一种新的组合理论判定方法，称为延迟理论组合（delayed theory combination，DTC）。N.O.方法将多个理论的判定过程组合成一个求解器，再与SAT求解器进行交互。不同于这种处理方式，DTC方法将每个理论都直接与SAT交互，并且只与SAT交互。 当前许多成熟的SMT求解器在组合理论的判定方法上大多基于N.O.和DTC方法[18]，并做了进一步改进。微软公司开发的SMT求解器Z3是一个强大的自动定理证明工具[19]。SRIInternational研发的SMT求解器Yices已经集成在PVS定理证明工具中。Alt-Ergo求解器由法国国家信息与自动化研究所研发，CamlPro公司维护。刘尧等[20]开发了NuTL2PFG工具，用来判定线性μ演算（vTL）公式的可满足性。 SMT求解器常用于程序验证，即将程序需要满足的前后置条件、循环条件，以及断言翻译成SMT公式，然后用SMT求解器判定这些公式的可满足性，确定程序的性质是存在的。一个基于Z3的程序验证器是，也称为静态程序验证器。Alt-Ergo求解器用于Why3、SPARK，以及Atel