張 杰，毛丹雯，關(guān) 永，施智平

（1.北京化工大學(xué) 信息科學(xué)與技術(shù)學(xué)院，北京100029；2.首都師范大學(xué) 信息工程學(xué)院，北京100048）

0 引 言

交互式高階邏輯定理證明系統(tǒng)HOL是由英國劍橋大學(xué)開發(fā)的一種基于定理證明方法的形式化驗證系統(tǒng)，其最新的版本為HOL4。形式化驗證是在二十世紀(jì)60年代末出現(xiàn)的一種用于系統(tǒng)設(shè)計正確性檢驗的方法，而定理證明方法是形式化驗證的傳統(tǒng)三種方法之一，近年來在計算機網(wǎng)絡(luò)協(xié)議、安全協(xié)議等各類協(xié)議，各種硬件電路，以及Viper微處理器、DSP處理器等硬件系統(tǒng)的分析與驗證中取得了較為廣泛的應(yīng)用［1－6］。

在定理證明系統(tǒng)中進(jìn)行形式化驗證離不開對定理的形式化證明。HOL4系統(tǒng)中最常用的形式化證明方法是目標(biāo)制導(dǎo)法，這種方法在使用時很大程度上依賴于一種叫做對策的證明工具的應(yīng)用，而重寫對策是HOL4系統(tǒng)所有對策中極為重要的一類對策。為了更好地在HOL4系統(tǒng)中完成定理的形式化證明，本文對重寫對策在基于HOL4系統(tǒng)的形式化證明過程中的應(yīng)用進(jìn)行了重點討論，并以幾個典型的重寫對策為例，進(jìn)一步說明如何在HOL4系統(tǒng)中利用重寫對策實現(xiàn)證明目標(biāo)的化簡與證明。

1 形式化證明與對策

HOL4系統(tǒng)中定理的形式化證明的實現(xiàn)方法是用戶在高層次做引導(dǎo)，而將推理的過程交給系統(tǒng)自動完成［7］。在定理證明系統(tǒng)發(fā)展的初期，定理的形式化證明方法為正向證明法。這種方法從欲證定理的假設(shè)條件出發(fā)，利用系統(tǒng)中的公理、定理和推理規(guī)則等逐步推導(dǎo)出欲證定理；然而對于一些復(fù)雜的問題，正向證明法并不能快速有效地完成證明。直到二十世紀(jì)70年代早期，開發(fā)定理證明系統(tǒng)的鼻祖之一，英國計算機科學(xué)家Robin Milner發(fā)明了對策，才產(chǎn)生了一種新的形式化證明方法－－目標(biāo)制導(dǎo)證明法［8］。該方法首先假設(shè)欲證定理為真，并將其作為初始目標(biāo)，再通過使用對策引導(dǎo)系統(tǒng)根據(jù)已知條件、公理、定義和定理產(chǎn)生簡化的子目標(biāo)，通過反復(fù)使用對策對子目標(biāo)進(jìn)行不斷地化簡，直到當(dāng)前子目標(biāo)可以利用某個對策直接證明為止。因為目標(biāo)制導(dǎo)法的本質(zhì)是通過證明各個簡化的子目標(biāo)而使初始目標(biāo)得到證明，所以也稱為反向證明法。不難看出，對策在目標(biāo)證明過程中起了重要作用。而對策其實就是HOL4系統(tǒng)中已編寫好的ML函數(shù)，用于簡化證明目標(biāo)，它主要完成兩項工作：一是將待證明目標(biāo)化簡為子目標(biāo)；二是保證上述轉(zhuǎn)換的正確性，即證明了子目標(biāo)，就證明了初始目標(biāo)。由此可知，采用目標(biāo)制導(dǎo)法進(jìn)行形式化證明的關(guān)鍵問題是采用合理的、恰當(dāng)?shù)膶Σ咄瓿纱C明目標(biāo)的化簡。

