形狀圖理論的定理證明及其在指針程序驗(yàn)證中的應(yīng)用.pdf

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

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

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

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