第7章程序驗(yàn)證(存儲(chǔ)版)
【正文】 – { 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。 y = 1。 y = 1。 { (x == m?y) ? (y = n) } while y n do { { (x+m == m?(y+1)) ? ((y+1) = n) } x = x + m 。 y = 0 。 y = 0 。 y = 0 。 y = 0 。 (x = m?0) ? (0 ? n) y = 0 。 y = 0 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 y = y + 1 。 y = y + 1 。 while(a[H] pivot) H 。 C2 { Q } { P ? B } C1 { Q } { P ? ?B } C2 { Q } { P } if B {C1} else {C2} { Q } { I ? B } C { I } { I } while B {C } {I ? ?B} Hoare邏輯 ? 部分正確性的證明規(guī)則 – 推論規(guī)則 ?AR P?? P 表示 P?? P在謂詞邏輯的自然演繹演 算中可以證明 ?AR P?? P { P } C { Q } ?AR Q ? Q? { P? } C { Q? } Hoare邏輯 n = 0 function mult(m, n) { { (0 == m?0) ? (0 = n) } x = 0 。 } } { y == x + 1 } { y == x ! } Hoare邏輯 ? 例 2 Fac1 ? 例 3 Fac2 { x = 0 } x0是輔助的邏輯變量 y = 1。記作 ? ?par { P } C { Q } – 完全正確性 在滿足 P的任何狀態(tài)下執(zhí)行 C，則 C一定 終止并且結(jié)果狀態(tài)一定滿足 Q。 B | B || B | E E | ( B ) – 命令 C ::= x = E | C 。 if (a 1 == 0 ) { z = 0。 while ( z != x ) { while ( x != 0 ) { z = z + 1。 { (x == m?(y+1)) ? ((y+1) = n) } y = y + 1 。 while y n do { x = x + m 。 while y n do { (x = m?y) ? (y ? n) // 循環(huán)不變式 x = x + m 。 while y n do { (x = m?y) ? (y ? n) x = x + m 。 ((x = m?y) ? (y ? n)) ? (y n) ? (x+m = m?(y+1)) ? ((y+1) ? n)
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號(hào)-1