形狀圖邏輯擴(kuò)展的實(shí)現(xiàn).pdf

1、信息時代的發(fā)展，引領(lǐng)計算機(jī)軟件應(yīng)用深入到千家萬戶，各行各業(yè)。隨著軟件的應(yīng)用領(lǐng)域迅速加大，規(guī)模急速擴(kuò)張，軟件安全性的要求也逐步提升，軟件調(diào)試和維護(hù)的成本越來越高，軟件的安全形勢日漸嚴(yán)峻。基于邏輯推理的形式驗(yàn)證是提高軟件可信程度的一種重要方法。進(jìn)入21世紀(jì)來，國際國內(nèi)對該方法的推廣和工業(yè)應(yīng)用進(jìn)行了大量的研究與開發(fā)，本實(shí)驗(yàn)室（中科大一耶魯高可信軟件聯(lián)合研究中心）在并行程序的驗(yàn)證方法和串行程序的驗(yàn)證工具的研發(fā)工作也相當(dāng)活躍。
　　本文工作

2、基于一個類C小語言PointerC的程序驗(yàn)證器原型。它是研究操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序的驗(yàn)證的試驗(yàn)性工具。
　　本文對此驗(yàn)證器進(jìn)行了兩方面擴(kuò)展，一是使驗(yàn)證器可以更好地用于一維數(shù)組程序的驗(yàn)證。二是使驗(yàn)證器能用于操作帶附加單鏈表的數(shù)據(jù)結(jié)構(gòu)的程序的驗(yàn)證。
　　本文的主要貢獻(xiàn)如下:
　　第一，設(shè)計并實(shí)現(xiàn)了對一維數(shù)組元素進(jìn)行賦值的語句的推理規(guī)則，并將此規(guī)則延伸應(yīng)用到全稱量詞的約束變元出現(xiàn)在訪問路徑的上角標(biāo)中的情況。
　　原

3、型系統(tǒng)雖然主要是針對指針程序設(shè)計的，但同時也考慮了操作其他數(shù)據(jù)類型的程序的驗(yàn)證，比如操作數(shù)組的程序的驗(yàn)證。操作一維數(shù)組的程序中，數(shù)組的很多性質(zhì)需要使用量化斷言（如全稱斷言）來描述。這樣在遇到數(shù)組元素的賦值語句時，在運(yùn)行賦值公理時需要使用本文設(shè)計的規(guī)則對量化斷言進(jìn)行展開。同理，此規(guī)則也適用在驗(yàn)證包含帶上角標(biāo)表達(dá)式的全稱量詞的程序中。
　　第二，設(shè)計并實(shí)現(xiàn)了一種操作帶附加鏈表的數(shù)據(jù)結(jié)構(gòu)的程序的驗(yàn)證方法。在形狀分析時，若想讓附加鏈表指針