終止證明方法在形式化建模中的應(yīng)用①

任 憑,張 杰,關(guān) 永

1(北京化工大學(xué) 信息科學(xué)與技術(shù)學(xué)院,北京 100029)

2(首都師范大學(xué) 信息工程學(xué)院,北京 100048)

形式化方法是通過數(shù)學(xué)建模和數(shù)學(xué)歸納等方法去驗證目標(biāo)的性質(zhì)規(guī)范以及確保目標(biāo)的正確性和可靠性的一條重要途徑,其廣泛應(yīng)用于計算機軟硬件的規(guī)范,開發(fā)和驗證.

形式化驗證一般分為等價性檢驗,模型檢驗和定理證明3 種,并且驗證方式各不相同.等價性檢驗的方法主要是通過檢驗?zāi)繕?biāo)修改前后的一致性,來確保修改后的目標(biāo)至少包含修改前的性質(zhì),但是不能進(jìn)行特定性質(zhì)或規(guī)范的驗證.模型檢驗的特點是完全自動化,但是存在狀態(tài)空間爆炸的問題,不能用于驗證無限狀態(tài)空間的目標(biāo).定理證明的形式化方法是將待驗證的目標(biāo)和規(guī)范通過數(shù)學(xué)建模,描述為一系列的邏輯語言,并通過邏輯演算的方式,證明目標(biāo)是否具有規(guī)范所描述的性質(zhì).定理證明的驗證方法可以對目標(biāo)的所有狀態(tài)空間進(jìn)行建模和驗證,與傳統(tǒng)的仿真測試相比,測試空間更加完備,其驗證結(jié)果具有相當(dāng)高的可靠性.

當(dāng)前用于定理證明方法的主流工具有半自動的一階定理證明器Proverif,高階定理證明器HOL4,Isabelle等;也有全自動定理證明器SmartVerif.它們各有優(yōu)劣,半自動工具功能強大,拓展性高,但是學(xué)習(xí)門檻高;全自動工具入門容易但功能略遜一籌,實用性不如半自動定理證明器.本文用的是基于Standard ML 函數(shù)式語言的半自動高階定理證明器HOL4.

近年來,隨著形式化方法和定理證明器系統(tǒng)被廣泛應(yīng)用于數(shù)學(xué)定理[1],計算機軟件[2],硬件[3],方法[4,5]以及協(xié)議[6]的驗證和證明,系統(tǒng)自帶的數(shù)據(jù)結(jié)構(gòu)和定理庫已不能滿足所有形式化工作的需要;因此,用戶在進(jìn)行形式化建模時,常常需要自定義數(shù)據(jù)結(jié)構(gòu),特別是在HOL4中定義遞歸函數(shù)時用戶必須考慮函數(shù)的終止問題[7],這就給遞歸函數(shù)的形式化建模帶來困難.

1 問題的提出

介紹終止證明問題之前首先需要了解什么是遞歸函數(shù).對于任意函數(shù),定義函數(shù)的語句描述了輸入與輸出之間的邏輯關(guān)系,當(dāng)輸入任意符合要求的x,都可以得到其對應(yīng)的唯一輸出.一般非遞歸函數(shù)f(x)在定義時可以調(diào)用外部函數(shù),但不會調(diào)用函數(shù)自身,如圖1所示.

圖1 一般非遞歸函數(shù)f(x)

而與之不同的是,遞歸是通過調(diào)用自身的代碼來解決問題,遞歸方法是計算機科學(xué)的核心思想之一[8].在使用遞歸函數(shù)進(jìn)行建模的過程中,如果考慮不周,使得在某些輸入的情況下,出現(xiàn)無限遞歸的情況,如圖2所示.在形式化建模中不允許遞歸函數(shù)無限調(diào)用自身無法得到輸出的情況存在.因此,建立滿足終止證明規(guī)范的遞歸函數(shù)模型是完成遞歸函數(shù)形式化證明的必要條件.

圖2 缺少終止條件的遞歸函數(shù)f(x)

為了使遞歸函數(shù)的形式化模型能夠滿足規(guī)范,需要在遞歸調(diào)用之前添加一個判斷語句,如圖3所示,使得輸入?yún)?shù)在滿足某些特定條件下不再進(jìn)行遞歸,而是得到相應(yīng)的輸出;而結(jié)束遞歸的判斷條件被稱為遞歸出口或終止條件.

