软件学报  2020, Vol. 31 Issue (1): 82-112   PDF    
机械化定理证明研究综述
江南1 , 李清安2 , 汪吕蒙2 , 张晓瞳2 , 何炎祥2     
1. 湖北工业大学 计算机学院, 湖北 武汉 430068;
2. 武汉大学 计算机学院, 湖北 武汉 430072
摘要: 随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的λ演算、3种编程逻辑、基于高阶逻辑的硬件验证技术、程序构造和求精技术之间的联系和发展变迁,其中,3种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare逻辑和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.
关键词: 定理证明    证明助手    消解    自然演绎    类型化的λ演算    编程逻辑    求精    
Overview on Mechanized Theorem Proving
JIANG Nan1 , LI Qing-An2 , WANG Lü-Meng2 , ZHANG Xiao-Tong2 , HE Yan-Xiang2     
1. School of Computer Science, Hubei University of Technology, Wuhan 430068, China;
2. School of Computer Science, Wuhan University, Wuhan 430072, China
Abstract: Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss. Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, FloydHoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed. Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.
Key words: theorem proving    proof assistant    resolution    natural deduction    typed λ-calculus    logics of programming    refinement    

计算机已经渗透到社会生产和人类生活的方方面面, 与计算机相关的各种故障足以造成巨大的经济损失. 2017年, 全球爆发的勒索病毒(WannaCry)源于Windows操作系统的漏洞(MS17-010);早在1994年, 奔腾处理器的浮点除运算错误使得英特尔公司不得不召回成百上千万芯片, 损失约4.5亿.更为严格的研发方法, 能够避免许多这样的错误.在这些方法中, 机械化定理证明是被学术界广泛认可的形式验证技术[1], 并在工业界获得了越来越多的成功应用.

机械化定理证明是指使用计算机, 以定理证明的方式对数学定理或计算机软、硬件系统进行形式验证, 是人工智能(artificial intelligence, 简称AI)的一种体现.Leibniz早在17世纪时就形成了由机器证明定理的思想, 然而直到19世纪末现代逻辑的创立和发展, 以及20世纪40年代计算机的出现, 才使得这一设想的实现具有了现实可能性[2].

始于20世纪50年代和60年代, 机械化定理证明围绕计算机如何高度自动化地完成证明而展开.受当时倡导的人工智能潜能的影响, 自动定理证明(automated theorem proving, 简称ATP)技术的研究经历了一段炽热的研发期, 也取得了许多具有影响力的成果; 但是随着新问题、新技术和新思想的到来, 完全自动定理证明的研究渐入停滞期, 对于大多数有意义的数学定理或计算机系统的正确性, 交互式地进行证明可能是唯一可行的工作方式[3].

交互式定理证明(interactive theorem proving, 简称ITP)在20世纪60年代开始呈现, 交互式定理证明工具也称为证明助手(proof assistant).交互式意味着用户能够引导证明过程, 在这个过程中, 用户使用某种语言编写证明纲要(outline); 证明助手自动填充证明的细节, 并检查证明, 最终机器完成整个形式证明.这种证明纲要的思想最初体现在Wang于1960年的著作中[4].McCarthy在1961年也指出:相比完全手工的数学证明, 由计算机检查的证明(纲要)可能更为简短和易于编写; 在证明(纲要)的引导下, 计算机能够生成大量证明细节, 并检查每步证明的正确性; 这些大量的、机械性的证明工作对于实际定理的证明来讲, 人工是很难胜任的[5].

自动定理证明最初旨在证明数学定理.不过, McCarthy同时指出:计算机能够检查的不仅仅是数学证明, 而且还包括复杂工程系统以及计算机程序是否符合它们的规范.事实正是如此, 从20世纪60年代晚期开始, 人们认识到许多其他问题, 譬如程序属性、专家系统和集成电路设计相关的许多问题等, 都可以表示为定理, 而由自动定理证明工具予以解决[6].并且, 对于程序的机械化验证而言, 交互式方式比完全自动化更为适用, 也促进了许多研究从完全自动化转换到交互式方式.

机械化定理证明的研究发展至今, 已经产生了比较成熟的证明助手, 如Isabelle/HOL(http://isabelle.in.tum.de/)、Coq(https://coq.inria.fr/)、HOL4(https://hol-theorem-prover.org/)、ACL2(http://www.cs.utexas.edu/users/ moore/acl2/)等.经过许多年的努力, 分别在Coq和Isabelle/HOL的支持下, 出现了首个验证的C优化编译器, 称为CompCert[79], 以及第一个验证的操作系统微内核seL4[1012], 已应用于安全攸关的工业开发中.这一领域的研究已经催生了每年举办的交互式定理证明(interactive theorem proving, 简称ITP)国际会议, 全世界范围的研究者们在这一会议上分享自己的研究成果.许多有关数据结构和算法分析、深度学习算法以及文件比较算法等研究成果也正在被机器验证[1316].

这些研究结果究竟是如何取得的?19世纪末, 德国哲学家、逻辑学家及数学家Frege试图证明“所有数学都可归为逻辑”, 结果创立了谓词逻辑; 20世纪, 德国数学家Hilbert试图证明数学是没有矛盾的, 他创建了现代证明理论; 荷兰数学家和哲学家Brouwer同样为了研究数学基础而开创了直觉主义的数学哲学[17].建立在这些基础之上, 许多数学家、逻辑学家和计算机科学家在进一步研究的过程中提出了新的理论, 在实践中不断发现新问题, 并给出有意义的解决方案.机械化定理证明的理论基石和支撑技术就来自这些交织进行的研究发展, 并在长达约60多年的持续研究过程中稳步向前推进.本文重点关注了对机械化定理证明具有重要影响力的理论和技术、相应的实现以及它们的应用.

本文第1节阐述与机械化定理证明紧密相关的概念和理论、主流或具有持续影响力的技术, 并剖析它们之间的联系以及变迁发展.第2节分析、比较各类证明助手的特点、开发和实现.第3节讨论它们在数学和计算机领域的应用现状, 并对编译器验证和操作系统微内核验证进行了详细分析.最后对机械化定理证明进行总结, 并提出面临的挑战和未来研究方向.

1 逻辑基础和关键技术分析

本节从一阶逻辑(first-order logic)和基于消解(resolution-based)的证明技术开始论述, 这是机械化定理证明研究得最久并仍然活跃的自动定理证明领域.然后, 论述将自然演绎和类型理论关联起来的Curry-Howard同构(correspondence), 它是当前以类型论为基础的证明助手的理论基石.接下来, 针对被广泛研究的程序的机械化验证, 讨论该领域主要使用的3种编程逻辑(logics of programming)和相关的编程语言语义(semantics).之后, 阐述在当时相当激进但却获得成功的基于高阶逻辑(higher-order logic)的硬件验证.最后讨论了程序构造(program construction)和求精(refinement)的方法.

1.1 一阶逻辑和基于消解的证明技术

自动定理证明要解决的主要问题是:

1) 知识如何展现?即用什么语言表述定理;

2) 如何由已有知识推导得到新的知识?即研究由已有定理(或公理)推出新定理的推理规则;

3) 如何找到证明, 即控制推理规则的使用.

自动定理证明最初使用相对简单的命题逻辑语言, 但是命题逻辑所能表述的定理太具限制性.相比而言, 一阶谓词逻辑(简称一阶逻辑)具有更强的表述力, 并具有理论上的完备性, 自动定理证明转而采用一阶逻辑.

第2)和第3)两个问题的解决相对更困难一些:数学家们或者人类在证明定理时, 人脑存储了许多已有知识.通常, 经验、洞察力、甚至直觉对完成定理的证明也起了很大作用; 开发自动定理证明工具需要找到适合机器推理的方法.Prawitz首次提出了通过计算进行合一(unification)的置换方法[18], 许多后来的合一算法都使用了类似的计算方式.Davis和Putnam于1960年提出了反驳法(refutation)和单文字子句(one-literal clauses)的消除规则, 称为单元消解法(unit resolution)[19].在这些研究成果的推动下, Robinson重新发现了合一和消解规则[20], 并以优雅的方式将这两个强大的技术实现在了IBM 704机器上[21], 称为基于消解的技术.

