程序分析與程序驗證_第1頁
程序分析與程序驗證_第2頁
程序分析與程序驗證_第3頁
程序分析與程序驗證_第4頁
已閱讀5頁,還剩8頁未讀, 繼續(xù)免費閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報或認(rèn)領(lǐng)

文檔簡介

1、程序分析與程序驗證程序分析與程序驗證計算機科學(xué)技術(shù)系計算機科學(xué)技術(shù)系陳意云陳意云0551-課課 程程 簡簡 介介計算機科學(xué)的理論體系計算機科學(xué)的理論體系1、模型理論、模型理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M,哪些問題可以由模型,哪些問題可以由模型M解決解決 如何比較模型的表達(dá)能力如何比較模型的表達(dá)能力 經(jīng)典計算經(jīng)典計算 確定的圖靈機,可計算性理論屬于模型理論確定的圖靈機,可計算性理論屬于模型理論 新型計算新型計算 本質(zhì)特點是交互本質(zhì)特點是交互( 并發(fā)、分布、網(wǎng)絡(luò)、網(wǎng)格、云并發(fā)、分布、網(wǎng)絡(luò)、網(wǎng)格、云 ) 計算和交互的統(tǒng)一模型理論尚未出現(xiàn)計算和交互的統(tǒng)一模型理論尚未出現(xiàn)課課 程程 簡簡

2、介介計算機科學(xué)的理論體系計算機科學(xué)的理論體系2、程序理論、程序理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M,如何用模型,如何用模型M解決問題解決問題 包括的領(lǐng)域包括的領(lǐng)域 程序設(shè)計范型、程序設(shè)計語言、程序設(shè)計、形式程序設(shè)計范型、程序設(shè)計語言、程序設(shè)計、形式語義、類型論、程序驗證、程序分析等語義、類型論、程序驗證、程序分析等課課 程程 簡簡 介介計算機科學(xué)的理論體系計算機科學(xué)的理論體系3、計算理論、計算理論 關(guān)心的問題關(guān)心的問題 給定模型給定模型M和一類問題,解決該類問題需要多少和一類問題,解決該類問題需要多少資源資源 包括的領(lǐng)域包括的領(lǐng)域 計算復(fù)雜性理論計算復(fù)雜性理論課課 程程 簡簡 介介作

3、為編譯原理的后續(xù)課程,可選內(nèi)容列舉:作為編譯原理的后續(xù)課程,可選內(nèi)容列舉: 獨立于機器的優(yōu)化(涉及,但不是重點)獨立于機器的優(yōu)化(涉及,但不是重點) 依賴于機器的優(yōu)化(留給高級系統(tǒng)結(jié)構(gòu)課程)依賴于機器的優(yōu)化(留給高級系統(tǒng)結(jié)構(gòu)課程) 形式語義和類型論(程序設(shè)計語言理論課程)形式語義和類型論(程序設(shè)計語言理論課程) 各各種語言范型的實現(xiàn)技術(shù)(不涉及)種語言范型的實現(xiàn)技術(shù)(不涉及) 提高軟件質(zhì)量的方法提高軟件質(zhì)量的方法1、程序分析、程序分析2、形式驗證、形式驗證模型檢測:模型檢測:對軟件的數(shù)學(xué)模型進(jìn)行系統(tǒng)地全面考察對軟件的數(shù)學(xué)模型進(jìn)行系統(tǒng)地全面考察程序驗證:程序驗證:用形式方法對軟件進(jìn)行數(shù)學(xué)推理用形

4、式方法對軟件進(jìn)行數(shù)學(xué)推理課課 程程 簡簡 介介 本課程概述本課程概述 學(xué)習(xí)學(xué)習(xí)程序分析和形式驗證的基本原理,它們在高程序分析和形式驗證的基本原理,它們在高可信軟件、代碼優(yōu)化、并行編譯等許多方面有廣可信軟件、代碼優(yōu)化、并行編譯等許多方面有廣泛應(yīng)用泛應(yīng)用 學(xué)習(xí)和討論各類方法解決的問題、采用的技術(shù)、學(xué)習(xí)和討論各類方法解決的問題、采用的技術(shù)、理論特性、算法等,并說明這些方法之間的關(guān)系理論特性、算法等,并說明這些方法之間的關(guān)系和不同。這些方法本身跨越多種程序設(shè)計語言特和不同。這些方法本身跨越多種程序設(shè)計語言特征征課課 程程 簡簡 介(程序分析原理)介(程序分析原理) 什么是程序分析什么是程序分析 一種靜

5、態(tài)(如編譯時)的技術(shù),用于預(yù)測程序運一種靜態(tài)(如編譯時)的技術(shù),用于預(yù)測程序運行時動態(tài)布局或行為的一種安全(忠實于語義)行時動態(tài)布局或行為的一種安全(忠實于語義)且有效(所需時空少)的近似且有效(所需時空少)的近似 程序分析的應(yīng)用程序分析的應(yīng)用 編譯時的代碼優(yōu)化,以避免冗余計算編譯時的代碼優(yōu)化,以避免冗余計算公共子表達(dá)式刪除、無用賦值刪除、循環(huán)優(yōu)化公共子表達(dá)式刪除、無用賦值刪除、循環(huán)優(yōu)化 一些靜態(tài)分析工具,用于分析所關(guān)心的程序性質(zhì)一些靜態(tài)分析工具,用于分析所關(guān)心的程序性質(zhì)程序切片工具、安全性程序切片工具、安全性 程序驗證程序驗證課課 程程 簡簡 介(程序分析原理)介(程序分析原理) 集中在四種