圖3 有終止條件的遞歸函數(shù)

并且,在形式化建模過程中定義遞歸函數(shù),與使用非形式化語言定義函數(shù)的過程有很大的區(qū)別:在非形式化的定義當(dāng)中,一個沒有終止條件或終止條件不完備的遞歸函數(shù)也能被成功定義,直到它在實際調(diào)用中發(fā)生錯誤時才會拋出錯誤;而由于形式化方法的嚴(yán)謹(jǐn)性,在其定義遞歸函數(shù)時,首先必須證明它滿足“輸入集中的任意元素在輸出集中都存在唯一對應(yīng)”的規(guī)范,該證明過程被稱為終止性證明,若無法完成終止證明,就無法成功定義且使用該函數(shù).所以,在HOL4中定義遞歸函數(shù)的關(guān)鍵是要確定其終止條件.在終止條件不夠全面的情況下,終止證明必然失敗,同時證明過程將暴露終止條件中的問題,幫助用戶發(fā)現(xiàn)和補全終止條件的漏洞.然而,即使保證了終止條件的完備性,為什么定理證明器仍然無法自動完成所有遞歸函數(shù)的終止證明?

在一些定理證明器的定理庫中,存在列表等基礎(chǔ)的數(shù)據(jù)結(jié)構(gòu)和相關(guān)的性質(zhì)定理,當(dāng)使用這些結(jié)構(gòu)進(jìn)行遞歸定義時,定理證明器基本能夠自動的完成終止證明.而在HOL4 定理證明器中,存在集合結(jié)構(gòu)和相關(guān)的定理庫,但仍然無法完成一部分集合遞歸函數(shù)的終止證明,這是因為HOL4的集合定理庫中缺少一些集合遞歸函數(shù)終止證明所需的定理,這些所需定理可以用已存在的定理推導(dǎo)得到,但是半自動定理證明器在自動進(jìn)行終止證明的過程中,不能將定理庫中定理進(jìn)行組合,推導(dǎo)得到新的定理后用于終止證明.所以當(dāng)系統(tǒng)無法自動完成終止證明時,意味著系統(tǒng)的定理庫中缺少關(guān)鍵的定理或引理,需要用戶自行推導(dǎo),并將其用于證明終止目標(biāo).

當(dāng)定理證明器無法自動完成終止證明時,如何手動輔助定理證明器完成終止證明是建模過程中的一個難題.本文主要介紹一種解決方案,能夠用于形式化建模過程中定義遞歸函數(shù)所產(chǎn)生的終止證明問題.

2 解決方案

終止證明問題的本質(zhì)是通過定理證明的形式化方法證明新定義的遞歸函數(shù)滿足“輸入集中的任意元素在輸出集中都存在唯一對應(yīng)”的規(guī)范.換而言之,遞歸函數(shù)在任意輸入?yún)?shù)時,經(jīng)過有限次遞歸后,終將滿足終止條件,得到相應(yīng)的輸出,所以該問題著重關(guān)注于輸入?yún)?shù)在遞歸過程是否具有不斷接近終止條件的趨勢.

在基于HOL4的形式化建模工作的實踐過程中,本文總結(jié)出定義兩大類定理證明器經(jīng)常無法自動完成終止證明的遞歸函數(shù):

1)使用自定義數(shù)據(jù)結(jié)構(gòu)作為參數(shù)時.在工作過程中驗證新目標(biāo)時,往往需要用到新的數(shù)據(jù)結(jié)構(gòu),如鏈結(jié)構(gòu),圖結(jié)構(gòu)等等.但是在系統(tǒng)的定理庫中,只有少量自定義數(shù)據(jù)結(jié)構(gòu)的衍生謂詞,性質(zhì)定理和函數(shù),故使用自定義的數(shù)據(jù)結(jié)構(gòu)定義遞歸函數(shù)時,針對不同的遞歸函數(shù),需要構(gòu)建和證明不同的功能函數(shù)和性質(zhì)定理,輔助系統(tǒng)完成終止證明.

2)使用自定義的函數(shù)作為參數(shù)時.

