循環(huán)不變式自動探測.pdf

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

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

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