循環(huán)不變式開發(fā)技術(shù)研究.pdf

1、高可靠性軟件是當(dāng)今軟件開發(fā)的熱點問題。確保算法程序邏輯結(jié)構(gòu)正確最理想途徑是算法程序的形式化推導(dǎo)和證明。循環(huán)不變式在軟件形式化方法中占有十分重要的地位，它是理解、證明和推導(dǎo)算法程序的基礎(chǔ)和關(guān)鍵。使用形式化方法來證明或推導(dǎo)算法程序無法回避的一個問題就是給出正確的循環(huán)不變式。但是循環(huán)不變式的開發(fā)一直是算法程序設(shè)計領(lǐng)域中最具挑戰(zhàn)性、最富有創(chuàng)造性、也是最困難的問題之一。自形式化方法出現(xiàn)以來，眾多專家致力于循環(huán)不變式的開發(fā)，提出了許多循環(huán)不變式開發(fā)

2、技術(shù)，如謂詞抽象技術(shù)、動態(tài)探測技術(shù)等。這些技術(shù)能探測出較簡單問題的循環(huán)不變式，但是卻無法處理復(fù)雜問題。 從本質(zhì)上來說，循環(huán)不變式刻畫了循環(huán)變量的變化規(guī)律和循環(huán)程序的特征，因此一個循環(huán)程序的循環(huán)不變式并非輕易就能得到，尤其是對復(fù)雜算法的來說，必須在對循環(huán)程序的算法本質(zhì)有充分理解的基礎(chǔ)上才能找到。而現(xiàn)有的循環(huán)不變式定義不能反映出循環(huán)不變式的本質(zhì)，基于現(xiàn)有循環(huán)不變式定義的技術(shù)缺乏理論上的指導(dǎo)，在探測循環(huán)不變式的過程中具有試探性和盲目性

3、，又因為本身技術(shù)上的限制，因而無法得出復(fù)雜問題的循環(huán)不變式。 薛錦云教授及其學(xué)術(shù)團(tuán)隊分析了大量算法程序的本質(zhì)特征及其與循環(huán)不變式關(guān)系[15]～[20]，發(fā)現(xiàn)現(xiàn)有循環(huán)不變式定義的不足，提出了關(guān)于循環(huán)不變式的新定義和基于新定義之上的循環(huán)不變式開發(fā)技術(shù)，并在此基礎(chǔ)上形成了一種實用的算法程序形式化開發(fā)方法—PAR方法及其開發(fā)環(huán)境，在復(fù)雜算法程序及軟件形式化開發(fā)中發(fā)揮了重要作用。本文是PAR方法及其開發(fā)環(huán)境研究的繼續(xù)，也是薛錦云主持承擔(dān)的

4、國家自然科學(xué)基金項目“基于PAR方法的算法設(shè)計形式化和自動化研究”和973前期預(yù)研項目“形式化方法制導(dǎo)的軟件自動化研究”的重要研究內(nèi)容。 本文主要的工作是對現(xiàn)有循環(huán)不變式定義和現(xiàn)有開發(fā)技術(shù)進(jìn)行深入研究，并與PAR方法中的循環(huán)不變式開發(fā)技術(shù)進(jìn)行比較，指出了現(xiàn)有開發(fā)技術(shù)的不足之處；同時基于薛錦云教授提出的循環(huán)不變式新定義和新開發(fā)技術(shù)，探討、研究并初步實現(xiàn)了循環(huán)不變式自動開發(fā)系統(tǒng)。具體研究成果如下： 1．深入研究了循環(huán)不變式定