重写对策在基于HOL的形式化证明中的应用

张 杰，毛丹雯，关 永，施智平

（1.北京化工大学 信息科学与技术学院，北京100029；2.首都师范大学 信息工程学院，北京100048）

0 引 言

交互式高阶逻辑定理证明系统HOL是由英国剑桥大学开发的一种基于定理证明方法的形式化验证系统，其最新的版本为HOL4。形式化验证是在二十世纪60年代末出现的一种用于系统设计正确性检验的方法，而定理证明方法是形式化验证的传统三种方法之一，近年来在计算机网络协议、安全协议等各类协议，各种硬件电路，以及Viper微处理器、DSP处理器等硬件系统的分析与验证中取得了较为广泛的应用［1－6］。

在定理证明系统中进行形式化验证离不开对定理的形式化证明。HOL4系统中最常用的形式化证明方法是目标制导法，这种方法在使用时很大程度上依赖于一种叫做对策的证明工具的应用，而重写对策是HOL4系统所有对策中极为重要的一类对策。为了更好地在HOL4系统中完成定理的形式化证明，本文对重写对策在基于HOL4系统的形式化证明过程中的应用进行了重点讨论，并以几个典型的重写对策为例，进一步说明如何在HOL4系统中利用重写对策实现证明目标的化简与证明。

1 形式化证明与对策

HOL4系统中定理的形式化证明的实现方法是用户在高层次做引导，而将推理的过程交给系统自动完成［7］。在定理证明系统发展的初期，定理的形式化证明方法为正向证明法。这种方法从欲证定理的假设条件出发，利用系统中的公理、定理和推理规则等逐步推导出欲证定理；然而对于一些复杂的问题，正向证明法并不能快速有效地完成证明。直到二十世纪70年代早期，开发定理证明系统的鼻祖之一，英国计算机科学家Robin Milner发明了对策，才产生了一种新的形式化证明方法－－目标制导证明法［8］。该方法首先假设欲证定理为真，并将其作为初始目标，再通过使用对策引导系统根据已知条件、公理、定义和定理产生简化的子目标，通过反复使用对策对子目标进行不断地化简，直到当前子目标可以利用某个对策直接证明为止。因为目标制导法的本质是通过证明各个简化的子目标而使初始目标得到证明，所以也称为反向证明法。不难看出，对策在目标证明过程中起了重要作用。而对策其实就是HOL4系统中已编写好的ML函数，用于简化证明目标，它主要完成两项工作：一是将待证明目标化简为子目标；二是保证上述转换的正确性，即证明了子目标，就证明了初始目标。由此可知，采用目标制导法进行形式化证明的关键问题是采用合理的、恰当的对策完成待证明目标的化简。

在基于高阶逻辑的交互式定理证明系统HOL4中，针对不同形式的证明目标常用的对策有：GEN＿TAC，EXISTS＿TAC，CONJ＿TAC，DISCH＿TAC，REWRITE＿TAC，RW＿TAC等等。其中，GEN＿TAC用于消去证明目标最外层的全称量词；EXISTS＿TAC用于将证明目标中存在量化的变量实例化，从而消去该变量前的存在量词；CONJ＿TAC用于将一个形式为合取式”t1∧t2”的证明目标分解成两个简化的子目标”t1”与”t2”；DISCH＿TAC用于将证明目标中的蕴含式的前件泄放到假设条件列表中去；REWRITE＿TAC和RW＿TAC均为重写对策，用于完成证明目标的重写［9，10］。

之所以说重写对策是HOL4系统的所有对策中极为重要的一类是因为在HOL4系统中目标制导证明法的核心思想就是利用已知条件和系统中已有的公理、定义、定理等完成证明目标的化简与证明，而重写对策的使用则是实现化简的关键步骤。接下来，本文就重写对策在形式化证明中的应用进行讨论。

2 重写对策在形式化证明中的应用

