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

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

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

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