第5章命令式程序的語(yǔ)義-資料下載頁(yè)
2025-07-20 11:28本頁(yè)面
【正文】 F ? F | ?F | ?locx. F | ?| ? – 一些縮寫 M ? N ? ? (M = N) F1 ? F2 ? ? (?F1 ? ?F2) F1 ? F2 ? ?F1 ? F2 ? ? ? (?bx.?F) 對(duì)于 b? {bool, val, loc} Kernel程序的前后斷言 ? 對(duì)模型 A來(lái)說(shuō) ， 一階公式的 可滿足性 可以歸納定義如下 ： – ?, s ? M = N當(dāng)且僅當(dāng) ?M?? s = ?N?? s – ?, s ? F1 ? F2當(dāng)且僅當(dāng) ?, s ? F1 并且 ?, s ? F2 – ?, s ? ? F當(dāng)且僅當(dāng)不是 ?, s ? F – ?, s ? ? a ? Ab， ?[x?a], s ? F V V Kernel程序的前后斷言 ? 部分正確性 (1) 在環(huán)境 ?和狀態(tài) s ??state下 ， 如果下面的蘊(yùn)涵 若 ?, s ? F且 ?P ?? s = ?s??， 則 ?, s? ? G 成立 ， 就說(shuō)部分正確性斷言 {F} P {G} 在環(huán)境 ?和狀態(tài) s??state下可滿足 (2) 如果 ?P ?? s = ?state， 則認(rèn)為 {F} P {G}在 s上也得到滿足 (3) 如果在任何環(huán)境 ?和狀態(tài) s ? ?state下 ， 部分正確性斷言 {F} P {G}都可滿足 ， 則說(shuō) {F} P {G}是可滿足的 (4) {F} P {G}可滿足不代表程序執(zhí)行一定終止 CC Kernel程序的前后斷言 證明規(guī)則 ? 邏輯推論規(guī)則 (conseq) ? 順序推理規(guī)則 (seq) ? 條件推理規(guī)則 (cond) {F}P{G} F ?? F G ? G ? {F ?}P{G ?} {F}P1{G} {G}P2{H} {F} P1。 P2 {H} {F ? B}P1{G} {F ? ?B}P2{G} {F} if B then P1 else P2 {G} Kernel程序的前后斷言 ? 賦值公理 (asg) {[M?cont x]F} x := M {F} 在賦值 x := M后對(duì) cont x為真的東西 ， 在賦值前必定 已對(duì) M為真 ? 例 – {y ? z} x := y {cont x ? z} – {cont w ? z} x := cont w {cont x ? z} – {y?cont v} x := y {cont x?cont v} // 假定沒(méi)有別名 ? 賦值公理為什么不是正向的 {F} x := y {[(cont x)/y]F} Kernel程序的前后斷言 ? while規(guī)則 (while) F叫做循環(huán)不變式 {F ? B} P {F} {F} while B do P od {F ? ?B} Kernel程序的前后斷言 ? 例 考慮下面計(jì)算 x y的簡(jiǎn)單程序 ， 假定 y ? x d := 0。 —P0 while (cont d ) + y x do —B d := (cont d ) + 1。 —P1 od 證明 {y ? x} P0。 while B do P1 od {(cont d) + y = x} Kernel程序的前后斷言 d := 0。 while (cont d ) + y x do —B d := (cont d ) + 1。 od (a) {y ? x} d := 0 {(cont d ) + y ? x} (b) {((cont d)+y ? x) ? B}d:=(cont d) +1{(cont d)+y ? x} (cont d) + y ? x) ? B ? (cont d ) + y x {(cont d) + y x} d:=(cont d) + 1{(cont d) + y ? x} (cont d)+y ? x是循環(huán)不變式 (c) ((cont d) + y ? x) ? ?B ? (cont d) + y = x Kernel程序的前后斷言 可靠性 ? 使用程序的指稱語(yǔ)義來(lái)證明可靠性 – 斷言語(yǔ)言的證明系統(tǒng)對(duì)指稱模型可靠 斷言語(yǔ)言上的證明系統(tǒng)用的就是經(jīng)典邏輯的公理和推理規(guī)則 ， 它們的可靠性證明比較簡(jiǎn)單 – Hoare邏輯的公理和推理規(guī)則對(duì)指稱模型可靠 Kernel程序的前后斷言 可靠性 ? 使用程序的指稱語(yǔ)義來(lái)證明可靠性 ? 定理 假定部分正確性規(guī)范 ?F?P?G?可證 ， 那么 ?F?P ?G?在模型 A?中有效 – 只要 證明該公理語(yǔ)義中的公理和推理規(guī)則對(duì)模型A?中都可靠就可以了 習(xí) 題 第一次： ， , (a), (b), (c)
環(huán)評(píng)公示相關(guān)推薦
鄂ICP備17016276號(hào)-1