在基于高階邏輯的交互式定理證明系統(tǒng)HOL4中，針對不同形式的證明目標(biāo)常用的對策有：GEN＿TAC，EXISTS＿TAC，CONJ＿TAC，DISCH＿TAC，REWRITE＿TAC，RW＿TAC等等。其中，GEN＿TAC用于消去證明目標(biāo)最外層的全稱量詞；EXISTS＿TAC用于將證明目標(biāo)中存在量化的變量實例化，從而消去該變量前的存在量詞；CONJ＿TAC用于將一個形式為合取式”t1∧t2”的證明目標(biāo)分解成兩個簡化的子目標(biāo)”t1”與”t2”；DISCH＿TAC用于將證明目標(biāo)中的蘊含式的前件泄放到假設(shè)條件列表中去；REWRITE＿TAC和RW＿TAC均為重寫對策，用于完成證明目標(biāo)的重寫［9，10］。

之所以說重寫對策是HOL4系統(tǒng)的所有對策中極為重要的一類是因為在HOL4系統(tǒng)中目標(biāo)制導(dǎo)證明法的核心思想就是利用已知條件和系統(tǒng)中已有的公理、定義、定理等完成證明目標(biāo)的化簡與證明，而重寫對策的使用則是實現(xiàn)化簡的關(guān)鍵步驟。接下來，本文就重寫對策在形式化證明中的應(yīng)用進(jìn)行討論。

2 重寫對策在形式化證明中的應(yīng)用

HOL4系統(tǒng)為用戶提供了許多種重寫對策，比如REWRITE＿TAC、ASM＿REWRITE＿TAC、RW ＿TAC、ONCE＿REWRITE＿TAC、PURE＿REWRITE＿TAC、GEN＿REWRITE＿TAC等。這些對策之所以統(tǒng)稱為重寫對策是因為它們在應(yīng)用過程中具有一個共同的特點－－可以利用對策中指定的定理重寫證明目標(biāo)，即利用HOL4系統(tǒng)中已有的公理、定義和定理作為重寫對策 （一個ML函數(shù)）的參數(shù)，并對證明目標(biāo)施加該對策，系統(tǒng)則會自動將證明目標(biāo)中的表達(dá)式與指定定理中的等式進(jìn)行匹配，若發(fā)現(xiàn)表達(dá)式與等式左邊式子的模式相同，則用等式右邊的式子替換該表達(dá)式，從而達(dá)到對證明目標(biāo)的化簡或證明作用。

作者在長期的實踐中發(fā)現(xiàn)，利用重寫對策對不同的證明目標(biāo)進(jìn)行化簡或證明有兩個關(guān)鍵所在：一是如何在HOL4系統(tǒng)提供的眾多重寫對策中選擇恰當(dāng)?shù)膶Σ?，并正確使用；二是如何在HOL4系統(tǒng)提供的定理庫中找到使用重寫對策所需的定理，以達(dá)到預(yù)期的化簡或證明效果。因此，為了有效地使用重寫對策，下面圍繞3個典型的重寫對策進(jìn)行詳細(xì)的分析和描述，并給出它們在應(yīng)用過程中可能出現(xiàn)的問題和解決辦法，以點概面說明重寫對策的一般使用原則和注意事項。

2.1 幾個典型的重寫對策

（1）REWRITE＿TAC對策

REWRITE＿TAC是最基本的一種重寫對策，其類型為thm list－＞tactic［9，10］，所以在應(yīng)用該對策時要提供一個定理表作為參數(shù)，該定理表中應(yīng)包含重寫所需的公理、定義及定理，系統(tǒng)將根據(jù)這些給定的定理反復(fù)不斷地對證明目標(biāo)進(jìn)行重寫。

通常情況下，對于一個既定的證明目標(biāo)，若有一個預(yù)期的化簡目標(biāo)，且已找到了實現(xiàn)該化簡目標(biāo)的定理，則可以通過使用REWRITE＿TAC對證明目標(biāo)進(jìn)行重寫。

