基于PAR平臺(tái)的最弱前置謂詞生成器的設(shè)計(jì)與實(shí)現(xiàn).pdf

1、從上世紀(jì)六十年代起，隨著大型軟件的快速發(fā)展，人們對(duì)軟件質(zhì)量的要求起來(lái)越高，尤其是對(duì)軟件的正確性要求。計(jì)算機(jī)界為確保軟件質(zhì)量尤其是軟件的高可靠性方面提出了許多新的理論研究，程序正確性證明就是其中之一，程序正確性證明就是采用嚴(yán)格的數(shù)學(xué)方法評(píng)價(jià)一個(gè)程序是否達(dá)到了預(yù)定的性能。但是在證明程序正確的過(guò)程中由于要涉及大量的數(shù)學(xué)符號(hào)和數(shù)學(xué)相關(guān)理論知識(shí)使得程序驗(yàn)證人員需要花費(fèi)一定的時(shí)間和精力去掌握這些知識(shí)。而且由于涉及到數(shù)學(xué)理論即使驗(yàn)證一個(gè)很短的程序也需

2、要比較繁瑣的驗(yàn)證過(guò)程，造成往往證明過(guò)程比要證明的程序要復(fù)雜很多的情況，這些種種不利條件使得依靠手工去證明程序正確性就可能產(chǎn)生許多不良的后果。
　　 為了克服手工對(duì)程序進(jìn)行正確性驗(yàn)證程序所導(dǎo)致的不良后果，許多計(jì)算機(jī)科學(xué)家開始利用機(jī)器去自動(dòng)驗(yàn)證程序來(lái)逐步降低人工干預(yù)程序驗(yàn)證的過(guò)程，最終的目的是將程序正確性驗(yàn)證走向完全自動(dòng)化。
　　 根據(jù)Dijkstra的最弱前置謂詞理論，對(duì)于程序{Q}S{R]，如果能證明：Q=>WP(“S”

3、，R)則能斷定程序正確。正是基于此理論，本文研究作為PAR平臺(tái)的一個(gè)輔助工具部分，目標(biāo)是開發(fā)一個(gè)自動(dòng)計(jì)算Apla程序的最弱前置謂詞的系統(tǒng)，減少Apla程序正確性驗(yàn)證的人工干預(yù)，在已知S，R的情況下自動(dòng)求解出最弱前置謂詞。圍繞這個(gè)宗旨本文做了如下工作：
　　 1、在深刻理解了Dijkstra最弱前置謂詞的的基礎(chǔ)上提出了自動(dòng)計(jì)算Apla語(yǔ)言最弱前置謂詞的算法。
　　 2、選取了若干Apla程序進(jìn)行試驗(yàn)，實(shí)驗(yàn)結(jié)果表明，系統(tǒng)初步