【正文】 循環(huán)不變性： a[0]到 a[i1]都小于 38 a[j+1]到 a[14]都大于 38 47 程 序 驗 證 實 例 ? 程序：二分查找 val = 38, i == 6, j == 6, k == 6 i = 0。 j = 14。 while(i = j) { k = i + (j ? i)/2。 if(val = a[k]) j = k ? 1。 if(val = a[k]) i = k + 1。 } if (i – 1 j) 找到 else 沒有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 i j k 觀察點 循環(huán)不變性： a[0]到 a[i1]都小于 38 a[j+1]到 a[14]都大于 38 48 程 序 驗 證 實 例 ? 程序：二分查找 val = 38, i == 6, j == 5, k == 6 i = 0。 j = 14。 while(i = j) { k = i + (j ? i)/2。 if(val = a[k]) j = k ? 1。 if(val = a[k]) i = k + 1。 } if (i – 1 j) 找到 else 沒有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 i j k 條件不成立 49 程 序 驗 證 實 例 ? 程序：二分查找 val = 37, i == 4, j == 6, k == 5 （若 val改成 37） i = 0。 j = 14。 while(i = j) { k = i + (j ? i)/2。 if(val = a[k]) j = k ? 1。 if(val = a[k]) i = k + 1。 } if (i – 1 j) 找到 else 沒有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 i j k 觀察點 循環(huán)不變性： a[0]到 a[i1]都小于 38 a[j+1]到 a[14]都大于 38 50 程 序 驗 證 實 例 ? 程序：二分查找 val = 37, i == 6, j == 4, k == 5 （若 val改成 37） i = 0。 j = 14。 while(i = j) { k = i + (j ? i)/2。 if(val = a[k]) j = k ? 1。 if(val = a[k]) i = k + 1。 } if (i – 1 j) 找到 else 沒有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 j i k 條件不成立 51 程 序 驗 證 實 例 ? 程序：二分查找的主要程序段和斷言 int i, j, k, val, a[m]。 //此前有 define m 15 {m == 15 ? (?n:[0..m?2].a[n] a[n+1]) ? i == 0 ? j == m?1} while(i = j) { {m==15 ?(?n:[0..m?2].a[n] a[n+1])? 0 ? i ? m ? ?1 ? j ? m?1 ? (j?i ? ?1?(?n:[j+1..m?1]. val a[n])? (?n:[0..i?1]. val a[n]) ? j?i == ?2 ? k == i?1 ? val == a[k] )} //循環(huán)不變式 , 含黃色部分 k = i + (j ? i)/2。 if(val = a[k]) j = k ? 1。 if(val = a[k]) i = k + 1。 } {m == 15 ? (?n:[0..m?2].a[n] a[n+1]) ? (i?j == 2 ? k == i?1 ? val == a[k] ? i?j == 1 ? ?n:[0..m?1]. val != a[n]) } 52 程 序 驗 證 實 例 ? 正在開發(fā)的程序驗證系統(tǒng)的 驗證實例 – 數(shù)組 快速排序、冒泡排序、二分查找、二叉堆、矩陣乘、矩陣分塊乘等 – 易變數(shù)據(jù)結構 下面這些數(shù)據(jù)類型的插入函數(shù)和刪除函數(shù)等 單鏈表、循環(huán)單鏈表 雙向變量、循環(huán)雙向鏈表 二叉排序樹、平衡樹 (AVL tree)、 AA 樹、樹堆 (treap)、伸展樹 (splay tree) – 演示二分查找的例子 53 程 序 驗 證 實 例 ? 正在開發(fā)的程序驗證系統(tǒng)的 驗證實例 – 驗證二分查找需用到的引理 lemma 1: ? int m. ? int b[m]. ? int value. ? int k. (? int n: [0..m2]. b[n] b[n+1]) ? value b[k] ? 0 = k m ? (? int n: [0..k]. value b[n]) lemma 2: ? int m. ? int b[m]. ? int value. ? int k. (? int n: [0..m2]. b[n] b[n+1]) ? value b[k] ? 0 = k m ? (? int n: [k..m1]. value b[n]) – 自動定理證明器發(fā)現(xiàn)不了這樣的歸納性質 54 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 k 小 結 ? 本講座小結 – 介紹怎樣從 Hoare邏輯得到對應的演算 ， 最終得到自動證明程序是否具備所期望性質的一種方法 ? 程序驗證的應用情況例舉 – 空客公司在 A400M軍用航空器以及 A380和 A350商用航空器的開發(fā)上，已經(jīng)用形式證明取代了部分安全攸關嵌入式軟件的測試 – 達索航空公司在健壯性的形式驗證方面，有約15%的斷言是用演繹驗證方式證明的 – 工具 VeriFast完成 4個工業(yè)應用案例 的 安全性驗證 ? 相關課程： 程序設計語言基礎、程序設計語言理論 55 小 結 ? 研究方向 – 提高斷言語言的表達能力 – 提高自動定理證明器的證明能力 ? 工具 – 實驗室： Dafny、 Spec、 Ynot和 Why3等 – 工業(yè)界開始應用的有 Caveat、 FramaC和 SPARK2022 56 小 結 ? 參考文獻 – 何偉等譯 ， 面向計算機科學的數(shù)理邏輯 ， 2022. – Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification – Yannick Moy, etc. Testing or Formal Verification: DO178C Alternatives and Industrial Experience. IEEE Software, 30(3):5057, 2022. – 本次講座的基礎知識部分來自上面第 1篇參考文獻 5