重寫對策在基于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.