基于消解的证明技术迅速成为了广被研究的主题.大量研究开始深入探索启发式策略, 用来控制消解, 以减少证明搜索空间.许多启发式策略是领域特定的, 譬如适合平面几何的策略并不适合群理论.一些研究赞成更为通用的启发式策略, 将策略实现为作用在证明机制上的限制[22], 并研究施加了限制之后的一阶系统是否仍然是完备的, 能否证明所有一阶定理(不计时间和内存空间限制).到20世纪60年代晚期, 大量研究提出了一系列技术, 产生了丰硕的研究成果.然而, 接之而来的研究实验结果表明:随着待证明定理复杂性的递增, 自动定理证明工具所花费的时间甚至远远超出了人的寿命.在当时, 这种灾难性的结果因为Gödel的不完备性定理而被理解, 因为“在一致的、定义了算术的一阶逻辑系统中, 总存在既不能证明又不能证否的定理”.从20世纪70年代开始, 自动定理证明的重心开始转向有效性方面, 并在程序验证、专家系统、电路设计验证等领域发挥作用.

Davis和Putnam也定义了可满足的(satisfiable)命题逻辑公式, 即布尔可满足性问题(Boolean satisfiability problem), 也称为SAT, 并受到广泛关注.针对这个问题, Davis和Putnam以及Logemann和Loveland提出了著名的DPLL算法[19, 23], 成为当前许多SAT求解器的基础算法.在SAT的基础之上, SMT(satisfiability modulo theories)处理了具有相等的一阶逻辑(first-order logic with equality)公式.许多SMT求解器的开发相当成功, 如微软公司开发的Z3是一个强大的自动定理证明工具(https://github.com/Z3Prover/z3), 用于验证软件及电路设计.Liu等人开发了NuTL2PFG工具, 用来判定线性μ演算(vTL)公式的可满足性[24].当前, 开发SMT求解器的研究仍然活跃, 可满足性理论及其应用大会每年承办SMT-COMP竞赛, 评估众多SMT求解器(http://smtcomp.sourceforge.net/2018).

一阶逻辑自动定理证明本身的研究是非常具有意义的, 基于消解技术的具大影响力也一直持续到现在. Vampire被认为是当前相当成功的一阶逻辑自动定理证明工具(http://vprover.org), 它的研究始于1994年, 已连续多年获得由自动推理大会承办的自动定理证明工具竞赛的FOF(first-order formulas)组和CNF(first-order problems in conjunctive normal form)/MIX组的冠军.

值得指出的是, 早在20世纪60年代初, McCarthy就将语言设计作为他的优先研究领域:良好设计的语言能够很大程度地减轻编写证明助手的工作量; 他在1962年设计和实现了被广泛使用的人工智能语言Lisp.事实证明了McCarthy的正确:当前主流证明助手ACL2、Nuprl(http://www.nuprl.org)和PVS(http://pvs.csl.sri.com)等的实现语言就是Lisp方言Common Lisp.

1.2 自然演绎和Curry-Howard同构

基于消解的证明技术使用的是反驳法, 譬如, 如果要证明“由PQP可以推出Q”, 其过程是:首先, 用逻辑与操作将待证明结论Q的否¬Q和所有前提联结, 形成(PQ)∧P∧(¬Q), 再转换成合取范式(¬PQ)∧P∧(¬Q), 所有合取分量形成子句集{(¬P∨Q), P, (¬Q)}; 于是, 可在前两个子句上运用消解规则, 消除互补公式¬PP, 得到结果子句集{Q, (¬Q)}; 同理, 在剩余的一对子句上再次运用消解规则, 结果产生空子句, 因此初始推测就是定理.若不能继续运用消解规则, 而未产生空子句, 表示前提推不出结论.因此, 初始推测并不是定理.事实上, 上述证明的定理是肯定前件式(modus ponens), 它本身可以视为一个特殊的消解规则.

自然演绎系统通常并不否定待证明定理, 它力图自然地、像人类思考那样进行推理.自然演绎系统具有许多推理规则, 它们和简单类型理论的类型规则之间存在着对应关系.Curry-Howard同构的发现以及扩展, 使得逻辑学家和计算机科学家基于证明和程序之间的对应关系而开发出了强大的类型理论以及相应的证明助手.

1.2.1 自然演绎

Hilbert于1920年启动了称为“Hilbert’s program”的研究计划, 目标是证明数学是一致的(consistent):所有数学都可由正确选择的一套公理系统而推得.然而, Gödel的不完备性定理被广泛认为宣告了Hilbert研究计划的失败.尽管如此, Hilbert创立了现代证明理论.在他的演绎推理系统中, 公理定义了大多数逻辑操作符的语法, 而仅有一条称为肯定前件式的推理规则, 这使得有些公理看起来令人生畏, 譬如((P→(qr))→((Pq)→(Pr))).Łukasiewicz在1926年提出了改进Hilbert的公理系统, 他建议在推理规则的前提和结论中包括假定(assumptions), 允许由假定推得结论.响应于他的倡导, Gentzen于1934年设计了这样的系统[25].

Hilbert公理系统中的命题形如⊦A, 而在Gentzen设计的系统中形如B1, …, BnA, 表示“假定B1, …, Bn都成立的条件下, A是真的”; 将大写希腊字母Γ表示一系列命题B1, …, Bn, 则形如Γ⊦A.一个Gentzen风格的命题逻辑自然演绎系统如图 1所示.从图 1可以看出:为了更接近于真实的推理, 除了相等(identity)规则外, Gentzen为每个逻辑操作定义了一对规则:引入(introduction)和消除(elimination)[26]规则.

Fig. 1 A natural deduction system of Gentzen style (propositional logic) 图 1 一个根岑风格的自然演绎系统(命题逻辑)

Gentzen的初始动机是为了证明数论的一致性.为实现这个目标, 他提出了称为“子公式属性(subformula property)”的概念, 即“任何形如ΓA定理的证明都可以简化, 使得出现在简化证明中的定理只可能是A, 或者来自Γ, 或者来自AΓ”.Gentzen设计了“sequent calculi”作为技术手段, 阐明他的思想.在这个演算中, 定理形如B1, …, BnA1, …, Am, 称为sequent.Gentzen定义了一个cut规则, 如公式(2.1)所示:

$\frac{{\mathit{\Gamma } \vdash A, \mathit{\Delta }\quad \mathit{\Pi }, A \vdash \mathit{\Lambda }}}{{\mathit{\Gamma }, \mathit{\Pi } \vdash \mathit{\Delta }, \mathit{\Lambda }}}$ (2.1)

即“cut”掉了A的出现.然后, 他证明了“cut elimination定理”:任何使用了cut规则而得到证明的sequent, 都可以不使用该规则而得到证明.从这个意义上讲, 不使用cut规则的定理证明具有子公式属性.

这种简化的证明更易于机器推理.sequent推理演算系统事实上提供了一个方便的工具, 用于设计证明搜索算法, 该算法应用推理规则, 后向证明定理.Gentzen证明了一阶经典逻辑和直觉主义逻辑的sequent推理演算满足子公式属性, 并证明了具有一个无限归纳规则的算术公理系统的一致性.但是, 他不能证明形如Γ⊦A的自然演绎系统具有子公式属性.

自然演绎系统具有大量的推理规则, 控制这些规则的使用, 是实现机械化推理的重要手段.譬如, 对于A, BAB, 即从假定AB推出AB这样一个简单的定理, 机器可能会以一种相当繁琐的方式进行, 如图 2所示:通过推得(BAAB)和BA, 再利用肯定前件式推理规则完成证明.

Fig. 2 A roundabout mechanical proof of A, BAB 图 2 机器证明A, BAB可能的一个繁琐过程

图 2的证明过程可以看出:除了待证明定理A, BAB中出现的公式A, BAB以外, 还出现了BA.但是, 一个直接且简单的证明只应用两次相等规则和一次与引入规则就可以完成证明, 如图 3所示.与图 2的证明过程相比, 没有出现BA.事实上, 简化自然演绎的关键技术已经发表, 即Church的λ演算, 接下来我们对此加以分析.

Fig. 3 A simple mechanical proof of A, BAB 图 3 A, BAB简单证明过程

1.2.2 类型化的λ演算

Church于1940年提出类型化的λ演算[27], 称为简单类型理论(simple theory of types).“简单”一词可追溯到类型论的早期历史.Russell和Whitehead为解决朴素集合论中的悖论问题而系统性地论述了分支类型论(the ramified type theory)[28].分支类型一层来源于分支的分层(ramified hierarchy)这个概念, 即对类型进一步分阶(orders).在类型分层中, 个体具有的类型处于最低层, 高层类型的数学对象基于低层所构建, 构建的对象具有固定的类型.当形成集合时, 集合中的元素必须具有相同的类型, 设为τ, 而该集合的类型是τ set, 因此, 不可能构造出RR这样的命题:如果R的类型是τ, 它的类型不可能同时又是τ set.类型分层的引入, 避免了著名的Russell悖论[29].阶分层是为了避免“说谎者(liar)”这种悖论.然而, 阶分层出现了新的问题, 为此, Russell引入了可归约公理(reducibility axiom).最终, Russell的学生宣布:阶分层和可归约公理在“逻辑”悖论中是多余的, 该观点得到了Russell的认可.之后, Chwistek和Ramsey提出了去除可归约公理, 保留类型分层, 从而得到简化了的类型理论, 即简单类型理论.

最具有影响力的简单类型理论就是Church的类型化λ演算.在这个演算中, Church准确地形式化了包括量词的语法, 解决了原始λ演算中的不一致, 这项技术成为当前证明助手的标准[30].

λ演算的设计初衷是为了使用函数, 而不是使用集合来研究数学基础, 因此, Church设计了这种非常紧凑的函数书写形式.通常, 函数f的定义形式是f(x)=t, 其中, t是包含了x的项.在λ演算中, 书写为λx.t, 称为λ抽象.x取某个特定值u而产生一个函数返回值f(u), 对应的λ项书写为(λx.t)(u), 称为应用(application).t[u/x]也是一个λ项, 表达置换(substitution), 即tx的每个出现都置换为u.于是, 计算是项的归约.应用的归约规则如公式(2.2)所示:

$ \begin{equation} (\lambda x, t)(u) \Rightarrow t[u / x] \end{equation} $ (2.2)

其中, 符号⇒的意思是“归约为”.

为使得λ演算支持更多的数据结构, 进一步添加λ项:元组⟨t, u⟩, ⟨t, u⟩.fst和⟨t, u⟩.snd, 后两项分别表示取得元组的首元素和第2个元素, 相应的归约规则是公式(2.3)和公式(2.4):

$ \langle t, u\rangle .fst \Rightarrow t $ (2.3)
$ \langle t, u\rangle .snd \Rightarrow u $ (2.4)

λ演算中, 函数可以作为参数, 并可以返回函数.自然数n可以定义为一个λ函数, 该函数以函数作为参数, 应用了n次.

类型化的λ演算是给每个λ项指定一个类型, 以冒号表示.记AB为函数类型, 表示函数的形参类型是A, 而返回值类型是B.记AB为元组的类型, 表示元组中首元素的类型是A, 第2个元素的类型是B.因此, Church的类型化λ演算的片段如图 4所示.

Fig. 4 A fragment of Church's typed λ-calculus 图 4 Church类型化λ演算片段

类型论并未受到数学家们的欢迎, 但是通过Church的简单类型理论, 它得到了计算机科学家们的推崇:类型化的λ演算特别适合软、硬件系统的规范和验证.许多后来的类型系统都在这个简单类型理论的基础上进行了扩展, 增加了更为丰富的类型, 譬如多态和依赖类型, 因此从这个意义上也可以说, Church的类型化λ演算是简单类型的(simply typed).函数可以作为参数, 也可以返回函数; 量化可以不受限制地应用在所有阶的命题上, 简单类型理论也称为高阶逻辑(higher-order logic)[31].

相比集合论, 类型论在机械化解决许多问题方面更具有优势.譬如, 在集合论中可以书写被类型论视为不合法的各种表达式, 数学家们能从直觉上拒绝它们.但是操纵这些数学表达式的计算机并不具备这样的直觉, 如果不以某种策略方式告诉计算机区分不同类型的数学对象, 计算机的处理是相当低效的.此外, 自动推理系统中的一个基本操作是找到变量的合适置换, 区分不同实体的类型, 避免了大量无用搜索.

近些年来, 普林斯顿高等研究院(Institute for Advanced Study in Princeton)着手探究一种基于依赖类型的更复杂的类型论, 即同伦类型理论(homotopy type theory)[32].该理论使用homotopy这个代数拓扑学的分支来解释类型理论, 将类型视为空间(spaces).这个逻辑允许用相对简单的方式定义和计算代数拓扑里的基本群概念, 对于形式化数学有很大帮助.

1.2.3 Curry-Howard同构和扩展

图 1图 4可以看出:如果忽略类型化λ演算中的黑体加粗部分, 它和自然演绎规则是完全一样的.这种对应关系最早由Curry发现:组合子(可以视为一种无变量的λ表达式)的类型对应于Hilbert公理系统中的直觉主义命题逻辑公理.

直觉主义指的是Brouwer所代表的数学哲学思想.为解决朴素集合论中的悖论问题, Brouwer提出了与主流数学界完全不同的观点:悖论的存在说明了经典数学本身存在问题, 而不是因为数学家们在证明数学没有矛盾的方法上出了问题, 数学必须重新构建, 因此产生了直觉主义的算术、代数、集合论等等.Brouwer认为, 数学是人的思维活动, 数学由这样的思维活动一个接一个地归纳构造出来, 任何不能构造出来的东西都不属于数学.因此, 数学直觉主义哲学也称为构造主义数学.直觉主义拒绝排中律, 这在当时是一个相当尖锐的观点, 也因此没有得到主流数学的青睐.但是, 其“构造”的思想建立了直觉主义逻辑与计算之间的联系.

Gentzen的自然演绎在1934年发表, 但他不能简化自然演绎的证明; Church类型化的λ演算在1940年发表, 而类型化λ项的归约就对应着证明的简化; 直至1965年, Prawitz给出了自然演绎的全面总结, 他将大部分sequent推理演算工作都转换到了自然演绎框架中, 证明了自然演绎具有子公式属性[33]; 最后在1969年, Howard描述了自然演绎与类型化λ演算之间的对应关系, 称为Curry-Howard同构[34].在这个同构中, 直觉主义逻辑的命题公式对应于简单类型理论的类型, 称为“命题即类型(propositions-as-types)”, 或者“公式即类型(formulae-as-types)”.于是, 证明一个永真式(定理)等同于找到该类型的一个λ项, 因此也称为“证明即项(proofs-as-terms)”或者“证明即程序(proofs-as-programs)”.譬如, 对于图 3中每步证明中的命题逻辑公式, 都可以构建相应的λ项, 如图 5中的黑体加粗项所示.可以看出, 构建出来的λ项是一个元组⟨x, y⟩, 两个分量的类型分别是AB.

Fig. 5 A proof of A, BAB with type derivations 图 5 证明A, BAB的类型推导

进一步考虑, 根据图 2所示的证明过程, 所构建的λ项是(λz.⟨z.snd, z.fst⟩)(⟨y, x⟩), 其中, xA类型, yB类型.按照归约规则可以归约为⟨x, y⟩, 如公式(2.5)所示:

$ (\lambda z.\langle z.snd, z.fst\rangle )(\langle y, x\rangle ) \Rightarrow \langle \langle y, x\rangle .snd, \langle y, x\rangle .fst\rangle \Rightarrow \langle x, y\rangle $ (2.5)

因此, 项的归约对应着证明的简化; 并且, 项的归约不会改变类型.

在“命题即类型”下, 定理的证明过程是高度构造的.证明一个定理就是构造出给定类型的项, 证明规范化成了计算, 证明检查对应于类型检查.Curry-Howard同构为许多主流证明助手的开发奠定了理论基础.

对简单类型理论进行扩展, 从而支持更丰富的类型, 可以使得Curry-Howard同构扩展到更丰富的逻辑, 如高阶逻辑, 能够表达更多有意义的定理.在Martin-Lof构造类型论(constructive type theory, 简称CTT)中[35], 依赖积类型对应于全称量词, 依赖和类型对应于存在量词, 支持归纳类型.构造演算(calculus of constructions, 简称CoC)支持多态类型, 将Martin-Lof构造类型论扩展到二阶逻辑[36].归纳构造演算(calculus of inductive constructions, 简称CIC)扩展了CoC而支持归纳类型[37].

1.3 编程逻辑

对程序进行推理, 可以使用特定针对程序验证而开发的逻辑, 如Floyd-Hoare逻辑, 或者直接作用在编程语言的语义上.程序视为形式化的数学对象, 程序规范视为数学对象具有的性质, 因此, 程序验证可以理解成形式化的数学证明.下面我们来分析3种具有影响力的编程逻辑.

1.3.1 一阶编程逻辑及变体

一阶编程逻辑, 也称为函数式语义(functional semantics), 是指将程序视为由输入状态映射到输出状态的递归函数, 因此, 程序性质可以使用递归归纳(recursion induction)进行验证.这种方法由McCarthy提出, 他也建立了一种新的递归函数理论, 即条件表达式(the theory of conditional expressions)理论来支持该方法[38].基于条件表达式, McCarthy定义了一系列恒等式作为公理, 同时定义一系列推理规则, 譬如分配律规则等, 条件表达式理论形成了一套一阶逻辑形式系统.

McCarthy提出的这种方法将程序推理建立在递归函数上, 带有条件表达式的递归函数表达了程序语义.对程序性质进行推理时, 程序首先转化为递归函数, 递归函数的定义被翻译为逻辑等式.1976年, Cartwright和McCarthy展示了该逻辑能够用来推理递归函数的性质, 并适用于Pascal程序性质的推理[39, 40].深受McCarthy和Bledsoe[41]的影响, Boyer和Moore于1975年基于一阶编程逻辑的限制性变体(restricted variant of first-order programming logic)实现了LISP程序的定理证明工具, 称为“纯粹的Lisp定理证明助手(pure Lisp theorem prover)[42]”.这个开发具有突破性的意义:当时流行的基于消解的技术不能证明诸如串联结的结合律这类更有意义的定理, 为此, Boyer和Moore研究了归纳证明(proof by induction)技术[43].

归纳证明的机械化存在两个主要挑战:机器如何选择归纳变量以及如何找到有用的归纳公理[44].Boyer和Moore设计了显式归纳(explicit induction)技术, 用来生成显式归纳假定; 并且能够泛化(generalize)待证明的定理, 以更好地利用归纳技术.归纳和泛化技术是Boyer和Moore开发的自动定理证明工具的核心技术, 这个自动定理证明工具也包括重写(rewriting)等技术; 在证明定理时, 推荐优先采用诸如重写这类相对简单且更可控的技术, 当这类技术不能完成证明的时候, 才考虑归纳和泛化.

理论上讲, 一阶编程逻辑更适合于如Lisp这类函数式编程语言, 因为这类编程语言避免了将程序转换成递归函数的麻烦.此外, 一阶编程逻辑的表达能力不及高阶逻辑, 也在一定程度上制约了这种逻辑系统的广泛应用.

1.3.2 Floyd-Hoare逻辑

Floyd-Hoare逻辑也称为归纳断言(inductive assertions).1967年, Floyd提出了证明程序正确性的基本思想[45]:程序表示为流程图, 断言表示在流程图的边上.1969年, Hoare将流程图方式的断言表示为三元式, 由前置断言、程序和后置断言组成[46].Hoare给出了简单命令式语言成分的公理和推理规则, 称为Hoare公理系统.在这个公理系统中, 公理和命题都是形如{P}S{Q}的三元式, PQ都是一阶逻辑公式, 三元式表示的意思是:如果程序S执行前P为真, 且执行完后Q成立, 那么这个三元式成立.因此, 若一个命题{P}S{Q}为真, 其表达的意思是:如果P在执行S前为真, 并且S能够终止, 那么QS终止时为真.

Hoare公理系统吸引了众多学者对其展开后续研究, 这些研究包括循环不变式的构造、支持并发、指针等语言特性、终止性问题、该公理系统的可靠性和完备性问题等, 产生了很多研究成果.其中, 1975年, Dijstra提出了最弱前置条件(weakest precondition)和谓词转换器(predicate transformer)[47], 成为开发循环不变式的指导思想.

归纳断言系统除了需要自动定理证明工具之外, 验证条件生成器(verification condition generator, 简称VCG)是另一个重要的组成部分, 通过验证条件生成器将断言转换为验证条件, 即一阶公式, 然后再由自动定理证明工具进行证明.早期基于Floyd-Hoare逻辑的大型验证工具是Stanford Verifier和Gypsy Verification Environment(GVE)[48, 49].当前, 许多工业应用的程序验证工具都采用了这种基于验证条件的程序验证方式, 如Why verification platform[50]、the Spec# static program verifier[51]、ESC/Java2[52]、SPARK GNATprove[53]等.其中, Spec#语言是C#的扩展, 其源程序可以包括方法契约(contracts)、不变式、类、成员以及类型的注解(annotations); Spec#的设计代表着编译器验证(compiler verification)的一种方法:编译器在编译源程序的同时也处理注解, 然后验证条件生成器将它们转换成一阶公式, 通常由自动定理证明工具Z3进行证明.

在归纳断言这种方法中, 程序以及加在程序上的注解被转换成大量逻辑公式, 当这些公式未通过证明时, 难以确定究竟是程序出了问题, 还是注解出了问题.而支持封装、继承、多态等面向对象特性编程语言的语义复杂性更加剧了这一问题的严重性.

旨在验证程序正确性的霍尔公理系统也被看成是一种公理语义(axiomatic semantics).公理语义没有操作语义中“状态”的概念, 程序变量的取值反映在断言中, 语义建立在这种断言上:断言是关于程序中变量取值的逻辑公式, 这些值随着程序的执行而发生改变, 但是存在着某种保持不变的关系, 程序执行前的初始断言和执行后的终止断言反映了这些不变式关系, 表示了这段程序代码的语义.从这种意义上讲, 公理语义是一种不直接的语义定义方式.

1.3.3 可计算函数逻辑的方法

Milner于1968年实现了一个自动定理证明工具, 尽管他盛赞Robinson基于消解的证明技术, 但是他还是被这个工具所能证明出有意义定理的困难性所击败, Milner对机器辅助(machine-assisted)而不是完全自动的程序证明更感兴趣[54].1969年, Milner在牛津大学聆听了Scott的域理论(domain theory)[55], 他意识到可以运用这个逻辑定义程序语法和语义实现其设想, Milner将这个逻辑称为可计算函数的逻辑(logic for computable functions, 简称LCF).于是, 他于1972年在斯坦福大学开发了一个证明检查器(proof checker), 称为Stanford LCF[56].为方便实现, Milner将类型化的组合子(combinators)转换为λ表达式, 类型解释为Scott域(domains), 逻辑公式是谓词演算公式.在证明机制上, 用户使用证明命令与Stanford LCF进行交互, 将待证明的定理(称为目标)分解为子目标, 子目标通过简化器(simplifier)得到证明, 或者进一步分解为更简单的子目标, 直到这些子目标全部得到证明.在分解子目标时, 代表着形式证明的数据结构被创建, 因此消耗了大量存储空间.

为了能够灵活地添加证明命令而不损害可靠性, 并可节约存储空间, Milner等人于1973年~1978年设计了Edinburg LCF[57].Edinburgh LCF不存储整个证明的数据结构, 只存储证明的结果, 即定理.为了确保定理只能由证明产生, 一个抽象数据类型, 称为thm, 用来表示定理的类型.它的预定义值是公理, 在这个类型上的操作只能是推理规则.推理规则实现为函数, 因此, 严格的类型检查将保证所有thm类型的值只能通过公理, 并使用推理规则而得到, 这种经由推理得到的定理保证了它的可靠性.此外, 这种将定理表示成抽象数据类型的方式使得这个机器证明工具支持了前向证明.

为了方便证明命令的扩展和使用, Edinburg LCF设计了函数式编程语言ML(meta language), ML是严格类型化的, 用来支持抽象类型机制.分解待证明目标的证明命令如推理规则一样, 也实现为函数, 称为策略(tactics).策略是由目标(goal)到子目标(subgoal)的函数.策略能够以不同的方式组合成为新的策略, 组合方式也是一个ML函数, 称为tacticals.策略可以视为推理规则的逆, 支持了后向证明.可编程的Edinburgh LCF为用户提供了更多与机器的交互, 但并不损失可靠性.

Edinburgh LCF为证明助手的开发建立了一个标准框架, 许多后来的证明助手或多或少都采用了其中的核心技术特点.这些证明助手包括对Edinburgh LCF进行了大量改进和完善的Cambridge LCF[58]、始于硬件验证的HOL系列[59]、基于Martin-Lof类型理论的Nuprl[60]、Isabelle和Coq等.

Milner成功地将斯科特的域理论应用在实践中, 而域理论为Strachey.20世纪60年代所提出的指称语义(denotational semantics)奠定了数学基础[61].由于指称语义以数学递归函数定义语义, 具有组合性(compositiona- lity)特点, 使得指称语义直接支持了两个语义等同语言成分的置换.这种组合性建立在其抽象生成规则所产生的语法成分的“结构(structure)”上, 称为语法制导的(syntax-directed).因此, 程序性质可以使用结构化归纳(structural induction)进行推理.但是, 严格的数学特性也导致了指称的困难; 并且, 指称语义在指称并发时相当复杂, 需要引入新的模型.从某种程度上看, 指称语义可能过于“数学化”, 而并不方便编程语言的设计.指称语义在20世纪70年代占据了主导地位, 之后让位于基于规则的操作语义(rule-based operational semantics), 即结构化的操作语义(structural operational semantics, 简称SOS)[62]和自然语义(natural semantics)[63], 它们分别也称为小步(small-step)和大步(big-step)操作语义.

由于指称语义的状态是程序状态, 即程序中各变量的取值, 它纯粹使用数学函数来定义状态的变化, 这使得LCF方法在推理程序的方式上非常不同于上述讨论的一阶编程逻辑和Floyd-Hoare逻辑.一阶编程逻辑和Floyd-Hoare逻辑都将程序语义嵌入在某种算法中:一阶编程逻辑将程序的语义转换为带有条件表达式的递归函数; Floyd-Hoare逻辑将程序语义通过验证条件生成器转换为验证条件; 而在LCF逻辑中, 程序是这个逻辑系统所操纵的对象, 因此程序的语义可以显式定义, 这也称为嵌入(embed)编程语言到证明助手中.事实上, 在Isabelle/HOL和Coq等证明助手中, 可以方便地定义大步操作语义和小步操作语义.程序的许多性质, 譬如程序的相等性、程序变换以及一致性和终止性等, 都能够方便地在证明助手的逻辑系统中得到表达.

从另外一方面来看, 由于Hoare逻辑是一种特定用于程序验证的逻辑, 证明程序的性质会更直接.为了充分利用LCF方法和Hoare逻辑的优势, Gordon、Mehta和Nipkow分别使用证明助手HOL和Isabelle/HOL, 将Hoare逻辑实现为推理出来的规则[64, 65], 保证了Hoare逻辑的可靠性.以这种方式, Hoare逻辑被优雅地嵌入在高阶定理证明助手中, 使得在这些证明助手内可以使用Hoare逻辑进行程序验证.

1.4 基于高阶逻辑的硬件验证技术

20世纪70年代, 定理证明工具的设计与实现围绕一阶逻辑而展开, 这在很大程度上是因为一阶逻辑具有很强的理论属性, 如完备性.然而, Gordon指出:这类属性对于验证是不相关的, 而简单类型理论, 即高阶逻辑所具有的额外表述力对于验证而言却是必要的[66].Gordon对高阶逻辑的研究是与硬件验证联系在一起的, 这不同于当时绝大多数的验证研究:出于历史原因, 也可能因为当时的硬件设计并不那么复杂, 除了Wagner于1977年使用FOL初步尝试了硬件验证[67]以外, 几乎所有其他同时代的验证研究在本质上都是以软件为主的.

当Paulson正在剑桥致力于Cambridge LCF的开发时, Gordon也正在剑桥从事着硬件验证的研究, 因此他对Cambridge LCF非常熟悉.Gordon对Milner所开发的通信演算系统(communication calculus system, 简称CCS)留有深刻印象, 他认识到:通过并行组合硬件系统中个体结构的描述, 可以计算推理得到整个硬件系统的行为.于是设计了称为LSM(logic of sequential machine)的符号, 用来表示机器的顺序行为, 并构造了一条类似CCS的Expansion Theorem的规则.接下来, Gordon对Cambridge LCF进行了改进, 使之适合LSM.这个改进的证明助手获得了初步成功, 对Viper处理器进行了规范和正确性证明[68].同时, 在剑桥攻读博士后的Moskowski向Gordon提出LSM中的项可用谓词逻辑进行编码, 使得LSM的Expansion Law可以推理得到, 而不是构造为公理.这种方法既优雅又具有更牢固的逻辑基础, 于是HOL诞生.

高阶逻辑的选择在当时相当激进, 譬如高阶合一在理论上是不可判定的, 不过在实际中, Huet开发的半可判定的高阶合一算法[69]在证明助手中表现得相当可靠[70].Gordon和他的学生继续扩展了这项技术, HOL进化成了HOL4.HOL吸引了许多研究者的兴趣, 他们开发出了不同版本, 形成了HOL系列[71].基于高阶逻辑的硬件验证技术具有很好的递增性, 可以验证单传感器设备, 也可以验证整个计算机, 囊括了大量数字系统, 包括浮点小数硬件、概率算法以及其他许多应用.

1.5 程序构造和求精

程序构造(program construction)也称为程序综合(synthesis), 是指由规范(specification)构造出具体程序.一个主要方法是将由规范到实现的过程视为一系列对数据结构和控制结构进行求精(refinement)的程序变换, 因此, 程序构造也常和求精这一术语联系在一起.

逐步求精(step refinement)的程序构造技术最初由Dijstra[72]和Wirth[73]提出.这是一种构造即正确(correct by construction)的方法:如果每步求精都能够谨慎地执行而保持了正确性, 那么最后的程序一定是正确的.但是, 实际算法和数据类型在实现过程中所包含的每步求精并不简单, 直觉远远不能判断其正确性.Gerhart明确提出了程序变换正确性概念[74].Burstall和Darlington提出使用预定义的一套程序变换规则构造每步求精[75], 许多理论研究围绕这种方法而展开, 这些方法大多并不利用定理证明技术, 而是将规则直接应用到规范上.不过, Manna和Waldinger研究了使用定理证明的方法进行程序构造[76].

旨在将逐步求精和程序变换与基于不变式的方法统一起来用于程序构造, 在一系列研究积累之上, Back利用Dijstra最弱前置条件演算, 于1988年提出了求精演算(refinement calculus)[77]:如果语句S的最弱前置条件能够推出语句S'的最弱前置条件, 那么S'是S的正确求精; 证明等同于计算它们的前置条件, 使得表达了这个正确性的一阶逻辑公式为真.李彬等人提出了一个通过抽象程序证明复杂具体程序的框架, 使得满足一致性比较容易得到证明, 并可能自动证明[78].

求精演算会产生大量既冗长又易错的谓词公式, 需要完成的工作非常艰巨.一些研究开始寻求机械化手段来支持求精演算[79, 80], 这些工具通常由验证条件生成器和自动定理证明工具两个独立部分组成.不同于这种方式, Back和Wright使用HOL, 在一个工具中实现了他们所设计的形式系统, 证明了许多求精规则[81].经过机器检查的规则, 避免了预定义程序变换规则可能存在的不一致性问题.Wright进一步利用HOL的窗口推理工具(window inference tool)(该工具支持程序变换风格的推理), 建构了一个用于求精的原型工具[82].

求精的思想也由Abadi和Lamport用来证明分布式程序的低层规范正确实现了高层规范, 称为求精映射(refinement mapping)[83].Lamport进一步将求精映射和时序逻辑(temporal logic)相结合, 提出了行为时序逻辑[84].Jonsson和Lynch等人泛化了求精映射, 称为模拟(simulation)[85, 86].这些方法和技术通常以模型检查(model checking)或者模拟技术而不是以定理证明的方式对并发程序进行验证.不过, Pnueli等人使用时序逻辑, 以定理证明的方式提出了一种对并发程序进行构造的算法[87].

一个获得了工业级应用的逐步求精工具是B方法的工具包Atelier B[88, 89].B方法以一阶公理化ZF (Zermelo-Fraenkel)集合论为基础; 1998年, Atelier用于巴黎城市地铁14号线全自动无人驾驶系统.

基于定理证明方法的求精工具较为少见.就目前我们所知, Isabelle/HOL通过Locales机制支持逐步求精. Cornell大学的PRL团队维护着NuPRL的开发, 其中, PRL代表证明或程序求精逻辑(proof/program refinement logic).从技术发展上看, 求精的概念和应用非常宽泛, 譬如可以应用在编译器验证的研究中.

2 证明助手特点比较和实现

已经详细剖析了证明助手的主要理论基础和关键技术, 接下来讨论证明助手的实现和应用.限于篇幅, 仅针对部分主流证明助手的设计特点进行分析比较, 阐述具有代表性的证明助手的开发与实现.

2.1 设计特点比较

证明助手的设计与实现并不像传统软件开发那样具有规范化的标准可以遵循, 特别是在早期阶段.从历史发展上看, 它的开发是一个从错误中不断修正、渐趋成熟的过程.不同证明助手之间相互影响, 一些完成了它的历史使命而终止开发或者进化成新的证明助手, 一些仍然活跃.在这个过程中, 逐步形成了开发一个现代证明助手所需要考虑的重要特点.本节先比较这些设计特点, 然后重点阐述几个具有代表性的证明助手的开发和实现.

针对证明助手的可靠性和使用性, 表 1对部分主流证明助手的设计特点进行了比较.

Table 1 A comparison of features of some mainstream proof assistants 表 1 部分主流证明助手的特点比较

各项特点分析如下.

(1) 小核

证明助手用来验证数学、计算机软/硬件的正确性, 它们本身是正确可靠的吗?一方面, 鉴于机器证明的机械刻板性, 即使存在某些缺陷, 它在证明定理时所具有的可靠性量级也远胜人工证明; 另一方面, 通常认为:如果一个证明助手具有相对较小的内核, 所有其他推理规则都是基于小核中的规则来定义的, 那么, 需要信任的就是这个小核[90]; 相对较小的内核更值得信任, 因而更可靠.

在LCF方法的证明助手中, Agda、Coq、Nuprl和PVS是基于类型理论的, 它们通常会生成证明对象, 由一个相对简单的证明检查程序进行检查, 这个小程序可被认为是一个小核, 不过, PVS的设计者并不太关注理论上的可靠性, 而持有相当松散和实际的正确性观点, 本文中标记为“—”; LCF方法的直接后代:HOL4、HOL Light以及Isabelle本身就是基于非常小的可信内核来设计的.

ACL2在设计时注重强大的自动推理能力和使用上的方便; Mizar旨在建立形式化验证的数学知识库.因此, 对这两种证明助手不按小核标准进行比较, 显示为符号“—”.

(2) 声明/过程式证明语言

用户使用证明助手支持的证明语言与证明助手进行交互.证明语言可分为声明式和过程式两种:前者指出证明什么, 后者指明如何进行证明.因此, 声明式的证明可读性较高.

在早期基于LCF方法证明助手的开发中, 策略脚本是传统过程式的, 其晦涩难懂性与Mizar声明式证明语言的相对高可读性形成了巨大反差, 因此, Harrison倡导Mizar声明式证明语言[91].虽然HOL Light支持声明式语言, 但并不常用, 因此标识为过程式.Isabelle于1999年支持了声明式的证明语言Isar[92].Coq的证明语言是过程式的, 不过, Gonthier等人为Coq设计了Ssreflect(small scale reflect language), 能够声明式地用于证明的高层结构中, 但在低层结构中切换到过程式[93], 因此在表中也标识为过程式.Nuprl的证明语言更接近于将声明式和过程式加以综合[94].自动定理证明工具, 如ACL2的证明语言可以视为声明式的:在这样的证明助手中, 仅陈述(声明)待证明的定理, 或书写一些中间定理, 证明助手自动完成证明任务.Agda支持声明式的证明.

(3) 实现语言

大多数证明助手, 譬如Coq、Isabelle等都是以函数式编程语言编写的, 譬如Haskell、Ocaml、Common Lisp、Standard ML以及Scala等.不过, Mizar的实现语言是Free Pascal, Free Pascal是Pascal编译器, 其目标平台包括多种处理器架构, 如Intel x86、AMD64/x86-64、PowerPC、MIPS和JVM等.

(4) 代码生成

许多证明助手支持代码生成, 或称为程序抽取(program extraction).代码生成是指将在证明助手中以证明语言书写的各种定义翻译成可执行的函数式程序, 可以独立运行.譬如, Isabelle/HOL可生成SML、OCaml和Haskell程序, Coq可以生成Ocaml、Haskell和Scheme程序, PVS可以生成Common Lisp程序, ACL2和Agda本身是可执行的.Mizar旨在建立合适的数学语言对数学进行形式定义和证明, 因此对它不考虑代码生成这个特点, 显示为符号“—”.

(5) 用户界面

证明助手建立在函数式编程语言之上, 使用命令行方式与之进行交互.Aspinall于1999年开发了Proof General[95], 许多证明助手的早期版本支持一种称为Emacs模式的图形用户界面:交互依然是基于一系列命令, 但是可以区分未检查的证明和已检查的证明, 用户可以一步步地引导证明, 证明助手返回结果.Emacs界面模式主导了Isabelle和Coq的开发约10年之久.

一种不同的方法是通过证明助手集成开发环境框架(prover IDE framework, 简称PIDE)完成.PIDE非常类似于现代软件集成开发环境, 用户在输入源码时, IDE就检查语法.Coq和Isabelle现已支持这种用户界面, 分别称为GTK-based CoqIDE和the Isabelle/jEdit IDE[96, 97].ACL2团队开发了Eclipse插件, 称为ACL2 Sedan theorem prover(ACL2s), 供用户与ACL2进行交互.Mizar旨在建立数学知识库, 为了更好地进行测试, Cairns为Mizar开发了一个用户界面Alcor, 方便用户与这个知识库进行交互[98].

以上分析比较了主流证明助手的设计特点, 为了更好地理解证明助手的设计, 图 6给出了联系比较紧密的证明助手之间的开发进化及影响关系, 黑体标识的是当前仍然活跃的证明助手.一些证明助手, 如ACL2、PVS和Mizar的设计相对独立, 没有包含在图 6中.

Fig. 6 Evolvement of proof assistants and influences on each other 图 6 一些证明助手的进化以及之间的相互影响

总体上讲, Milner设计的Edinburgh LCF和Bruijn设计的Automath[99]是具有先驱性的两大证明助手, 并且这两大证明助手衍生系统的开发也是交叉影响的.Bruijn基于他自己设计的依赖类型理论而实现了Automath, 可以说, 他独立发现了Curry-Howard同构[3], 以“证明即对象(proofs-as-objects)”的方式体现在Automath的开发中.Automath旨在准确地表达所有数学并进行验证, 尽管Automath几乎没有被广泛使用过, 但是它对许多以类型理论为基础的证明助手的开发都产生了很大影响.接下来, 我们分别阐述几个具有代表性的证明助手的开发和实现.

2.2 主要证明助手的开发和实现 2.2.1 Isabelle/HOL

Isabelle/HOL是当前被广泛使用的、LCF方法的证明助手, 它是建立在Isabelle元逻辑(meta-logic)之上的一个目标逻辑(object logic).Isabelle元逻辑也称为Isabelle/Pure.

Paulson于1985年开始Isabelle的开发, 他考虑以元逻辑, 即通用的、适用于多种特定逻辑的证明助手的开发.以Paulson的观点来看:许多特定逻辑证明助手开发的困难性都是类似的, 故开发通用证明助手可以一劳永逸地解决这些难题, 而将特定逻辑要解决的特定问题留给特定逻辑, 由以元逻辑为基础的目标逻辑去处理.

这种观点也体现在Edinburgh逻辑框架(logical framework, 简称LF)中[100].在第1.3.3节所述的Edinburgh LCF完成之后, 在爱丁堡大学的开发重心转移至逻辑框架和构造类型论上, 导致的系统称为Edinburgh LF, 之后进化为Twelf.另一个逻辑框架是ALF(another logical framework), 最后成为Agda.

在这些以逻辑框架为设计思想的证明助手中, Isabelle是唯一得到广泛应用的证明助手, 它可以视为LCF方法和逻辑框架的联合.

Isabelle元逻辑的实现基础是Church的简单类型理论, 是具有蕴含、全称量词和相等的高阶逻辑, 推理规则不是前提到结论的ML函数, 而是前提蕴含结论的公理, 允许目标逻辑以自然演绎风格进行构造.Isabelle/Pure并未利用类型化λ演算与自然演绎之间“证明即程序”的对应关系, 没有显式的计算, 不显式生成独立可检查的证明对象.这种方式称为LCF方法的直接后代, 区别于使用了LCF方法, 但以类型理论为基础而设计的证明助手.

受Huet的启发, Isabelle实现了高阶合一, 在高阶合一的基础上, Isabelle支持许多自动推理工具, 从而具有强大的自动推理功能:高阶重写的简化器Simplifier、结合了Metis证明工具的经典推理器(the classical reasoner)和经典Tableau证明工具; 支持使用外部自动定理证明工具, 如Vampire、SPASS的Sledghammer工具; 支持反例搜索的Quickcheck和Refute.此外, Isabelle使用Locales处理参数化的理论, 支持了模块化的理论开发(modular theory development).

由元逻辑Isabelle/Pure可以构造许多不同种类的目标逻辑(object logics), 譬如经典和直觉的一阶逻辑(Isabelle/FOL)、Martin-Lof构造类型理论(Isabelle/CTT)、一阶ZF集合论(Isabelle/ZF)以及经典的高阶逻辑Isabelle/HOL等, 如图 7所示.

Fig. 7 Meta-logic and object logics of Isabelle 图 7 Isabelle元逻辑和目标逻辑

Isabelle/HOL是当前使用最多的一个目标逻辑, 在图 7中以黑体标识, 主要由Nipkow于2002年完成[101].从用户的观点看, 该目标逻辑可以理解为函数式编程和逻辑的结合, 供用户用来交互的编程语言类似于Haskell.利用Locales, 在Isabelle/HOL中可以表达由抽象规范到具体数据结构和算法的逐步求精的概念.此外, Isabelle/ HOL能够充分利用多核处理器进行并行证明[102, 103].Isabelle/HOL仍然在不断改进和完善中, 当前的稳定版本是Isabelle 2019.许多有关安全协议、数学、编程语言和系统验证等众多领域的正确性问题都可以在Isabelle/HOL内进行描述并得到验证.

2.2.2 HOL系列

Gordon在剑桥大学为研究硬件验证而开发了HOL.历经了数个版本的改进完善之后, 当前最新版本为HOL4.HOL也衍生出了新的证明助手, 这些统称为HOL系列, 如图 8所示, 其中, HOL4、HOL Light、HOL Zero (http://proof-technologies.com/holzero/index.html)以及ProofPower(http://www.lemma-one.com/ProofPower/index/)现仍然在开发和维护中, 它们都是经典的高阶逻辑.HOL light由在Intel公司工作的Harrison于1994年推出.虽然始于硬件验证的动机, HOL系列也可以进行算法和程序验证, 并支持进程代数以及极限理论、微分和积分等经典数学验证.

Fig. 8 Evolvement of HOL family 图 8 HOL系列的进化

2.2.3 Coq和Nuprl

1984年, 法国国家信息与自动化研究所INRIA的Huet和Coquand决定实现构造演算(calculus of constructions, 简称CoC), 初始版本是一个证明检查器, 紧接着采纳了LCF方法的策略方式, 导致的系统可以视为Automath的Martin-Lof构造类型论的扩展, 综合了依赖类型和多态.之后, Mohring实现了称为Auto的证明搜索策略, 代表着Coq证明助手的诞生.Mohring和Coquand于1988年开始设计归纳构造演算(calculus of inductive constructions, 简称CIC).之后, Coq经历了反复的重设计和实现, 当前, Coq的稳定版本是8.8.0.一个新的扩展是Coq团队开始实现同伦类型理论.

Nuprl是康奈尔大学的PRL(proof/program refinement logic)研究团队的Constable等人于1986年开发的证明助手, 实现的也是Martin-Lof的构造类型论.PRL团队一直致力于开发基于逻辑的编程工具和实现构造主义的数学, 当前的稳定版本是Nuprl 5.2003年, Hickey等人以逻辑框架的思想重新实现了Nuprl, 称为MetaPRL (http://metaprl.org).

Coq与Nuprl都是使用了LCF方法且以类型理论而设计的证明助手.这类证明助手基于非简单的类型理论, 即依赖类型等.利用命题即类型、证明即项的思想, 类型化的λ项既用于表示逻辑定理, 又表示证明, 通过依赖类型, 类型检查执行了大多数推理任务.

2.2.4 ACL2和PVS

ACL2始于Boyer和Moore于1973年开发的纯粹Lisp定理证明工具, 该工具解决了归纳证明的机械化问题, 如第1.3.1节所述.之后, Boyer和Moore继续对其进行完善.20世纪80年代中期, Kaufmann加入了开发团队.经过多年的持续改进, Boyer和Moore终于实现了他们在1973年设计自动定理证明工具的目标:ACL2(a computational logic for applicative common Lisp)诞生[104], 其效率远远超出了设计之初的纯粹Lisp定理证明工具, 而成为工业可用的工具, 并于2005年集成到Centaur公司的开发流程中.为充分利用多核处理器的功效, ACL2和Isabelle/HOL一样也处理了并行证明的问题[105].当前, ACL2的稳定版本是8.0.

PVS是Prototype Verification System的简称, 由SRI公司于1992年开始研发.PVS和ACL2一样具有强大的自动化证明能力, 但是PVS也意图提供如证明助手所具有的强表述力和逻辑, 提供了类Lisp语言供用户与之进行一定的交互.PVS是经典类型化的高阶逻辑, 但不像Coq和Nuprl那样产生独立可检查的证明对象.PVS当前的稳定版本是6.0.

3 机械化定理证明应用成果分析

从第一个定理证明工具至今, 经过约60多年的持续研究, 机械化定理证明在实际应用中产生了丰硕的研究成果, 以下从数学、编译器验证、操作系统微内核验证、电路设计验证等几个具有影响力的研究领域来讨论所取得的应用成果.

3.1 数学定理的证明

最早提出“数学机械化”思想, 并做出卓越贡献的是美籍华裔数理学家王浩先生.他于1959年编写了一个计算机程序, 实现了带有相等关系的谓词逻辑, 在很短时间内证明了Russell和Whitehead所著的数学原理中的几百条定理.秉承数学机械化的思想, 针对几何定理的机器证明, 吴文俊在1977年提出了“吴方法”:待证定理由坐标间的代数关系表示, 从而将平面几何问题代数化; 再通过多项式的消元法进行验证[106].这种方法既可以手工完成, 又可方便地以计算机编程进行实现, 这种方法被进一步推广到一类微分几何问题上.1996年, 杨路和张景中等人建立了多项式完全判别系统[107], 使得不等式的机器证明成为现实.1999年, 杨路和夏壁灿等人进一步编制了研究半代数系统(semi-algebraic-system)实解的新软件包DISCOVERER[108].DISCOVEREER现已集成到Maple工具箱, 在自动求解参系数半代数系统实解分类问题上具有优势.

许多数学家们都接受了使用证明助手来证明数学定理.van BJLS使用Automath形式化了由Landau所著的数学教科书中的定理[109].旨在设计具有强表述力的数学语言, Trybulec开发了Mizar[110], Mizar库已经成为当前最大的形式化验证的数学知识库.此外, 形式化数学越来越多地用于验证目的.Hurd使用HOL形式化了概率论, 验证了Miller-Rabin概率素性测试[111].Holzl使用Isabelle/HOL形式化了马尔可夫链[112].

表 2列举了几个具有代表性的机器证明的数学定理.其中, 开普勒猜想和四色定理的证明是两个非常具有说服力的例子.Hales于1998年给出了长达300多页的开普勒猜想证明, 并辅以40 000行的程序代码, 经过长达4年的评审之后, 因其代码的不可信而被拒绝.于是, Hales启动了一个联合项目Flyspeck, 多个研究小组使用不同的证明助手共同完成证明:HOL Ligth提供欧氏几何背景知识; Coq用于非线性的不相等验证, 之后改为使用Isabelle/HOL完成该验证; Isabelle/HOL用于图枚举和线性编程.Flyspeck项目获得了成功, 确定并简化了Hales的证明, 它是迄今为止完成的最大的形式化证明[113, 114].四色定理的机器证明也非常有意义.Appel和Haken于1976年完成了四色定理的证明[115], 他们使用一个计算机程序检查了近2 000个实例, 争议由此产生.虽然争议在Robertson等人于1996进行了优雅的修正后而可能平息, 但是缺陷仍然存在:这两个证明都使用了计算机代码, 而这些代码超出了人工评审的能力, 却又没有经过机器检查.最后, Gonthier使用Coq证明了四色定理[116], 用来检查实例的算法在Coq中进行了验证.

Table 2 Lists of some representative mathematical theorems which are machined checked 表 2 几个具有代表性的机器证明的数学定理列表

数学的机械化证明能够清除疑问, 解决模糊性, 并发现错误.正如Lakatos指出的:数学家们常会出错, 有时甚至连定义都会出错[117].因此, 形式化验证数学的驱动力越来越多地来自数学家们自身.此外, 许多与电路设计正确性相关的验证都需要纯数学定理和数学算法的支持, 数学的机械化证明是非常有意义的研究领域[118]. Isabelle的开发者Paulson正在剑桥大学致力于数学的形式化, 当前, 他正主持一个形式化数学的大型项目Alexandria[119], 它以Isabelle/HOL为基础, 目标是得到一个覆盖所有大学水平数学的形式化数学库.国内施智平等人在数学形式化领域也做出了比较有影响力的工作, 他们在HOL-light中建立了几何代数系统的形式化模型, 在共形几何代数空间中, 给刚体运动问题提供了一种简单、有效的形式化建模与验证方法[120, 121].

3.2 编译器验证

编译器是将高级语言编写的程序转换到能在目标平台上运行指令集的重要系统软件.当前, 绝大多数编译器都没有经过形式化验证, 虽然在发布前已经进行了大量测试, 但仍存在许多问题.形式化验证编译器的研究随着第一个高级语言编译器的诞生就开始展开.但是, 表达和证明编译器正确的困难性, 以及不断发展的高级编程语言带来的语义和编译转换过程的复杂性使得这项研究历经几十年而经久不衰.随着关键技术和证明助手的成熟, 编译器验证领域涌现出了大量研究成果.这些成果可以分为“验证的编译器(verified compiler)”和“验证编译器(verifying compiler)”[122].验证的编译器是获得一个正确性得到验证的编译器, 而验证编译器并不获得这样一个编译器, 而是验证编译后的目标程序相对于源程序的正确性, 因此验证的是一次编译(compilation)是否正确.何炎祥等人深入研究了可信软件的构造理论和方法, 并在编译器验证领域开展了有意义的研究工作.为了表述方便, 以下按照何炎祥等人的研究[123], 将这两种验证方式分别称为编译器自身的正确性验证和编译后代码的正确性验证.

3.2.1 编译器自身的正确性验证

传统的编译器自身正确性验证的方法原理源自莫里斯(Morris F. L.), 如图 9所示:定义源语言和目标语言的语义, 定义源语言到目标语言的编译, 构造语义等同(homomorphism)定理, 最后采用归纳对定理进行证明[124].在实际应用中, 源语言和目标语言的语义定义方式大多采用了操作语义或者指称语义, 并且需要构造许多辅助定理才能完成一个真实语言编译器的语义等同定理的证明.

Fig. 9 Semantics homomorphism diagram 图 9 语义等同示意图

伴随编程语言语义的不断发展进化, 表 3列举了部分具有代表性或者影响力的编译器自身正确性验证的研究成果.

Table 3 Lists of achievements of verified compiler 表 3 编译器自身正确性的机器验证研究成果列表

编译器的机器验证最开始针对的是实验性质的语言.20世纪80年代, 两个比较大型的编译器验证分别使用Stanford Verifier和Boyer-Moore定理证明工具完成.前者的源语言类似Pascal, 目标机器类似B6700, 源语言和目标机器指令的指称语义之间的等同性表示为断言(assertions)语言, 这些断言转换为验证条件, 再由Stanford Verifier进行证明[125].后者的源语言是类似Pascal语言的Micro-Gypsy, 目标语言是高级汇编语言Piton, 语义采用操作的方式进行定义, 使用结构化归纳完成证明[126].Moore进一步完成了从Piton汇编语言到寄存器传输级(RTL)的正确性验证[127].

到20世纪90年代, 更多的证明助手被开发出来.使用HOL, Curzon基于指称语义证明了一个结构化的汇编语言Vista到目标Viper微处理器的编译[128].同样基于指称语义, Calvert使用PVS, 对Stepney给出的一个学习案例进行了实现[129], 该案例的源语言Tosca是一个小但并不简单的高级语言, 目标语言是典型的汇编语言.

到20世纪末和21世纪初, 证明助手已渐趋成熟, 联合结构化操作语义和自然语义的出现, 这些为实际编程语言编译器的验证创造了良好条件.最具代表性的两个项目是使用Coq的C编译器CompCert, 以及使用Isabelle/HOL的Java编译器Jinja和JinjaThread, 下面分别予以阐述.

(1) C优化编译器CompCert

始于2005年, Leroy等人使用Coq定义了C语言子集(Clight)的大步操作语义, 经过多遍翻译变换, 完成了从Clight到PowerPC汇编码的验证, 如图 10所示.CompCert对编译优化也进行了验证, 形式化了静态单赋值的语义, 并验证了基于SSA的全局值计数(global value numbering, 简称GVN)算法.

Fig. 10 Compilation passes and intermediate languages of CompCert 图 10 CompCert多遍编译和中间语言

严格上讲, 为了对优化算法进行验证, CompCert结合了编译后代码验证, 并辅以手工证明:编译器在编译转换的同时, 也生成安全性规范.对于编译器的每遍翻译, 证明翻译前后的语义等同; 或暂不证明而延迟到后续的某遍翻译中去验证翻译后的程序是否满足安全性规范, 并以注解的形式表示在翻译结果中; 最后对这些注解的一致性进行验证.国内王生原编译器研究组采用Coq实现了一个可信编译器L2C, L2C将同步数据流语言Lustre编译到了Clight, 他们对L2C的核心翻译步骤及其设计与实现进行了论述[130, 131].

建立在CompCert2.0基础之上, Beringer等人证明了在共享内存交互情况下的编译优化[132].Jaroslav等人形式化了一个支持共享内存的并发算法, 并证明了编译这类并发程序的正确性[133].目前, CompCert已成功应用于工业开发中, 它是迄今为止最为成功的C语言验证编译器.

(2) Java编译器Jinja和JinjaThread

Java编译器因其面向对象特性以及内建多线程机制而使得验证更为复杂.Nipkow和Oheimb首先于1998年使用Isabelle/HOL对Java子集进行了形式定义, 并证明了它的类型安全性[134].2002年, Klein对Java虚拟机(Java virtual machine, 简称JVM)字节码验证器的正确性进行了机器验证[135].在这些基础之上, 2006年, Klein和Tobias构建了包括Java、JVM目标机器以及编译器等在内的统一模型, 证明了Java编译到JVM虚拟机的正确性[136], 为Java这样的OO语言编译器验证奠定了良好的研究基础.Jinja源码共涉及1 000多个定理的证明, 所有定义和定理证明包括在BV、Common、Compiler、DFA、J、JVM这6个理论文件夹中, 构成语义等同框架的核心理论如图 11所示(包括类型安全).

Fig. 11 Core theories of semantics homomorphism of Jinja (including type safety) 图 11 Jinja语义等同框架(包括类型安全)的核心理论

建立在Jinja基础之上, Lochbihler设计了一个能够定义线程的语义框架JinjaThread, 如图 12所示, 将Java内存模型(Java memory model, 简称JMM)规范与运行时操作语义联合在一起进行分析, 机器证明了交错语义和JMM的类型安全、DRF(data race free)保证, 分析了值凭空出现的问题等, 并将编译器的正确性验证扩展到了支持线程, 具有良好的模块性[137, 138].何炎祥和江南等人以Jinja为基础, 研究了Java语言子集编译到Android Dalvik虚拟机字节码的机器验证[139, 140].在他们的形式化中, 用新的Dalvik VM理论文件夹取代了JVM.由于寄存器架构的Dalvik虚拟机不同于栈架构的Java虚拟机, 大量规范描述需要重新定义, 并构造和证明新的定理, 这些修改主要包含在Common、Compiler和BV中.

Fig. 12 Semantics stack of JinjaThreads with JMM 图 12 带有内存模型的JinjaThreads语义栈

除了传统的语义等同原理方法外, 编译器自身验证的另外一种方法是采用如第1.5节所述的“构造即正确”的方法:定义程序转换规则, 源语言程序按照转换规则被逐步求精到可执行的目标语言程序.转换规则是编译器行为, 规则的可靠性保证编译的正确性.20世纪90年代初期开始的欧洲项目ProCos(provably correct systems)采用了类似方法[141, 142].ProCos项目旨在建立所有开发阶段的正确性, 并包括显式并行和时间约束条件.其中, Buth和Buth等人研究了Occam顺序子集编译到Transputer机器语言的正确性验证[143], 何积丰和Ian等人研究了将Occam子集编译到适合用于现场可编程门阵列(field-programmable gate array, 简称FPGA)硬件的范式(normal form)[144].此外, 作为ProCos项目的一部分, 周巢尘提出了规范和验证实时系统的时段演算(duration calculus)[145], 这项研究获得国际同行的重视[146], 并进一步对时段演算的可判定性和不可判定性进行了研究[147], 在机械化自动证明研究方面取得了很大进展.

在ProCos项目研究的大环境下, Sampaio使用项重写term rewriting系统OBJ3[148], 针对编译器验证的代数方法进行了研究[149], 他的工作建立在Back[76]和Morris[150]的基础之上.Sampaio深入研究了范式方法[151]:范式代表着不可继续归约(reduction)的目标代码, 编译视为一种程序求精, 是程序到范式的归约; 归约包括一系列语义等同的转换, 语义等同的中心概念是程序的排序关系(ordering relation); 代表着代数语义的转换法则用来证明归约定理, 证明了归约定理可以作为重写规则执行编译任务, 自动地完成编译, 也保证了编译转换的语义等同.与Sampaio的方法一致, Duran等人针对类似Java的面向对象语言的编译器进行了正确性构造[152], 但是没有进行机器检测.