例如：現(xiàn)有一個證明目標(biāo)：“a＞b”，預(yù)期的化簡目標(biāo)為”b＜a”，且HOL4系統(tǒng)中的已有定理”GREATER＿DEF：｜－m n.m＞n＝n＜m”能夠?qū)崿F(xiàn)該化簡目標(biāo)。在這種情況下，就可采用REWRITE＿TAC對該證明目標(biāo)進(jìn)行重寫，具體實現(xiàn)過程如下：

由此可見，使用REWRITE＿TAC對證明目標(biāo)進(jìn)行重寫，系統(tǒng)能根據(jù)指定的公理、定義、定理等實現(xiàn)對證明目標(biāo)預(yù)期的特定的化簡。

然而，REWRITE＿TAC并不適用于所有情況，在特殊情況下應(yīng)用HOL4系統(tǒng)可能會拋出異常，例如：

在上例中，對于一個證明目標(biāo)”c＋a－c＝a”，欲利用定理”ADD＿SYM：｜－m n.m＋n＝n＋m”將證明目標(biāo)中的”c＋a”重寫為”a＋c”，但由于REWRITE＿TAC對策會根據(jù)給定的定理反復(fù)進(jìn)行重寫，這樣會不斷地將”c＋a”重寫為”a＋c”，再重寫為”c＋a”……如此反復(fù)循環(huán)，從而導(dǎo)致了HOL4系統(tǒng)出現(xiàn)異常：內(nèi)存不足 （如代碼框中所示）。這是REWRITE＿TAC應(yīng)用的一個缺陷，HOL4系統(tǒng)的初學(xué)者往往會忽略這個問題。此時用戶可考慮使用系統(tǒng)中的另一個重寫對策ONCE＿REWRITE＿TAC，這里不再做詳細(xì)介紹。

（2）ASM＿REWRITE＿TAC對策

與REWRITE＿TAC一樣，ASM＿REWRITE＿TAC的類型也為thm list－＞tactic［9，10］，因此在應(yīng)用該重寫對策時也需要提供一個定理表作為參數(shù)，系統(tǒng)可以根據(jù)給定的定理反復(fù)不斷地對證明目標(biāo)進(jìn)行重寫。但是，ASM＿RE－WRITE＿TAC在REWRITE＿TAC的基礎(chǔ)上增加了一個功能，即不僅能根據(jù)給定的定理，而且可以根據(jù)證明目標(biāo)的假設(shè)條件表，反復(fù)不斷地對證明目標(biāo)進(jìn)行重寫。

通常情況下，對于一個含有假設(shè)條件表的證明目標(biāo)，若有一個預(yù)期的化簡目標(biāo)，且實現(xiàn)這一預(yù)期的化簡目標(biāo)需要使用證明目標(biāo)的這些假設(shè)條件，則可應(yīng)用ASM＿REWRITE＿TAC對證明目標(biāo)進(jìn)行重寫。

例如：初始證明目標(biāo)為：“對任意的兩個自然數(shù)a與b，若b為0，則a＋b＝a”。系統(tǒng)要想對其進(jìn)行形式化證明，則必須能證明”a＋0＝a”，而 HOL4系統(tǒng)中已存在定理”ADD＿0：｜－m.m＋0＝m”，所以可以考慮采用重寫對策進(jìn)行重寫。但是由于該證明的實現(xiàn)依賴于證明目標(biāo)的假設(shè)條件”b＝0”，因此如果僅僅使用最基本的重寫對策REWRITE＿TAC是不能完成預(yù)期的證明的。如下所示，施加REWRITE＿TAC對策后證明目標(biāo)沒有變化。

在這種情況下可以考慮采用對策ASM＿REWRITE＿TAC對目標(biāo)進(jìn)行重寫，具體實現(xiàn)過程如下：

由此可知，應(yīng)用ASM＿REWRITE＿TAC能根據(jù)證明目標(biāo)的假設(shè)條件表及指定的公理、定義、定理等達(dá)到對證明目標(biāo)的預(yù)期的化簡或證明目的。