HOL4系统为用户提供了许多种重写对策，比如REWRITE＿TAC、ASM＿REWRITE＿TAC、RW ＿TAC、ONCE＿REWRITE＿TAC、PURE＿REWRITE＿TAC、GEN＿REWRITE＿TAC等。这些对策之所以统称为重写对策是因为它们在应用过程中具有一个共同的特点－－可以利用对策中指定的定理重写证明目标，即利用HOL4系统中已有的公理、定义和定理作为重写对策 （一个ML函数）的参数，并对证明目标施加该对策，系统则会自动将证明目标中的表达式与指定定理中的等式进行匹配，若发现表达式与等式左边式子的模式相同，则用等式右边的式子替换该表达式，从而达到对证明目标的化简或证明作用。

作者在长期的实践中发现，利用重写对策对不同的证明目标进行化简或证明有两个关键所在：一是如何在HOL4系统提供的众多重写对策中选择恰当的对策，并正确使用；二是如何在HOL4系统提供的定理库中找到使用重写对策所需的定理，以达到预期的化简或证明效果。因此，为了有效地使用重写对策，下面围绕3个典型的重写对策进行详细的分析和描述，并给出它们在应用过程中可能出现的问题和解决办法，以点概面说明重写对策的一般使用原则和注意事项。

2.1 几个典型的重写对策

（1）REWRITE＿TAC对策

REWRITE＿TAC是最基本的一种重写对策，其类型为thm list－＞tactic［9，10］，所以在应用该对策时要提供一个定理表作为参数，该定理表中应包含重写所需的公理、定义及定理，系统将根据这些给定的定理反复不断地对证明目标进行重写。

通常情况下，对于一个既定的证明目标，若有一个预期的化简目标，且已找到了实现该化简目标的定理，则可以通过使用REWRITE＿TAC对证明目标进行重写。

例如：现有一个证明目标：“a＞b”，预期的化简目标为”b＜a”，且HOL4系统中的已有定理”GREATER＿DEF：｜－m n.m＞n＝n＜m”能够实现该化简目标。在这种情况下，就可采用REWRITE＿TAC对该证明目标进行重写，具体实现过程如下：

由此可见，使用REWRITE＿TAC对证明目标进行重写，系统能根据指定的公理、定义、定理等实现对证明目标预期的特定的化简。

然而，REWRITE＿TAC并不适用于所有情况，在特殊情况下应用HOL4系统可能会抛出异常，例如：

在上例中，对于一个证明目标”c＋a－c＝a”，欲利用定理”ADD＿SYM：｜－m n.m＋n＝n＋m”将证明目标中的”c＋a”重写为”a＋c”，但由于REWRITE＿TAC对策会根据给定的定理反复进行重写，这样会不断地将”c＋a”重写为”a＋c”，再重写为”c＋a”……如此反复循环，从而导致了HOL4系统出现异常：内存不足 （如代码框中所示）。这是REWRITE＿TAC应用的一个缺陷，HOL4系统的初学者往往会忽略这个问题。此时用户可考虑使用系统中的另一个重写对策ONCE＿REWRITE＿TAC，这里不再做详细介绍。

（2）ASM＿REWRITE＿TAC对策

与REWRITE＿TAC一样，ASM＿REWRITE＿TAC的类型也为thm list－＞tactic［9，10］，因此在应用该重写对策时也需要提供一个定理表作为参数，系统可以根据给定的定理反复不断地对证明目标进行重写。但是，ASM＿RE－WRITE＿TAC在REWRITE＿TAC的基础上增加了一个功能，即不仅能根据给定的定理，而且可以根据证明目标的假设条件表，反复不断地对证明目标进行重写。

通常情况下，对于一个含有假设条件表的证明目标，若有一个预期的化简目标，且实现这一预期的化简目标需要使用证明目标的这些假设条件，则可应用ASM＿REWRITE＿TAC对证明目标进行重写。

例如：初始证明目标为：“对任意的两个自然数a与b，若b为0，则a＋b＝a”。系统要想对其进行形式化证明，则必须能证明”a＋0＝a”，而 HOL4系统中已存在定理”ADD＿0：｜－m.m＋0＝m”，所以可以考虑采用重写对策进行重写。但是由于该证明的实现依赖于证明目标的假设条件”b＝0”，因此如果仅仅使用最基本的重写对策REWRITE＿TAC是不能完成预期的证明的。如下所示，施加REWRITE＿TAC对策后证明目标没有变化。

在这种情况下可以考虑采用对策ASM＿REWRITE＿TAC对目标进行重写，具体实现过程如下：

