高阶逻辑验证系统HOL及其应用初探

陈波

【摘 要】形式化方法在硬件、软件的设计和验证中的应用越来越广泛，基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍，并结合例子说明HOL系统在硬件设计中的应用。

【关键词】形式化验证方法；HOL逻辑；HOL系统；带复位的奇偶校验器

中图分类号： TP316；TP309 文献标识码： A 文章编号： 2095-2457（2018）28-0162-002

DOI：10.19694/j.cnki.issn2095-2457.2018.28.074

【Abstract】Formal method has been used in both practical hardware and software design and verification widely， formal verification tools based on different theory emerge as the times require.The paper discusses the higher order logic theory prover HOL and illustrates specification and verification in hardware design.

【Key words】Formal Verification method；HOL logic；HOL system；Parity-reset checking device

0 引言

随着数字系统设计技术的发展，传统的模拟验证方法已不能满足需求，形式化验证方法逐渐应用到数字系统的验证中。一般来说，形式化验证方法可分为模型检测、定理证明和等价性验证等三类[1]。HOL系统是基于高阶逻辑的定理证明器，它即能进行软件验证，又能进行硬件的形式化验证，是目前形式化领域的研究的热点之一[2-3]。本文对HOL逻辑及HOL验证系统之间的关系进行分析研究，并给出HOL系统在硬件设计验证中的一个应用实例。

1 HOL系统

HOL系统是英国剑桥大学的M.J.C.Gordon教授在80年代开发的高阶逻辑（HOL）定理证明系统[3]，该系统的基础是Church的简单带类型演算，演算是由Alonzo Church提出的作为数学基础的函数理论。带类型 演算是用来表示函数的另一种方式，是函数语言的基础，类型的引入保障了逻辑系统的健康性。HOL系统包含了函数式语言ML，它既是HOL系统的开发语言也是它的实现语言。函数式语言采用一种基于递归表示的函数定义的计算模型[4]。

1.1 HOL逻辑

HOL逻辑是对谓词演算进行了三项扩展[5]：

变量可以为函数和谓词。

逻辑是有类型的。

没有公式的单独语法类（类为bool的项为公式）。

由于HOL逻辑系统中的最基本的常量T都是用λ表达式T=（（λx.x）=（λx.x））进行定义的，所以λ演算是HOL逻辑的基础。HOL逻辑是HOL验证系统的逻辑基础，为了避免不一致性HOL逻辑是有类型的，通常有4种类型：

σ：：=α|c|（σ1，…，σn）op|σ1→σ2，

其中σ表示变量，c表示原子类型，op表示类型操作符。

在HOL逻辑中出现的任何合法的符号都是项，项也有4种。

M：：=c|v|（MN）|λv.M

其中c表示常量，v表示变量，M和N表示项。

1.2 HOL逻辑在HOL定理证明系统中的表示

HOL定理证明系统的项是用ML的抽象数据类型表示的。抽象数据类型就是带有其特有的一组运算的数据类型。在HOL系统中，项的前后加上引号，系统在进行词法检查时就认为是逻辑项。HOL系统的项的类型构成了一种叫做type的ML类型。HOL的逻辑类型是目标语言的类型，而ML类型是元语言类型。

1.3 HOL定理证明系统的理论

在HOL系统中，一个理论（theory）包含一组类型、常元、定义、公理和定理等。关于理论的工具能够维护不同的理论之间的关系，例如增加、结合、扩展和保存理论。每个理论记录了某些类型、常数、公理、定义和定理，同时具有指向它的上级理论的指针。所有的理论构成了一个分层的树形结构。最基本的理论是min，它定义了最基本的类型和常量符号。在这基础上，逐步构成各种数据类型和经过证明的定理，并为以后更高层的理论及相关定理的证明所使用，现在HOL系统的理论库已经非常庞大。

1.4 用HOL定理证明系统证明定理

要证明一个定理，实际上就是要找出一个公理或定理序列，由序列中前面的元素（公理或已经证明的定理）利用推理规则可以得到其后面的元素，最后得到的就是要證明的定理。文献[3]中给出了HOL系统内核中五个公理和八条推理规则，见表1。

HOL支持两种证明方式：正向证明方式：指从定理的假设条件和公理、定理、定义出发推导出结论的过程。目标制导方式：指从要证明的目标出发，即假定结论正确，利用已知条件和公理、定理、定义等推出需要证明的子目标；如果证明了各个子目标，原来的目标也就证明了。在实际应用中经常正向证明和目标制导方法结合起来使用。

2 HOL定理证明系统的应用

HOL系统现在已经应用在工业和学术上进行形式化推理的很多领域：硬件的设计与验证、安全性的推理、实时系统的证明、硬件描述语言的语义、编译器的验证、程序正确性的证明、并发模型及程序细化等方面。结合例子说明。

2.1 验证步骤

在用HOL系统对系统进行验证时，一般有以下四个步骤：

建立系统行为的形式化规范（SPEC）。

建立系统实现的形式化描述（IMP），包括子模块的行为规范及各子模块间连接的结构描述。

用公式形式描述证明目标，或者。

运用推理规则对目标进行形式化验证。

在应用时往往要先对系统用结构抽象、行为抽象、数据抽象、时态抽象等抽象技术进行处理，去掉不必要的细节，建立规范和实现的形式化描述。

2.2 实例

下面通过例子进行说明，带复位的奇偶校验器的设计与验证：主要包括一个能计算输入序列中1的奇偶性的设备的规范说明和验证，此设备包括一个输入 in， 一个复位reset和一个输出键out.，从上一次进行复位开始，当且仅当输入二进制序列中1的个数为偶数个时，输出为真，否则为假。

规范说明：

val PARITY_RESET_SPEC =

|- （！f reset. PARITY_RESET_SPEC 0 f reset = T） /＼

！n f reset.

PARITY_RESET_SPEC （SUC n） f reset =

（if reset （SUC n） then

T

else

（if f （SUC n） then

～PARITY_RESET_SPEC n f reset

else

PARITY_RESET_SPEC n f reset）） ： thm

根据说明设计出电路并进行形式化描述：

val PARITY_RESET_IMP =

|- ！inp reset out.

PARITY_RESET_IMP （inp，reset，out） =

？l1 l2 l3 l4 l5 l6.

NOT （l2，l1） /＼ MUX （inp，l1，l2，l3） /＼ REG （out，l2） /＼ ONE l4 /＼

REG （l4，l5） /＼ MUX （reset，l4，l3，l6） /＼ MUX （l5，l6，l4，out） ： thm

建立目标及对目标进行推理证明（其中引理UNIQUENESS_LEMMA，PARITY_RESET_LEMMA已得以证明）：

3 結束语

高阶逻辑验证系统HOL在验证过程中用到了各种相关的技术，特别是推理技术和抽象技术，对使用者的要求较高。以后的研究将注重HOL系统理论库的扩充以及与其它形式化技术的结合，特别是模型检测技术，以使其在更多的领域中得到应用。

【参考文献】

[1]Rolf Drechsler.Advanced Formal Verification[M].Dordrecht：Kluwer Academic Publishers，2004.1-20.

[2]韩俊刚，杜慧敏. 数字硬件的形式化验证[M].北京大学出版社.2001.12.

[3]M.J.C.Gordon and T.F.Melham.Introduction to HOL：A Theorem Proving Environment for Higher-order Logic[M]. Cambridge University Press，1993.

[4]Lawrence C.Paulson著，柯韦译.ML程序设计教程（第二版）[M].北京：机械工业出版社.2005.

[5]The HOL System Logic，2018，https：//hol-theorem-prover.org/.