形式化方法以嚴(yán)格的數(shù)學(xué)化和機(jī)械化方法為基礎(chǔ)來規(guī)約、構(gòu)建和驗(yàn)證計(jì)算系統(tǒng),是改善和確保計(jì)算系統(tǒng)質(zhì)量的重要方法,其模型、技術(shù)和工具已延伸成為計(jì)算思維的重要載體。形式化方法中,形式化推導(dǎo)是通過對問題程序規(guī)約進(jìn)行精確變換,最終得到算法程序。形式化驗(yàn)證是在對軟件進(jìn)行規(guī)約的基礎(chǔ)上,驗(yàn)證軟件是否具有所期望的性質(zhì)。軟件形式化方法使軟件系統(tǒng)的描述更加精確,以減少可能的錯(cuò)誤所帶來的問題,提高軟件的可靠性。圖結(jié)構(gòu)在現(xiàn)實(shí)生活中應(yīng)用非常廣泛,圖的數(shù)據(jù)結(jié)構(gòu)廣泛應(yīng)用在公路運(yùn)輸網(wǎng)絡(luò)、地鐵線路網(wǎng)絡(luò)、網(wǎng)絡(luò)節(jié)點(diǎn)優(yōu)化等生活中的很多領(lǐng)域,另外計(jì)算機(jī)系統(tǒng)中的狀態(tài)執(zhí)行等也是基于圖數(shù)據(jù)結(jié)構(gòu)的。因此,圖的深度優(yōu)先遍歷算法在現(xiàn)代的各種軟件中應(yīng)用十分頻繁,這些軟件的可靠性的高低很大程度取決于圖的深度優(yōu)先算法是否正確完備。深度優(yōu)先算法的可靠性驗(yàn)證使用傳統(tǒng)的手工推導(dǎo)來驗(yàn)證已經(jīng)不能滿足我們的需要了,數(shù)學(xué)定理證明工具Isabelle與軟件形式化方法的結(jié)合既可以適應(yīng)日益繁瑣的軟件驗(yàn)證,又可以避免手工推導(dǎo)驗(yàn)證所帶來的失誤。Isabelle是一種通用的且支持高階邏輯的交互式定理證明器。它允許以正式語言表達(dá)數(shù)學(xué)公式,并提供用于在邏輯演算中證明這些公式的工具...

【文章頁數(shù)】：48 頁

【學(xué)位級別】：碩士

【文章目錄】：
中文摘要
英文摘要
第1章 緒論
    1.1 研究背景
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 主要研究工作
第2章 Isabelle定理證明器
    2.1 定理證明器的分類
    2.2 Isabelle定理證明器的剖析
    2.3 Isabelle定理證明器的規(guī)則和策略
    2.4 本章小結(jié)
第3章 圖結(jié)構(gòu)的規(guī)則庫和類型庫在 Isabelle 中的擴(kuò)充
    3.1 圖結(jié)構(gòu)擴(kuò)充
    3.2 DFS的定義及其定理在Isabelle中的證明
    3.3 本章小結(jié)
第4章 基于Isabelle的 DFS算法的驗(yàn)證
    4.1 算法程序驗(yàn)證的方法
    4.2 DFS算法的自動(dòng)化驗(yàn)證
    4.3 本章小結(jié)
總結(jié)
參考文獻(xiàn)
致謝



本文編號：3793997