循環(huán)不變式自動(dòng)探測(cè).pdf

1、保障軟件的可靠性一直以來(lái)都是軟件開(kāi)發(fā)的熱點(diǎn)問(wèn)題，而采用形式化方法來(lái)開(kāi)發(fā)軟件是保障軟件可靠性的有效方法，其中形式化開(kāi)發(fā)軟件的關(guān)鍵是對(duì)算法程序中循環(huán)語(yǔ)句的分析與驗(yàn)證。而要很好的理解循環(huán)程序，其重點(diǎn)是要能正確的寫(xiě)出該循環(huán)程序的循環(huán)不變式。循環(huán)不變式無(wú)論是手工開(kāi)發(fā)，還是自動(dòng)構(gòu)造一直都是算法程序設(shè)計(jì)領(lǐng)域中最具挑戰(zhàn)性、最富有創(chuàng)造性、也是最困難的問(wèn)題之一。本文是國(guó)家自然科學(xué)基金面上項(xiàng)目“新概念循環(huán)不變式及其自動(dòng)探測(cè)技術(shù)研究”的研究方向之一。
　

2、　本文首先分析循環(huán)不變式現(xiàn)有定義及其開(kāi)發(fā)技術(shù)的國(guó)內(nèi)外研究現(xiàn)狀。之后介紹 PAR方法中關(guān)于循環(huán)不變式的新定義及新的開(kāi)發(fā)策略，也是本文構(gòu)造循環(huán)不變式的指導(dǎo)思想。接著介紹單元賦值語(yǔ)句型循環(huán)不變式的概念，并在本團(tuán)隊(duì)已有的循環(huán)不變式生成系統(tǒng)的基礎(chǔ)上，分析單元賦值語(yǔ)句的算法程序的循環(huán)不變式的構(gòu)造過(guò)程，發(fā)現(xiàn)有一類(lèi)單元賦值語(yǔ)句型的算法程序，在分劃過(guò)程中其分劃后的子問(wèn)題與原問(wèn)題的結(jié)構(gòu)不相同。對(duì)于此類(lèi)單元賦值語(yǔ)句型的算法程序，提出一種使用全稱(chēng)量詞的方式來(lái)刻

3、畫(huà)此類(lèi)單元賦值語(yǔ)句分劃過(guò)程中的不變性，進(jìn)而構(gòu)造循環(huán)不變式。最后使用 Java語(yǔ)言實(shí)現(xiàn)單元賦值語(yǔ)句型循環(huán)不變式自動(dòng)探測(cè)，并用Isabelle定理證明器對(duì)自動(dòng)構(gòu)造的循環(huán)不變式進(jìn)行機(jī)械的證明，相對(duì)于傳統(tǒng)的手工驗(yàn)證，具有更高的可靠性。
　　主要?jiǎng)?chuàng)新點(diǎn)包括以下3個(gè)方面：
　?。?）對(duì)于一類(lèi)單元賦值語(yǔ)句型的算法程序在分劃過(guò)程中其分劃后的子問(wèn)題與原問(wèn)題的結(jié)構(gòu)不相同的情況，提出一種使用全稱(chēng)量詞的方式來(lái)刻畫(huà)其分劃過(guò)程中的不變性，進(jìn)而構(gòu)造其循環(huán)