由此可知，应用ASM＿REWRITE＿TAC能根据证明目标的假设条件表及指定的公理、定义、定理等达到对证明目标的预期的化简或证明目的。

然而，ASM＿REWRITE＿TAC的应用也有缺陷。与REWRITE＿TAC类似，在一些特殊情况下，应用ASM＿REWRITE＿TAC会对证明目标进行反复重写而使HOL4系统抛出异常。初学者若对该对策理解不深入，在应用时就会发生这样的问题，此时可考虑使用系统中的另一个重写对策ONCE＿ASM＿REWRITE＿TAC。

（3）RW＿TAC对策

RW＿TAC是一种功能更加强大的重写对策，其类型为simpset－＞thm list－＞tactic［9，10］，因此在应用该对策时不仅要提供一个定理表作为参数，同时还要给出一个化简集作为参数。化简集是一个特定的集合，其中包含了一些特定领域的重写定理。例如化简集bool＿ss中包含了一些与布尔逻辑相关的定理，如｜－A B. （AB）＝ A∧ B；化简集arith＿ss则是在bool＿ss的基础上又添加了一些与自然数运算相关的定理，如｜－m n.（m＊n＝0）＝ （m＝0）∨ （n＝0）；而化简集list＿ss是在arith＿ss的基础上又增添了一些与表相关的定理，如｜－（LENGTH ［］＝0）∧ h t.LENGTH （h：：t）＝ SUC（LENGTH t）。应用RW＿TAC的最大优势就是 HOL4系统可以根据指定的化简集和给定的公理、定义、定理等对证明目标及假设条件表进行重写，且能自动处理证明目标结论中的全称量词、合取符、析取符、蕴含符，甚至是假设条件表中的存在量词等等，另外该对策还具备自动执行案例分解、决策程序等更加高级的功能。

通常情况下，由于RW＿TAC功能强大，利用它可以快速完成许多证明目标的化简或证明工作。特别是对于一个比较复杂的证明目标，假如用户不能确定一个预期的化简目标，更不清楚应该使用HOL4系统中的哪些定理来化简证明目标，这时可以先根据该证明目标的具体情况选取相关领域的化简集，在定理表为空的情况下应用RW＿TAC对证明目标进行重写，此时可能会产生一些意想不到的化简效果，还将有助于打开用户的证明思路。

例如：对于上述的证明目标 “对任意的两个自然数a与b，若b为0，则a＋b＝0”，假设用户由于经验不足等问题不能确定一个预期的化简目标，且不清楚应该利用HOL4系统中的哪些定理来化简，则用户可通过待证明目标的背景确定该目标与自然数的运算有关，因此可尝试选取化简集arith＿ss作为参数，应用RW＿TAC对证明目标进行重写，结果发现系统不但完成了重写，而且还自动地完成了证明目标的证明，一步到位。具体实现过程如下所示：

由此可见，RW＿TAC确实是一种非常强大的重写对策，它不仅包含了前两种重写对策的功能，而且可以将化简进行得十分彻底，进一步提高形式化证明的效率。

然而，RW＿TAC对策尽管强大，其应用也存在着缺陷。比如说，有时会因为证明目标被过于彻底地化简而越过了某些中间结果，这反而可能不利于后续的形式化证明。这时可以考虑使用REWRITE＿TAC等一般的重写对策，根据给定的定理得到特定的化简效果。

综上所述，在HOL4系统中实施形式化证明时，应针对不同的证明目标，根据不同重写对策的功能、应用方法、应用环境和应用中可能出现的问题等恰当地选用重写对策，这样才能提高形式化证明的有效性，并缩短形式化证明的时间。

2.2 重写对策的定理参数的选择

在HOL4系统提供的庞大定理库中选择合适的重写定理作为参数是利用重写对策对证明目标进行化简或形式化证明的另一个关键点。作者通过对HOL4系统的研究与使用对定理的搜索过程进行了探索，得出如下一些方法。

方法1：在HOL4系统中采用函数DB.match搜索所需定理。这种方法的优点在于可按照所需定理的模式，在指定的理论中进行搜索，从而缩小了搜索定理的范围，提高了搜索效率。然而，采用这种方法的一个前提是必须能够总结出所需定理的模式，且必须指定搜索的范围，这也是本方法的局限性所在。

