算法的形式化推導與基于Isabelle的自動化驗證.pdf

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

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

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