然而，ASM＿REWRITE＿TAC的應(yīng)用也有缺陷。與REWRITE＿TAC類似，在一些特殊情況下，應(yīng)用ASM＿REWRITE＿TAC會對證明目標(biāo)進(jìn)行反復(fù)重寫而使HOL4系統(tǒng)拋出異常。初學(xué)者若對該對策理解不深入，在應(yīng)用時就會發(fā)生這樣的問題，此時可考慮使用系統(tǒng)中的另一個重寫對策ONCE＿ASM＿REWRITE＿TAC。

（3）RW＿TAC對策

RW＿TAC是一種功能更加強大的重寫對策，其類型為simpset－＞thm list－＞tactic［9，10］，因此在應(yīng)用該對策時不僅要提供一個定理表作為參數(shù)，同時還要給出一個化簡集作為參數(shù)?；喖且粋€特定的集合，其中包含了一些特定領(lǐng)域的重寫定理。例如化簡集bool＿ss中包含了一些與布爾邏輯相關(guān)的定理，如｜－A B. （AB）＝ A∧ B；化簡集arith＿ss則是在bool＿ss的基礎(chǔ)上又添加了一些與自然數(shù)運算相關(guān)的定理，如｜－m n.（m＊n＝0）＝ （m＝0）∨ （n＝0）；而化簡集list＿ss是在arith＿ss的基礎(chǔ)上又增添了一些與表相關(guān)的定理，如｜－（LENGTH ［］＝0）∧ h t.LENGTH （h：：t）＝ SUC（LENGTH t）。應(yīng)用RW＿TAC的最大優(yōu)勢就是 HOL4系統(tǒng)可以根據(jù)指定的化簡集和給定的公理、定義、定理等對證明目標(biāo)及假設(shè)條件表進(jìn)行重寫，且能自動處理證明目標(biāo)結(jié)論中的全稱量詞、合取符、析取符、蘊含符，甚至是假設(shè)條件表中的存在量詞等等，另外該對策還具備自動執(zhí)行案例分解、決策程序等更加高級的功能。

通常情況下，由于RW＿TAC功能強大，利用它可以快速完成許多證明目標(biāo)的化簡或證明工作。特別是對于一個比較復(fù)雜的證明目標(biāo)，假如用戶不能確定一個預(yù)期的化簡目標(biāo)，更不清楚應(yīng)該使用HOL4系統(tǒng)中的哪些定理來化簡證明目標(biāo)，這時可以先根據(jù)該證明目標(biāo)的具體情況選取相關(guān)領(lǐng)域的化簡集，在定理表為空的情況下應(yīng)用RW＿TAC對證明目標(biāo)進(jìn)行重寫，此時可能會產(chǎn)生一些意想不到的化簡效果，還將有助于打開用戶的證明思路。

例如：對于上述的證明目標(biāo) “對任意的兩個自然數(shù)a與b，若b為0，則a＋b＝0”，假設(shè)用戶由于經(jīng)驗不足等問題不能確定一個預(yù)期的化簡目標(biāo)，且不清楚應(yīng)該利用HOL4系統(tǒng)中的哪些定理來化簡，則用戶可通過待證明目標(biāo)的背景確定該目標(biāo)與自然數(shù)的運算有關(guān)，因此可嘗試選取化簡集arith＿ss作為參數(shù)，應(yīng)用RW＿TAC對證明目標(biāo)進(jìn)行重寫，結(jié)果發(fā)現(xiàn)系統(tǒng)不但完成了重寫，而且還自動地完成了證明目標(biāo)的證明，一步到位。具體實現(xiàn)過程如下所示：

由此可見，RW＿TAC確實是一種非常強大的重寫對策，它不僅包含了前兩種重寫對策的功能，而且可以將化簡進(jìn)行得十分徹底，進(jìn)一步提高形式化證明的效率。

然而，RW＿TAC對策盡管強大，其應(yīng)用也存在著缺陷。比如說，有時會因為證明目標(biāo)被過于徹底地化簡而越過了某些中間結(jié)果，這反而可能不利于后續(xù)的形式化證明。這時可以考慮使用REWRITE＿TAC等一般的重寫對策，根據(jù)給定的定理得到特定的化簡效果。

