第7章程序驗(yàn)證-展示頁(yè)
2024-09-13 09:06本頁(yè)面
【正文】 jkstra最弱前條件演算 ? 從程序到定理 – 驗(yàn)證條件生成 ? 從定理到證明 – 定理證明器 – 判定過(guò)程 ? 循環(huán)不變式的推斷 ? 以 Gee C. Necula教授的講稿為主來(lái)介紹 程 序 邏 輯 ? Hoare邏輯 – 良形公式 （ wellformed formula） 的形式為 { P } C { Q } – C是程序片段 需要介紹編程語(yǔ)言 – P 和 Q是斷言 需要介紹斷言及推理規(guī)則 – { P } C { Q }稱為程序規(guī)范 需要介紹規(guī)范語(yǔ)言及推理規(guī)則 – Hoare邏輯也稱為語(yǔ)言的一種公理語(yǔ)義 作為例子的核心編程語(yǔ)言 ? 語(yǔ)法 – 整數(shù)表達(dá)式 E ::= n | x | ?E | E + E | E ? E | E ? E | ( E ) – 布爾表達(dá)式 B ::= true | false | !B | B amp。 B | B || B | E E | ( B ) – 命令 C ::= x = E | C 。 z = 0。 y = y ? z } Hoare邏輯 ? 斷言語(yǔ)言 – 用來(lái)描述程序變量滿足的性質(zhì)，如 x==5, x+y 30 – 通常，斷言 P, Q的語(yǔ)法同編程語(yǔ)言布爾表達(dá)式的語(yǔ)法有些區(qū)別：如可以出現(xiàn)量詞 ? Hoare邏輯的良形公式 – { P } C { Q } – C是一段程序， P和 Q分別是 C的前條件和后條件 – 例如 { x == 5 } x = x + 1 { x == 6 } Hoare邏輯 ? Hoare邏輯良形公式 { P } C { Q }的解釋 – 部分正確性 在滿足 P的任何狀態(tài)下執(zhí)行 C，若 C終止則結(jié)果狀態(tài)一定滿足 Q。記作 ? ?tot { P } C { Q } – 通常建議用部分正確性證明＋終止性證明來(lái)得到完全正確性證明 Hoare邏輯 ? 例 1 Succ ? 例 2 Fac1 { ? } { x = 0 } a = x + 1。 if (a 1 == 0 ) { z = 0。 while ( z != x ) { } else { z = z + 1。 y = y ? z。 { x = 0 ? x == x0 } z = 0。 while ( z != x ) { while ( x != 0 ) { z = z + 1。 y = y ? z。 } } { y == x ! } { y == x0 ! } Hoare邏輯 ? 部分正確性的證明規(guī)則 – 賦值公理 賦值公理的實(shí)例 – { 2 == 2 } x = 2 { x == 2 } – { 2 == 4 } x = 2 { x == 4 } – { 2 == y } x = 2 { x == y } – { 2 0 } x = 2 { x 0 } – { x + 1 + 5 == y } x = x + 1 { x + 5 ==y } – { x + 1 0 ? y 0 } x = x + 1 { x 0 ? y 0 } { Q[E/x] } x = E { Q } Hoare邏輯 ? 部分正確性的證明規(guī)則 – 賦值公理 – 復(fù)合規(guī)則 – 條件規(guī)則 – 循環(huán)規(guī)則 { Q[E/x] } x = E { Q } { P } C1 { R } { R } C2 { Q } { P } C1。 { (x == m?0) ? (0 = n
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1