形狀圖理論的定理證明及其在指針程序驗證中的應用.pdf

1、隨著信息時代的到來和深入，計算機技術已經(jīng)在各行各業(yè)中得到了廣泛地應用。但隨著計算機軟件系統(tǒng)的普及和規(guī)模的不斷增大，其安全性問題也越來越突出。提高軟件可靠程度的方法有很多，形式程序驗證是其中一個重要的方法?；谶壿嬐评硎浅绦蝌炞C中最嚴格也最可靠的，它根據(jù)特定的程序邏輯通過形式化的數(shù)學推導演算，并利用定理證明工具來證明。但由于自動推斷循環(huán)不變式困難、斷言語言表達力弱以及自動定理證明能力有限等諸多原因，形式程序驗證尚未在工業(yè)界得到應用。

2、>　　 本文的工作建立在一個基于形狀圖邏輯的自動程序驗證原型系統(tǒng)上，主要用于指針程序的驗證。該驗證過程主要分成兩個階段:第一階段是對指針程序進行形狀分析，第二階段是利用形狀分析得到的結(jié)果進行程序驗證。其中，形狀分析階段使用形狀圖邏輯和形狀系統(tǒng)，實現(xiàn)了循環(huán)不變形狀圖的自動推斷，并且對于非遞歸函數(shù)可以推斷出函數(shù)前后形狀圖。
　　 本文主要的研究工作是形狀圖理論的定理證明及其在指針程序驗證中的應用。形狀圖理論主要包括形狀圖重寫系統(tǒng)、

3、形狀圖等價判定方法和形狀圖蘊涵判定方法;形狀圖理論在指針程序驗證中的應用主要包括對循環(huán)不變形狀圖和遞歸函數(shù)前后形狀圖的推斷。通過對系統(tǒng)原型做擴展之后，系統(tǒng)能夠驗證帶遞歸的指針程序。
　　 本文的主要貢獻是:
　　 第一，設計并實現(xiàn)了形狀圖理論的判定方法。
　　 形狀圖及其等價變換規(guī)則和蘊涵變換規(guī)則可分別類比為代數(shù)項及其等式規(guī)則和重寫規(guī)則，因而可像研究代數(shù)規(guī)范的理論那樣來研究形狀圖理論。我們定義了形狀圖重寫系統(tǒng)及其

4、終止性、局部合流性和合流性等概念，最后得到基于形狀圖重寫的形狀圖等價判定和蘊涵判定的方法。
　　 第二，設計并實現(xiàn)了指針類型遞歸函數(shù)前后形狀圖的自動推斷方法。
　　 該自動推斷方法源子一個通過迭代推斷循環(huán)不變式的一般方法，并借助了上述形狀圖理論的判定方法。該方法的實現(xiàn)使得原型系統(tǒng)能夠用于指針類型遞歸程序驗證。
　　 通過上述方法的實現(xiàn)以及對系統(tǒng)原型其他地方的完善，系統(tǒng)原型能夠驗證平衡二叉排序樹和自頂向下伸展樹等復