綜上所述，在HOL4系統(tǒng)中實施形式化證明時，應(yīng)針對不同的證明目標(biāo)，根據(jù)不同重寫對策的功能、應(yīng)用方法、應(yīng)用環(huán)境和應(yīng)用中可能出現(xiàn)的問題等恰當(dāng)?shù)剡x用重寫對策，這樣才能提高形式化證明的有效性，并縮短形式化證明的時間。

2.2 重寫對策的定理參數(shù)的選擇

在HOL4系統(tǒng)提供的龐大定理庫中選擇合適的重寫定理作為參數(shù)是利用重寫對策對證明目標(biāo)進(jìn)行化簡或形式化證明的另一個關(guān)鍵點。作者通過對HOL4系統(tǒng)的研究與使用對定理的搜索過程進(jìn)行了探索，得出如下一些方法。

方法1：在HOL4系統(tǒng)中采用函數(shù)DB.match搜索所需定理。這種方法的優(yōu)點在于可按照所需定理的模式，在指定的理論中進(jìn)行搜索，從而縮小了搜索定理的范圍，提高了搜索效率。然而，采用這種方法的一個前提是必須能夠總結(jié)出所需定理的模式，且必須指定搜索的范圍，這也是本方法的局限性所在。

方法2：在HOL4系統(tǒng)中采用函數(shù)DB.find搜索所需定理。使用該方法可利用所需定理名字中的關(guān)鍵字，在當(dāng)前系統(tǒng)加載的所有理論中搜索名字中包含這些關(guān)鍵字的定理，而無需給出特定的搜索范圍，這是其優(yōu)勢所在。但是這種方法也具有明顯的缺點，即系統(tǒng)當(dāng)前未加載的理論不會納入搜索的范圍，這可能會降低搜索的有效性；且搜索出來的數(shù)據(jù)量一般比較大，需要逐個研究，找出有用的定理，這無疑會降低搜索的效率。

方法3：利用所需定理的名字或內(nèi)容中的關(guān)鍵字在HOL4官網(wǎng)所提供的定理庫中進(jìn)行搜索。這種方法沒有什么明顯的優(yōu)點，在前兩種方法失敗后，再使用該方法。這是因為定理庫包含了所有理論中的定理，搜索出來的數(shù)據(jù)量會更大，找出所需的定理將更加困難。

方法4：打開所有可能的理論，逐個查看，搜尋所需定理。這種方法是所有方法中最不方便，效率最低的，因而盡量在嘗試了前3種方法后再考慮之。

針對證明目標(biāo)的實際情況選擇恰當(dāng)?shù)乃阉鞫ɡ淼姆椒▽⒂兄诳焖儆行У卣业街貙懰璧亩ɡ?，從而保證重寫對策的順利應(yīng)用，達(dá)到對證明目標(biāo)的化簡或證明效果。

3 結(jié)束語

在HOL4系統(tǒng)中快速有效地進(jìn)行形式化證明依賴于對系統(tǒng)提供的數(shù)百個對策及幾千個定理的熟悉與了解，對普通用戶而言全部了解顯然不太現(xiàn)實，但是深入細(xì)致地了解像重寫對策這樣重要對策的功能、應(yīng)用方法、應(yīng)用環(huán)境及應(yīng)用中可能出現(xiàn)的問題還是十分必要的。本文對重寫對策在基于HOL4系統(tǒng)的形式化證明過程中的應(yīng)用進(jìn)行了分析與闡述，以期對HOL4系統(tǒng)用戶，特別是初學(xué)者提供一些幫助與啟發(fā)。此外，當(dāng)用戶對HOL4系統(tǒng)已有對策了解得十分透徹并熟練使用之后，用戶也可以嘗試著自行定義對策，以滿足各自的特殊需求，這也將會促進(jìn)HOL4系統(tǒng)的進(jìn)一步發(fā)展與完善，從而可以支持更多的形式化問題的解決。

［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－h(huán)elpdocs／help／HOLindex.html.