对程序进行推理的逻辑 计算机科学导论第二讲

Presentation on theme: "对程序进行推理的逻辑 计算机科学导论第二讲"— Presentation transcript:

1 对程序进行推理的逻辑 计算机科学导论第二讲
计算机科学技术学院 陈意云

2 课 程 内 容 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题
给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力 2. 程序理论关心的问题 给定模型M，如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 本次讲座讨论怎样用数学方法证明程序是正确的 2

3 讲 座 提 纲 基本知识 Hoare逻辑 生成验证条件的演算 程序验证实例演示 程序验证、程序逻辑、命题逻辑、谓词逻辑
最弱前条件演算、生成验证条件的演算 程序验证实例演示 二分查找程序 3

4 序 曲 近几年软件错误带来危害的事例 2012年，美国KCP金融公司由于电子交易系统出现故障，交易算法出错，导致该公司对150支不同的股票高价购进、低价抛出，直接给公司带来了4.4亿美元的损失，当天股票下跌62% 2013年9月12日，美联航售票网站一度出现问题，售出票面价格为0-10美元的超低价机票，引发抢购。大约15分钟后，美联航发现错误，关闭售票网站并声称正在进行维护。大约两个多小时后，该公司售票网站恢复正常，并且承认已卖出的票有效 4

5 序 曲 软件错误带来危害的事例 据《自然》杂志网站报道，广受世界天文学界期待的日本旗舰级天文卫星“瞳”（Hitomi）于2016年2月17日发射升空，但在大约5周之后便出现翻滚失控迹象。经调查后日本方面宣布，事故原因源自底层软件错误。卫星的控制系统在发现飞行姿态失控时，采取了错误的调整，推进器点火时朝向了错误的反方向，导致自身旋转更加严重，最终彻底失控 5

6 序 曲 软件无处不在 全世界有超过10亿辆汽车在行驶，每辆新汽车上都有20～80个微处理器，有多达3000万行的代码在运行
序 曲 软件无处不在 全世界有超过10亿辆汽车在行驶，每辆新汽车上都有20～80个微处理器，有多达3000万行的代码在运行 全世界每年有多达23亿次手术，在每个现代医疗设备上往往会有超过30万行的代码在运行 全世界有超过3000辆高速列车在行驶，每辆列车上会有多达6000万行的代码在运行 全世界有超过300万架飞机，新型飞机上会有多达2000万行代码在运行 如何保证这些代码没有错误？ 6

7 基 本 知 识 程序：在数组a中快速查找某个值 怎样进行测试 int a[m] n:[0..m2].a[n] < a[n+1]
对数组a的长度m (m>0) 的各种情况都要测试吗？ 对a中出现的各个元素都需要测试吗？ 对a中不出现的元素要测多少种情况？ 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 7

8 基 本 知 识 程序测试与程序验证 测试能发现程序有错；一般而言，测试不能保证程序无错
程序验证：用数学的方法来证明程序的性质，提高软件可信程度 演绎验证：指用逻辑推理的方法来证明程序具备所期望的性质 就所期望的性质而言，演绎验证可保证程序无错 程序逻辑：对程序进行推理的逻辑 8

9 基 本 知 识 命题逻辑 程序设计中用到命题逻辑的知识 if (0 <= m && m <100) …
 &&是命题逻辑的二元运算符(下面用而非&&) if (0 < m || 0 < n) …  ||是命题逻辑的二元运算符（下面用而不是 ||） n = 0; while(! n >= 100) { …; n = n + 1;}  !是命题逻辑的一元运算符（下面用而不是 !） 9

10 基 本 知 识 命题逻辑 合式公式（well-formed formula）的归纳定义
 ::= p |   |    |    |    | ( ) (1) p代表原子命题，例如 x > 3, a[5] == 10.5 原子命题具体形式与讨论的问题领域有关 (2)  代表一般命题，“::=”右部用“| ”分隔的各部分代表命题的构成形式，如 0<= x  x <100 (3) , , 和代表合取、析取、非和蕴涵运算，在确定了它们的运算优先关系后，很多情况下括号可以省略，如p  (q1  q2)可简化为p  q1  q2 备注：蕴涵采用而不是 ， 用于描述函数类型 10

11 基 本 知 识 命题逻辑 推理规则 例：有关合取“”运算的推理规则 ( i) (e1) (e2)
“  i”表示合取引入规则（i: introduction） “  e”表示合取消去规则（e: elimination） 对和等也都有各自的推理规则              11

