算法的形式化推導(dǎo)與基于Isabelle的自動(dòng)化驗(yàn)證.pdf

1、可信軟件的不斷發(fā)展，進(jìn)一步推動(dòng)了形式化方法的深入研究。形式化方法具有嚴(yán)格的數(shù)學(xué)語(yǔ)言和精確的邏輯語(yǔ)義，從而保證軟件在開(kāi)發(fā)過(guò)程中的正確性。
　　形式化方法主要包括形式化推導(dǎo)和形式化驗(yàn)證兩個(gè)部分。形式化推導(dǎo)是通過(guò)對(duì)問(wèn)題程序規(guī)約進(jìn)行精確變換，最終得到算法程序。形式化驗(yàn)證是在對(duì)軟件進(jìn)行規(guī)約的基礎(chǔ)上,驗(yàn)證軟件是否具有所期望的性質(zhì)。形式化方法對(duì)保證軟件正確性和可靠性具有十分重要的意義。
　　本文從形式化推導(dǎo)和自動(dòng)化驗(yàn)證兩方面研究提高算法程

2、序正確性的有效途徑。
　　在形式化推導(dǎo)方面，采用基于遞推技術(shù)的算法形式化方法開(kāi)發(fā)算法程序，通過(guò)程序規(guī)約變換技術(shù)對(duì)形式化程序規(guī)約進(jìn)行等價(jià)變換，得到問(wèn)題求解的遞推關(guān)系和循環(huán)不變式，以此為基礎(chǔ)得到算法程序。該方法不僅清晰地展示了算法的設(shè)計(jì)思路與過(guò)程，而且有效保證了算法程序的正確性。
　　在自動(dòng)化驗(yàn)證方面，選擇Isabelle定理證明器為工具。Isabelle傳統(tǒng)應(yīng)用領(lǐng)域?yàn)閿?shù)學(xué)定理證明，本文結(jié)合驗(yàn)證需要在對(duì)其內(nèi)置類(lèi)型庫(kù)和規(guī)則庫(kù)進(jìn)行擴(kuò)

3、充的基礎(chǔ)上，探索將它應(yīng)用于算法程序自動(dòng)化驗(yàn)證以及問(wèn)題求解序列遞推關(guān)系自動(dòng)化驗(yàn)證的有效方法。論文從三個(gè)層面深入剖析了Isabelle定理證明器，從三個(gè)部分展示了 Isabelle的理論證明過(guò)程。結(jié)合本文兩方面驗(yàn)證工作的需要，對(duì)Isabelle的類(lèi)型庫(kù)和規(guī)則庫(kù)進(jìn)行了擴(kuò)充，完成了新添加規(guī)則的內(nèi)部形式轉(zhuǎn)換和正確性驗(yàn)證，以及新類(lèi)型的嵌入；然后以此擴(kuò)充的Isabelle類(lèi)型庫(kù)和規(guī)則庫(kù)為基礎(chǔ)，采用后推證明方式，結(jié)合Dijkstra最弱前置謂詞方法，給