當(dāng)進(jìn)行形如式(1)的遞歸函數(shù)定義時(其中h(x)也是自定義的函數(shù)).無論參數(shù)x的數(shù)據(jù)結(jié)構(gòu)是否是自定義結(jié)構(gòu),都需要手動輔助其完成終止證明.

如上所述,具有明確的終止條件是解決終止證明問題的前提,確定待定義的遞歸函數(shù)的終止條件是解決問題的第一步.充分考慮輸入?yún)?shù)的可能性后,一個完整的終止條件通常由復(fù)數(shù)通過析取連接的子條件組成.這些子條件在輸入集合的基礎(chǔ)上分割出若干個非空真子集,若輸入?yún)?shù)屬于這些子條件描述的真子集中,則將得到確定的輸出,否則繼續(xù)遞歸.將終止條件描述的集合稱為輸入集合的終止子集,將終止子集的補集稱為輸入集合的遞歸子集.

假設(shè)目標(biāo)遞歸函數(shù)設(shè)置了合適的終止條件,即可通過系統(tǒng)中存在的函數(shù)或定義方法,編譯定義語句.在不同的定理證明器中所使用的函數(shù)和方法存在區(qū)別,但是目標(biāo)和思路大體相同,以下將以HOL4 定理證明器中的函數(shù)和方法為例進(jìn)行詳細(xì)分解.

在HOL4 定理證明器中,使用Hol_defn 方法編譯遞歸函數(shù)的定義語句,系統(tǒng)將剝離出終止條件和遞歸參數(shù),再使用Defn.tgoal 方法即可得到終止證明目標(biāo).終止證明目標(biāo)將剔除與遞歸無關(guān)的定義語句,關(guān)注于輸入?yún)?shù)在遞歸過程中的變化趨勢.

系統(tǒng)通過證明輸入?yún)?shù)在遞歸過程中存在某種指標(biāo)一步步的由遞歸子集趨近于終止子集來說明函數(shù)必定終止,用戶需要輔助系統(tǒng)的工作首先是明確該指標(biāo).例如在遞歸函數(shù)實現(xiàn)的列表遍歷方法中,若終止條件為輸入?yún)?shù)等于空列表,輸入列表的長度在每次遞歸時遞減.因此列表的長度屬性是指標(biāo),通過函數(shù)量化列表的長度,并且將終止條件描述的空列表的長度設(shè)定為固定值x,在遞歸的過程中列表長度量化值不斷的向x趨近,即可證明在有限次遞歸后,輸入?yún)?shù)的列表長度必將等于x,從而觸發(fā)終止條件,得到確定的輸出.

在HOL4 定理證明器的終止證明中,需要將以上的趨近關(guān)系改寫成值域為自然數(shù)的單調(diào)遞減函數(shù),終止證明的目標(biāo)變化為證明該函數(shù)的單調(diào)遞減性.在一些復(fù)雜的遞歸函數(shù)中,如圖的深度優(yōu)先和廣度優(yōu)先遍歷算法中,同時對圖的深度和廣度進(jìn)行遞歸,需要選取復(fù)數(shù)個指標(biāo)進(jìn)行量化,并且構(gòu)建合適的單調(diào)遞減函數(shù).

將終止證明目標(biāo)轉(zhuǎn)化為單調(diào)遞減性證明后,根據(jù)具體目標(biāo)不同,證明方法也不同.對于定理證明器無法自動證明的子目標(biāo),有可能是缺少一些引理,或者是缺少相關(guān)自定義結(jié)構(gòu)的性質(zhì)定理.應(yīng)推理出詳細(xì)的證明過程,證明輔助定理并推進(jìn)證明目標(biāo).

最后將終止證明過程中使用的方法和對策整理為策略,使用定理證明器中的相關(guān)方法將定義語句與策略進(jìn)行整合,規(guī)范建模格式.

通過詳細(xì)分析,無論是使用自定義數(shù)據(jù)結(jié)構(gòu)或定義嵌套遞歸函數(shù)的情況,都可以按照以下方法來進(jìn)行函數(shù)定義和終止證明.

