第7章程序驗證-全文預(yù)覽
【正文】 – 我們構(gòu)造一個驗證條件 VC(C, Q) 循環(huán)需要有循環(huán)不變式標(biāo)注 VC要強于 WP 但仍然要弱于 P， P ? VC(C, Q) ? WP(C, Q) false true ? 強 弱 Pre(C, Q) 最弱前條件 WP(C, Q) P 驗證條件 VC(C, Q) 驗證條件生成 ? 驗證條件 – 循環(huán)不變式很難寫出 , 考慮源于 QuickSort的代碼 int partition(int *a, int L0, int H0, int pivot) { int L = L0, H = H0。 { (x == m?y) ? (y = n) } while y n do { { (x+m == m?(y+1)) ? ((y+1) = n) } x = x + m 。 x = x ? 1。 y = 1。 y = a。 y = 1。 while (z != x) { z = z +1。第 7章 程序驗證 內(nèi)容概述 ? 程序邏輯：描述和論證程序行為的邏輯 – Hoare邏輯 – Dijkstra最弱前條件演算 ? 從程序到定理 – 驗證條件生成 ? 從定理到證明 – 定理證明器 – 判定過程 ? 循環(huán)不變式的推斷 ? 以 Gee C. Necula教授的講稿為主來介紹 程 序 邏 輯 ? Hoare邏輯 – 良形公式 （ wellformed formula） 的形式為 { P } C { Q } – C是程序片段 需要介紹編程語言 – P 和 Q是斷言 需要介紹斷言及推理規(guī)則 – { P } C { Q }稱為程序規(guī)范 需要介紹規(guī)范語言及推理規(guī)則 – Hoare邏輯也稱為語言的一種公理語義 作為例子的核心編程語言 ? 語法 – 整數(shù)表達式 E ::= n | x | ?E | E + E | E ? E | E ? E | ( E ) – 布爾表達式 B ::= true | false | !B | B amp。 z = 0。記作 ? ?tot { P } C { Q } – 通常建議用部分正確性證明＋終止性證明來得到完全正確性證明 Hoare邏輯 ? 例 1 Succ ? 例 2 Fac1 { ? } { x = 0 } a = x + 1。 while ( z != x ) { } else { z = z + 1。 { x = 0 ? x == x0 } z = 0。 y = y ? z。 { (x == m?0) ? (0 = n) } y = 0 。C2 , Q) = WP (C1, WP(C2, Q)) – WP(if B {C1} else {C2}, Q) = (B ? WP(C1, Q)) ? (?B ? WP(C2, Q)) { Q[E/x] } x = E { Q } { P } C1 { R } { R } C2 { Q } { P } C1。 if(L H) { swap a[L] and a[H] } } return L } // 僅考慮內(nèi)存安全，外循環(huán)的不變式是什么？ – 循環(huán)不變式的自動生成是尚未解決的問題 驗證條件生成 ? 驗證條件生成 – VC的計算方式類似于 WP的計算 – 只有 while語句例外 VC(while B {C }, Q ) = I ? (
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1