6、主要程序分析方式上集中在四種主要程序分析方式上 數(shù)據(jù)流分析數(shù)據(jù)流分析(data flow analysis) 基于約束的分析基于約束的分析(constraint based analysis) 抽象解釋抽象解釋(abstract interpretation) 類型和結(jié)果系統(tǒng)類型和結(jié)果系統(tǒng)(type and effect system) 對每種方式對每種方式 描述主要原理,而不是技術(shù)的詳細(xì)介紹描述主要原理,而不是技術(shù)的詳細(xì)介紹 怎樣用到更復(fù)雜編程語言的分析怎樣用到更復(fù)雜編程語言的分析課課 程程 簡簡 介(模型檢測)介(模型檢測) 什么是模型檢測什么是模型檢測 驗證系統(tǒng)驗證系統(tǒng)滿足性質(zhì)滿足性質(zhì)

7、( )的方法。它操)的方法。它操作在系統(tǒng)的模型作在系統(tǒng)的模型 (語義)上,而不是在系統(tǒng)的(語義)上,而不是在系統(tǒng)的描述(語法)上描述(語法)上 模型檢測的應(yīng)用模型檢測的應(yīng)用 常用于硬件和通信協(xié)議的驗證中常用于硬件和通信協(xié)議的驗證中 模型檢測方法已經(jīng)在工業(yè)界逐步得到應(yīng)用模型檢測方法已經(jīng)在工業(yè)界逐步得到應(yīng)用,并且并且有一些較好的工具有一些較好的工具課課 程程 簡簡 介(模型檢測)介(模型檢測) 集中在采用下面兩種邏輯的方法上集中在采用下面兩種邏輯的方法上 線性時態(tài)邏輯:時間是線性的邏輯線性時態(tài)邏輯:時間是線性的邏輯 計算樹邏輯:時間可以分支的邏輯計算樹邏輯:時間可以分支的邏輯(時態(tài)邏輯:公式的真假

8、不是靜態(tài)的)(時態(tài)邏輯:公式的真假不是靜態(tài)的) 模型檢測的大體步驟模型檢測的大體步驟 由用戶描述的一個模型開始由用戶描述的一個模型開始 判斷用戶所斷言的假設(shè)在模型中是否有效判斷用戶所斷言的假設(shè)在模型中是否有效 若無效,則產(chǎn)生由執(zhí)行軌跡構(gòu)成的反例若無效,則產(chǎn)生由執(zhí)行軌跡構(gòu)成的反例課課 程程 簡簡 介(程序驗證)介(程序驗證) 什么是程序驗證什么是程序驗證 將基于邏輯證明的方法用于程序性質(zhì)的證明將基于邏輯證明的方法用于程序性質(zhì)的證明1、系統(tǒng)的描述是適當(dāng)邏輯中的一組公式、系統(tǒng)的描述是適當(dāng)邏輯中的一組公式 2、待證性質(zhì)的規(guī)范是另一個公式、待證性質(zhì)的規(guī)范是另一個公式 3、驗證就是通過該邏輯來證明、驗證就

9、是通過該邏輯來證明 程序驗證的應(yīng)用程序驗證的應(yīng)用 對安全攸關(guān)的程序,驗證所關(guān)心的性質(zhì)對安全攸關(guān)的程序,驗證所關(guān)心的性質(zhì) 軟件的機械驗證將改進(jìn)軟件的生產(chǎn)率、效率、軟件的機械驗證將改進(jìn)軟件的生產(chǎn)率、效率、reliability課課 程程 簡簡 介(程序驗證)介(程序驗證) 程序驗證的大體步驟程序驗證的大體步驟 程序員提供附加了適當(dāng)斷言的程序程序員提供附加了適當(dāng)斷言的程序 驗證條件生成器為該程序產(chǎn)生驗證條件驗證條件生成器為該程序產(chǎn)生驗證條件 定理證明器完成驗證條件的證明定理證明器完成驗證條件的證明 涉及機械驗證過程的各主要部分涉及機械驗證過程的各主要部分 Hoare邏輯(公理語義)、最弱前條件演算邏

10、輯(公理語義)、最弱前條件演算 從程序到定理從程序到定理 驗證條件生成驗證條件生成 從定理到證明從定理到證明 自動定理證明自動定理證明課課 程程 簡簡 介介教材和參考書教材和參考書 F. Nielson, H. R. Nielson, and C. Hankin, Principles of Program Analysis, 2nd edition, Springer, 2005 A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools , 2nd edition, Addison-Wesley, 2007 M. Huth

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

最新文檔

評論

0/150

提交評論