算法1.終止證明方法(1)分析待定義函數(shù)的輸入集,明確終止條件.(2)分析遞歸過程,確定輸入?yún)?shù)中在遞歸過程中變化最明顯的可量化屬性,定義量化函數(shù),并根據(jù)每個終止子條件設(shè)置固定的量化值.(3)使用定理證明器中手動進(jìn)行終止證明的定義方法,得到終止證明目標(biāo).(4)根據(jù)終止子條件的固定值和輸入?yún)?shù)在遞歸過程中的變化趨勢,構(gòu)建單調(diào)遞減函數(shù),并將終止證明目標(biāo)簡化為所構(gòu)建函數(shù)的單調(diào)遞減性證明.(5)在證明過程中補充系統(tǒng)定理庫缺少的定理和引理,輔助系統(tǒng)推進(jìn)證明.如果在證明過程中遇到無法被證明的子目標(biāo),回到第(1)步檢查是否缺失終止子條件.(6)完成終止證明,整理定義和證明過程,規(guī)范建模格式.

3 應(yīng)用實例

在實際應(yīng)用中,經(jīng)常會需要用到圖結(jié)構(gòu)來表示節(jié)點與節(jié)點間的連接關(guān)系.而HOL4 定理庫中暫時沒有圖的數(shù)據(jù)結(jié)構(gòu)和相關(guān)性質(zhì)定理,所以需要用戶自定義圖結(jié)構(gòu).因此,下面將以自定義圖結(jié)構(gòu)作為遞歸參數(shù),在HOL4中使用該終止證明方法完成一個遞歸函數(shù)定義和終止證明.在該應(yīng)用中,定義graph 結(jié)構(gòu)包含了存儲圖中節(jié)點信息的集合nodes,以及節(jié)點之間連接關(guān)系的集合edges,其中點集nodes 與邊集edges的論域都為全集,graph的論域為點集nodes 與邊集edges的笛卡爾乘積.

有向圖的定義約束了點集與邊集之間的關(guān)系,故有向圖集是graph的真子集.因此將有向圖定義進(jìn)行形式化,得到謂詞Digraph 將輸入集切分為有向圖集與非有向圖,并以此作為以graph 作為輸入?yún)?shù)的有向圖的遞歸函數(shù)的第一個終止子條件:當(dāng)輸入?yún)?shù)不屬于有向圖集時將終止遞歸,如圖4所示.

圖4 graph 類型與有向圖關(guān)系示意圖

此外,在實現(xiàn)節(jié)點的信息統(tǒng)計等功能函數(shù)時,需要遍歷一個有向圖中的所有節(jié)點.在HOL4 定理證明器使用的Standard ML 函數(shù)式語言中,沒有循環(huán)語句,取而代之的是使用遞歸的方法來實現(xiàn)循環(huán)和遍歷的效果.由于HOL4 定理庫中缺少自定義的graph 結(jié)構(gòu)的相關(guān)性質(zhì)定理,所以使用者必須手動輔助定理證明器完成終止證明.下面將詳細(xì)介紹如何使用以上給出的方法,完成圖節(jié)點遍歷遞歸函數(shù)的終止證明.

3.1 實現(xiàn)過程

首先,繼續(xù)設(shè)置終止條件切分輸入集.待實現(xiàn)的遞歸函數(shù)功能為遍歷圖中所有節(jié)點,若點集nodes為無限集,則遍歷行為無意義,故得到第2 個終止子條件:當(dāng)輸入?yún)?shù)的點集nodes 不屬于有限集時將終止遞歸;若輸入為空圖,則不需要繼續(xù)遍歷,將輸出固定值,因此得到第3 個終止子條件:當(dāng)輸入?yún)?shù)不屬于非空圖時將終止遞歸.通過3 個終止子條件,將輸入集切分為如圖5所示的真子集.

圖5 通過謂詞切割有向圖集

當(dāng)輸入?yún)?shù)不僅屬于如圖所示的有向圖集合時,將終止遞歸并輸出.

終止條件的確定也明確了遞歸過程中,輸入?yún)?shù)在遞歸的過程中應(yīng)不斷趨向于終止條件.在圖節(jié)點遍歷函數(shù)中,可以將輸入的圖參數(shù)視作“已遍歷”和“未遍歷”兩部分.在遞歸過程中,“未遍歷”的部分將持續(xù)減少,在遍歷完成時“未遍歷”部分應(yīng)當(dāng)為空,滿足第3 個終止子條件.因此,對于該遞歸函數(shù)的終止證明問題,應(yīng)當(dāng)關(guān)注輸入?yún)?shù)“未遍歷”部分的節(jié)點規(guī)模,并定義合適圖規(guī)模量化函數(shù),設(shè)置空圖的規(guī)模為0.