12 基 本 知 识 谓词逻辑 程序设计中用到谓词逻辑的知识 谓词：结果类型为bool的函数
bool even(int m) { //用编程语言写的谓词，与数理 if (m/2 * 2 == m) return true; //逻辑中的有区别 else return false; } if(even(x) && even(y)) … <、<=、==、!= …等关系算符都是谓词 12

13 基 本 知 识 谓词逻辑 合式公式 (1) 谓词集合、函数集合（包括常量） (2) 基于来定义项集
t ::= x | c | f(t, …, t) ( f  ) 例如 a + 5 < b – 3中的a + 5和b – 3 (3) 归纳地定义基于（ ,  ）的合式公式  ::= P(t1, t2, …, tn) |   |    |    |    | x  |  x  | ( ) ( P  ) 增加的规则 全称量词断言和存在量词断言的证明规则等 13

14 Hoare 逻 辑 程序逻辑 对程序进行推理的逻辑 Hoare逻辑是一种程序逻辑
14

15 Hoare 逻 辑 合式公式（well-formed formula） 语法形式：{P} S {Q}，称为Hoare三元式
(2) P和Q是关于程序状态（变量到值的映射）的断言，分别称为S的前断言和后断言，断言是谓词逻辑的合式公式 (3) 例： {x == 1  y < 5} x = x +1 {x == 2  y < 5} {P} S {Q}的含义：在满足P的状态下执行S ，若执行终止，则终止状态满足Q 例：{x == 1  y < 5} x = x +1 {x == 2  y < 5}成立 {x > 1  y < 5} x = x +1 {x > 0  y < 5}也成立 15

16 Hoare 逻 辑 赋值公理 形式：{Q[E/x]} x = E {Q} Q[E/x]表示Q中出现的变量x用表达式E代换
例: {x +1 > 6} x = x +1 {x > 6} 是赋值公理的实例 特点： x +1 > 6 （即x > 5）是语句x = x+1和后断言x > 6 的最弱前断言 (1) x > 5.1和x > 7都可作为前断言，因都强于x > 5 x > 5.1  x > 5 并且x > 7  x > 5 (2) 若x > 4.9作为前断言，则三元式不成立，因为 x > 4.9  x > 5不成立 16

17 Hoare 逻 辑 结构化语句的推理规则 {P} S1 {R} {R} S2 {Q} {P} S1; S2 {Q} 顺序语句
条件语句（也可用其它形式表示） 插曲：推论规则 {P} S1 {R} {R} S2 {Q} {P} S1; S2 {Q} {P  E} S1 {Q} {P  E} S2 {Q} {P} if E then S1 else S2 {Q} P  P {P} S {Q} Q  Q {P} S {Q} 17

18 Hoare 逻 辑 例（用Hoare逻辑手工证明简单程序段）
证: {true} if (x > y) z = x; else z = y; {z >= x  z >= y} (1)由赋值公理:{x >= x  x >=y}z = x{z >= x  z >=y} (2) 由(1)的所得、(true  x > y)  (x >= x  x >= y) 和推论规则，可得： {true  x > y} z = x {z >= x  z >= y} (3) 同理得: {true  (x > y)} z = y {z >= x  z >= y} (4) 得: {true} if (x > y) z = x; else z = y;{z >= x  z >= y} 由条件语句 的规则 {P  E} S1 {Q} {P  E} S2 {Q} {P} if E then S1 else S2 {Q} 18

19 Hoare 逻 辑 结构化语句的推理规则（续） {IE} S {I} {I} while E do S {IE} 循环语句
例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m  n  演算得到语句S和后断言I的最弱前条件： x+m == m(y+1)  y+1 n {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 //循环不变式I：(x == my)  (y  n) 19

20 Hoare 逻 辑 结构化语句的推理规则（续） {IE} S {I} {I} while E do S {IE} 循环语句
例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m  n  演算得到语句S和后断言I的最弱前条件： x+m == m(y+1)  y+1 n {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 //循环不变式I：(x == my)  (y  n) 分两步看，对于y = y + 1 20

21 Hoare 逻 辑 结构化语句的推理规则（续） {IE} S {I} {I} while E do S {IE} 循环语句
例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m  n  演算得到语句S和后断言I的最弱前条件： x+m == m(y+1)  y+1 n {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 //循环不变式I：(x == my)  (y  n) 分两步看，对于x = x + m 21

22 Hoare 逻 辑 结构化语句的推理规则（续） {IE} S {I} {I} while E do S {IE} 循环语句
例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m  n  证明I E 语句S和后断言I的最弱前条件： {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 //循环不变式I：(x == my)  (y  n) 最后一行称为验证条件 (x == my  y n  y< n)  (x+m == m(y+1)  y+1 n) 22

23 Hoare 逻 辑 小结 用Hoare逻辑，可对简单程序进行手工推理证明 手工体现在两方面 (1) 手工用推理规则进行演算或推理
(2) 手工进行验证条件的证明（前例遇到蕴涵式的证明，第一讲对自动定理证明已略有介绍） 虽是证明程序的一种方法，但低效、不能接受 如何走向自动验证（以函数的正确性验证为例） (1) 函数的前条件和后条件必须由验证者给出 (2) 把Hoare逻辑规则改成能自动推演的演算规则 (3) 借助自动定理证明器证明验证条件 23

24 生成验证条件的演算 最弱前条件（Weakest Precondition）演算WP 函数WP : 程序集  断言集  断言集
WP(S, Q)：计算{P} S {Q}的最弱前条件P Hoare逻辑的赋值公理直接是最弱前条件演算的一条规则 (1) 赋值公理：{Q[E/x]} x = E {Q} (2) 赋值语句的WP演算规则： WP (x =E, Q) = Q[E/x] 24

25 生成验证条件的演算 最弱前条件演算WP 若一个函数的前后条件是P和Q，函数的代码是赋值语句序列S1, …, Sn，那么
(1) 逆向从Sn到S1连续使用赋值语句的WP规则， WP(S1, …, WP(Sn, Q)…) 它是保证执行上述代码段后得到Q的最弱前条件 (2) 若P  WP(S1, …, WP(Sn, Q)…)得证，则代码段S1, …, Sn对前后条件P和Q正确 (3) P  WP(S1, …, WP(Sn, Q)…)称为验证条件 强调：P蕴涵最弱前条件即可, 不必要求等于后者 25

26 生成验证条件的演算 最弱前条件演算WP WP(x =E, Q) = Q[E/x] {P} S1 {R} {R} S2 {Q}
{Q[E/x]} x = E {Q} WP(S1;S2, Q) = WP (S1, WP(S2, Q)) WP(if E then S1 else S2, Q) = (WP(S1, Q)  E)  (WP(S2, Q)  E) {P} S1 {R} {R} S2 {Q} {P} S1; S2 {Q} {P  E} S1 {Q} {P  E} S2 {Q} {P } if E then S1 else S2 {Q} 26

27 生成验证条件的演算 最弱前条件演算WP 对于WP (while E do S, Q)，演算有可能不终止 假定WPk为循环体S执行k次的演算
WP0(while E do S, Q) = E  Q WPi (while E do S, Q) = E  WP(S, WPi1(while E do S, Q)) WP(while E do S, Q) = WP0 (…)  WP1 (…)  WP2 (…)  … {IE} S {I} {I} while E do S {IE} WP演算在循环语句 这里遇到了困难 27

28 生成验证条件的演算 最弱前条件演算WP 一些其他规则 Q  Q
(1) WP(S, Q1  Q2) = WP(S, Q1)  WP(S, Q2) (2) WP(S, Q1  Q2) = WP(S, Q1)  WP(S, Q2) (3) (4) WP(S, false) = false (4)和(5)较难理解, 不介绍 (5) WP(S, true) = 保证S终止的最弱前条件 … … …. 下面考虑解决由循环语句引出的问题 Q  Q WP(S, Q)  WP(S, Q) 28

29 生成验证条件的演算 生成验证条件的演算VC(verification condition) (1) 观察P和WP之间的关系
(2) 寻找两者之间的一种称为VC(S, Q)的演算 (3) 即P VC(S, Q)WP(S, Q) (4) VC演算的特点：要求验证者提供循环不变式 true false  Precondition(S, Q) weak strong 验证条件演算结果VC(S, Q) 最弱前条件 WP(S, Q) 验证者提供的前条件P 29

30 生成验证条件的演算 生成验证条件的演算VC(verification condition) 除了循环语句外，VC演算与WP的一致
循环语句的VC演算如下，其中I是循环不变式 VC(while E do S, Q) = I  x1…xn(( I  E  VC(S, I))  (I  E  Q)) 其中x1, …, xn是在S中被修改的所有变量 实际做法 (1) 黄色部分和绿色部分 分别作为循环出口和入口的验证条件 (2) I作为继续逆向VC演算的后断言 {IE} S {I} {I} while E do S {IE} 30

31 程 序 验 证 实 例 例子：用加运算来实现乘运算的函数 void mult(int m, int n) { x = 0 ; y = 0 ;
while (y < n) do { x = x + m ; y = y + 1 ; } 例子：用加运算来实现乘运算的函数

32 程 序 验 证 实 例 由程序员提供 由程序员提供 n  0 // 前条件 void mult(int m, int n) {
x = 0 ; y = 0 ; while (y < n) do { x = x + m ; y = y + 1 ; } } x == m  n // 后条件 由程序员提供 由程序员提供

33 程 序 验 证 实 例 也由程序员提供 n  0 void mult(int m, int n) { x = 0 ; y = 0 ;
while (y < n) do { (x == my)  (y  n) // 循环不变式 x = x + m ; y = y + 1 ; } } x == m  n 也由程序员提供

34 程 序 验 证 实 例 函数前后条件、循环不变式 都称为断言 它们看上去像编程语言的布 尔表达式 n  0
void mult(int m, int n) { x = 0 ; y = 0 ; while (y < n) do { (x == my)  (y  n) // 循环不变式 x = x + m ; y = y + 1 ; } } x == m  n 函数前后条件、循环不变式 都称为断言 它们看上去像编程语言的布 尔表达式

35 程 序 验 证 实 例 n  0 void mult(int m, int n) { x = 0 ; y = 0 ;
while (y < n) do { (x == my)  (y  n) x = x + m ; y = y + 1 ; } ((x == my)  (y  n))  (y < n) // 循环结束程序点的断言 } x == m  n I  E

36 程 序 验 证 实 例 第1个验证条件 n  0 void mult(int m, int n) { x = 0 ; y = 0 ;
while (y < n) do { (x == my)  (y  n) x = x + m ; y = y + 1 ; } ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n I  E  Q（Q是函数后条件） 第1个验证条件

37 程 序 验 证 实 例 通过最弱前条件演算得到 n  0 void mult(int m, int n) { x = 0 ;
y = 0 ; while (y < n) do { (x == my)  (y  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n 通过最弱前条件演算得到

38 程 序 验 证 实 例 n  0 void mult(int m, int n) { x = 0 ; y = 0 ;
while (y < n) do { (x == my)  (y  n) (x+m == m(y+1))  ((y+1)  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n

39 程 序 验 证 实 例 第2个验证条件 n  0 void mult(int m, int n) { x = 0 ;
y = 0 ; I  E  VC(S, I)（S是循环体） ((x ==my)  (y  n))  (y < n)  (x+m ==m(y+1))  ((y+1)  n) while (y < n) do { (x == my)  (y  n) (x+m == m(y+1))  ((y+1)  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n 第2个验证条件

40 程 序 验 证 实 例 n  0 void mult(int m, int n) { x = 0 ;
(x == m0)  (0  n) y = 0 ; ((x ==my)  (y  n))  (y < n)  (x+m ==m(y+1))  ((y+1)  n) while (y < n) do { (x == my)  (y  n) (x+m == m(y+1))  ((y+1)  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n

41 程 序 验 证 实 例 n  0 void mult(int m, int n) { (0 == m0)  (0  n)
x = 0 ; (x == m0)  (0  n) y = 0 ; ((x ==my)  (y  n))  (y < n)  (x+m ==m(y+1))  ((y+1)  n) while (y < n) do { (x == my)  (y  n) (x+m == m(y+1))  ((y+1)  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n

42 程 序 验 证 实 例 第3个验证条件 n  0 P  VC(S, I)
void mult(int m, int n) { ( n  0 )  ((0 == m0)  (0  n)) (0 == m0)  (0  n) x = 0 ; (x == m0)  (0  n) y = 0 ; ((x ==my)  (y  n))  (y < n)  (x+m ==m(y+1))  ((y+1)  n) while (y < n) do { (x == my)  (y  n) (x+m == m(y+1))  ((y+1)  n) x = x + m ; (x == m(y+1))  ((y+1)  n) y = y + 1 ; } (x == my)  (y  n) ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n P是函数前条件，S是循环之前的语句序列 第3个验证条件

43 程 序 验 证 实 例 由自动定理证明器完成验证条件的证明 n  0
void mult(int m, int n) { ( n  0 )  ((0 == m0)  (0  n)) x = 0 ; y = 0 ; ((x ==my)  (y  n))  (y < n)  (x+m ==m(y+1))  ((y+1)  n) while (y < n) do { (x == my)  (y  n) x = x + m ; y = y + 1 ; } ((x == my)  (y  n))  (y < n)  (x == mn) } x == m  n 由自动定理证明器完成验证条件的证明

44 程 序 验 证 实 例 程序：二分查找 #define m 15 int a[m] n:[0..m2].a[n] < a[n+1]
10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 44

45 程 序 验 证 实 例 程序：二分查找 val = 38, i == 0, j == 14, k == 7 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 k j 观察点 45

46 程 序 验 证 实 例 程序：二分查找 val = 38, i == 0, j == 6, k == 3 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 k j 观察点 46

47 程 序 验 证 实 例 程序：二分查找 val = 38, i == 4, j == 6, k == 5 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 k j 循环不变性： a[0]到a[i-1]都小于38 a[j+1]到a[14]都大于38 观察点 47

48 程 序 验 证 实 例 程序：二分查找 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 j i 循环不变性： a[0]到a[i-1]都小于38 a[j+1]到a[14]都大于38 k 观察点 48

49 程 序 验 证 实 例 程序：二分查找 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 j i k 条件不成立 49

50 程 序 验 证 实 例 程序：二分查找 val = 37, i == 4, j == 6, k == 5 （若val改成37）
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 k j 循环不变性： a[0]到a[i-1]都小于38 a[j+1]到a[14]都大于38 观察点 50

51 程 序 验 证 实 例 程序：二分查找 val = 37, i == 6, j == 4, k == 5 （若val改成37）
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 k i 条件不成立 51

52 程 序 验 证 实 例 程序：二分查找的主要程序段和断言 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] )} //循环不变式, 含黄色部分 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

53 程 序 验 证 实 例 正在开发的程序验证系统的验证实例 数组 快速排序、冒泡排序、二分查找、二叉堆、矩阵乘、矩阵分块乘等 易变数据结构
下面这些数据类型的插入函数和删除函数等 1、单链表、循环单链表 2、双向变量、循环双向链表 3、二叉排序树、平衡树(AVL tree)、 AA 树、树堆(treap)、伸展树(splay tree) 演示二分查找的例子 53

54 程 序 验 证 实 例 正在开发的程序验证系统的验证实例  ( int n: [0..k]. value > b[n])
验证二分查找需用到的引理 lemma 1:  int m.  int b[m].  int value.  int k. ( int n: [0..m-2]. 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: [k+1..m-1]. value < b[n]) 自动定理证明器发现不了这样的归纳性质 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 k 54

55 小 结 本讲座小结 程序验证的应用情况例举 相关课程：程序设计语言基础、程序设计语言理论
小 结 本讲座小结 介绍怎样从Hoare逻辑得到对应的演算，最终得到自动证明程序是否具备所期望性质的一种方法 程序验证的应用情况例举 空客公司在A400M军用航空器以及A380和A350商用航空器的开发上，已经用形式证明取代了部分安全攸关嵌入式软件的测试 达索航空公司在健壮性的形式验证方面，有约15%的断言是用演绎验证方式证明的 工具VeriFast完成4个工业应用案例的安全性验证 相关课程：程序设计语言基础、程序设计语言理论 55

56 小 结 研究方向 工具 提高断言语言的表达能力 提高自动定理证明器的证明能力 实验室：Dafny、Spec#、Ynot和Why3等
小 结 研究方向 提高断言语言的表达能力 提高自动定理证明器的证明能力 工具 实验室：Dafny、Spec#、Ynot和Why3等 工业界开始应用的有Caveat、 Frama-C和 SPARK2014 56

57 小 结 参考文献 何伟等译，面向计算机科学的数理逻辑，2007.
小 结 参考文献 何伟等译，面向计算机科学的数理逻辑，2007. Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to Verification Yannick Moy, etc. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Software, 30(3):50-57, 2013. 本次讲座的基础知识部分来自上面第1篇参考文献 57