方法2：在HOL4系统中采用函数DB.find搜索所需定理。使用该方法可利用所需定理名字中的关键字，在当前系统加载的所有理论中搜索名字中包含这些关键字的定理，而无需给出特定的搜索范围，这是其优势所在。但是这种方法也具有明显的缺点，即系统当前未加载的理论不会纳入搜索的范围，这可能会降低搜索的有效性；且搜索出来的数据量一般比较大，需要逐个研究，找出有用的定理，这无疑会降低搜索的效率。

方法3：利用所需定理的名字或内容中的关键字在HOL4官网所提供的定理库中进行搜索。这种方法没有什么明显的优点，在前两种方法失败后，再使用该方法。这是因为定理库包含了所有理论中的定理，搜索出来的数据量会更大，找出所需的定理将更加困难。

方法4：打开所有可能的理论，逐个查看，搜寻所需定理。这种方法是所有方法中最不方便，效率最低的，因而尽量在尝试了前3种方法后再考虑之。

针对证明目标的实际情况选择恰当的搜索定理的方法将有助于快速有效地找到重写所需的定理，从而保证重写对策的顺利应用，达到对证明目标的化简或证明效果。

3 结束语

在HOL4系统中快速有效地进行形式化证明依赖于对系统提供的数百个对策及几千个定理的熟悉与了解，对普通用户而言全部了解显然不太现实，但是深入细致地了解像重写对策这样重要对策的功能、应用方法、应用环境及应用中可能出现的问题还是十分必要的。本文对重写对策在基于HOL4系统的形式化证明过程中的应用进行了分析与阐述，以期对HOL4系统用户，特别是初学者提供一些帮助与启发。此外，当用户对HOL4系统已有对策了解得十分透彻并熟练使用之后，用户也可以尝试着自行定义对策，以满足各自的特殊需求，这也将会促进HOL4系统的进一步发展与完善，从而可以支持更多的形式化问题的解决。

［1］Hasan O.Formal probabilistic analysis using theorem proving［D］.Montreal Quebec Canada：Concordia University，2008.

［2］Hasan O，Tahar S.Performance analysis and functional verification of the stop－and－wait protocol in HOL ［J］.Berlin：Journal of Automated Reasoning，2009，42 （1）：1－33.

［3］Basin D，Capkun S，Schaller P，et al.Formal reasoning about physical properties of security protocols ［J］.USA：ACM Transactions on Information and System Security，2011，14（2）：1－16.

［4］Hasan O，Patel J，Tahar S.Formal reliability analysis of combinational circuits using theorem proving ［J］.Journal of Applied Logic，2011，9 （1）：41－60.

［5］Habibi A，Tahar S，Ghazel A.Formal verificaction of the ADSP－2100processor using the HOL theorem prover ［EB／OL］.［2013－01－30］.http：／／users.encs.concordia.ca／～tahar／pub／DSP＿TR02.pdf.

［6］Abdullah A N M，Akbarpour B，Tahar S.Error analysis and verification of an IEEE 802.11OFDM modem using theorem proving ［J］.Electronic Notes in Theoretical Computer Science，2009，242 （2）：3－30.

［7］Slind K，Norrish M.A brief overview of HOL4 ［G］.LNCS 5170：Berlin Heidelberg：Springer－Verlag，2008：28－32.

［8］Cambridge research center of SRI International.The HOL System TUTORIAL（For HOL Kananaskis－7）［EB／OL］.［2013－01－30］.http：／／cdnetworks－kr－1.dl.sourceforge.net／project／hol／hol／kananaskis－7／kananaskis－7－tutorial.Pdf.

［9］Cambridge Research Center of SRI International.The HOL System Reference（For HOL Kananaskis－7）［EB／OL］.［2013－01－30］.http：／／cdnetworks－kr－1.dl.sourceforge.net／project／hol／hol／kananaskis－7／kananaskis－7－reference.Pdf.

［10］HOL reference page ［EB／OL］.［2013－01－30］.http：／／hol.Sourceforge.net／kananaskis－7－helpdocs／help／HOLindex.html.