重寫對(duì)策在基于HOL的形式化證明中的應(yīng)用

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

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

0 引 言

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

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

1 形式化證明與對(duì)策

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

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

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

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

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

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

2.1 幾個(gè)典型的重寫對(duì)策

（1）REWRITE＿TAC對(duì)策

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

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

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

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

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

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

（2）ASM＿REWRITE＿TAC對(duì)策

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

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

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

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

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

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

（3）RW＿TAC對(duì)策

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

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

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

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

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

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

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

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

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

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

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

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

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

3 結(jié)束語(yǔ)

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