在HOL4 定理證明器中,使用Hol_defn 方法和Defn.tgoal 方法可以得到終止證明目標(biāo),為了簡化目標(biāo)中不必要的部分,關(guān)注于證明遞歸參數(shù)量化指標(biāo)的遞減性,使用WF_REL_TAC 對策簡化目標(biāo)并重寫展開自定義的函數(shù)后,得到兩個子目標(biāo).

?

查閱定理證明器中的集合定理庫可知,系統(tǒng)拋出該子目標(biāo)無法繼續(xù)的原因是庫中缺少處理{x|x ∈ s ∧x≠ CHOICE s}的相關(guān)定理,需要用戶輔助證明.因此,利用定理證明器提供的集合定理庫,證明以下引理:

引理1.對于任意的集合s,由s中CHOICE s 元素以外的元素組成的新集合,等于REST s 集合.

?s.{x|x ∈ s ∧ x≠ CHOICE s}=REST s

引理2.對于任意集合s,如果s為非空有限集,則CARD s 大于0.

?s.FINITE s ∧ s≠ ? ? 0

借助引理即可完成子目標(biāo)1的證明.然后關(guān)注子目標(biāo)2.

?

觀察可知,系統(tǒng)拋出此目標(biāo)的原因不僅是缺少子目標(biāo)1中的兩個引理,而且缺少圖的相關(guān)性質(zhì)定理:當(dāng)邊集非空時,點集必定非空.該定理由圖的定義與空圖的定義推導(dǎo)而來.

有向圖性質(zhì)1 邊集非空的有向圖點集必然非空

?G.Digraph G ∧ G.edges≠ ? ? G.nodes≠ ?

借由引理1和引理2,圖的性質(zhì)定理和定理證明器的相關(guān)定理庫,即可完成該遍歷函數(shù)的終止證明.最后將對策整理為策略,并使用Defn.tprove 方法定義該函數(shù).

在本實例中,可見使用本文提出的終止證明方法解決終止證明問題,思路非常清晰,迅速確定終止條件,補充必要的謂詞和函數(shù),將終止證明目標(biāo)簡化為圖的節(jié)點數(shù)量在遞歸過程中的遞減性證明,準(zhǔn)確找到終止證明過程中缺少的兩個集合引理和一個圖的性質(zhì)定理,順利完成終止目標(biāo)的證明,解決終止證明問題,從而在HOL4中成功定義圖的節(jié)點遍歷遞歸函數(shù).

4 結(jié)語

形式化建模工作中對遞歸函數(shù)的應(yīng)用十分廣泛而且重要.由于定理證明器的定理庫更新上的嚴(yán)謹(jǐn)和滯后,在涉及到遞歸函數(shù)的建模過程中,特別是使用到自定義的數(shù)據(jù)結(jié)構(gòu)進(jìn)行遞歸的建模中,經(jīng)常出現(xiàn)定理證明器無法自動完成終止證明的問題,導(dǎo)致遞歸函數(shù)無法被成功定義和使用,阻礙了形式化方法的應(yīng)用和發(fā)展.

本文針對上述問題,介紹了在形式化工作中為什么會遇到終止證明問題,以及解決終止證明問題的必要性;分析了定理證明器無法自動完成終止證明的原因;設(shè)計了一種在形式化建模中通用的終止證明方法,并將該方法應(yīng)用于基于HOL4 定理證明器的一個實例中.在不同的定理證明器中,使用的具體對策和函數(shù)有所不同,但是方法的步驟和思路是相同的,以可量化的指標(biāo)作為終止條件的遞歸函數(shù)可以使用該方法進(jìn)行定義并證明.該方法很大程度方便了形式化建模的初學(xué)者在定理證明器中定義和使用自己的數(shù)據(jù)結(jié)構(gòu)和遞歸函數(shù),使用形式化方法解決更具體和實際的問題.

同時,該方法尚存不足,無法解決式(2)形式的自嵌套遞歸函數(shù)的終止證明問題.