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

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

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

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