《对程序进行推理的逻辑计算机科学导论第二讲教学课件.ppt》由会员分享，可在线阅读，更多相关《对程序进行推理的逻辑计算机科学导论第二讲教学课件.ppt（45页珍藏版）》请在三一文库上搜索。
1、对程序进行推理的逻辑 计算机科学导论第二讲 计算机科学技术学院 陈意云 0551-63607043 课 程 内 容 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比 较模型的表达能力 2. 程序理论关心的问题 给定模型M，如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 讲 座 提 纲 基本知识 程序验证、程序逻辑、命题逻辑、谓词逻辑 Hoare逻辑 Hoare三元式、赋值公理、结
2、构化语句的推理规则 、推论规则 生成验证条件的演算 最弱前条件演算、生成验证条件的演算 程序验证实例演示 二分查找等程序 基 本 知 识 程序测试测试 与程序验证验证 测试测试 能发现发现 程序有错错；一般而言，测试测试 不能保 证证程序无错错 程序验证：用数学的方法来证明程序的性质，提 高软件可信程度 演绎验证：指用逻辑推理的方法来证明程序具备 所期望的性质 演绎验证可以保证程序无错 程序逻辑逻辑 ：对对程序进进行推理的逻辑逻辑 基 本 知 识 命题逻辑 合式公式（well-formed formula）的归纳定义 := p | ( ) | ( ) | ( ) | ( ) (1) p代表原子
3、命题题，例如 x 3, a5 = 10.5 原子命题题具体形式与讨论讨论 的问题领问题领 域有关 (2) 代表一般命题题，“:=”右部用“| ”分隔的各部 分代表命题题的构成形式，如 0 1 y 0 y 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不成立 Hoare 逻 辑 结结构化语语句的推理规则规则 顺顺序语语句 条件语语句（也可用其
4、它形式表示） 插曲：推论规则论规则 P P P S Q Q Q P S Q P E S1 Q P E S2 Q P if E then S1 else S2 Q P S1 R R S2 Q P S1; S2 Q Hoare 逻 辑 例（用Hoare逻辑手中证明简单程序段） 证：true if (x y) z = x else z = y z = x z = y (1)由赋值公理:x = x x =yz = xz = x z =y (2) 由(1)的所得、(true x y) (x = x x = y) 和推论规则，可得： true x y z = x z = x z = y (3) 同理得:
5、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 由条件语句 的规则 Hoare 逻 辑 结结构化语语句的推理规则规则 （续续） 循环语环语 句 例：用自然数加法来完成自然数相乘 x = 0; y = 0; while (y = ak) i = k + 1; if (i 1 j) 找到 else 没有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 ijk
6、观察点 程 序 验 证 实 例 程序：二分查找 val = 38, i = 0, j = 6, k = 3 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 ijk 观察点 程 序 验 证 实 例 程序：二分查找 val = 38, i = 4, j = 6, k = 5 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到 10 15 21 28 32
7、37 44 49 53 57 62 67 71 77 83 ijk 观察点 程 序 验 证 实 例 程序：二分查找 val = 38, i = 6, j = 6, k = 6 i = 0; j = 14; while(i = ak) 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 观察点 程 序 验 证 实 例 程序：二分查找 val = 38, i = 6, j = 5, k = 6 i = 0; j = 14; while(i = ak) i = k + 1; if
8、(i 1 j) 找到 else 没有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 ij k 观察点 程 序 验 证 实 例 程序：二分查找 val = 37, i = 4, j = 6, k = 5 （若val改成37） i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 ijk 观察点 程 序 验 证 实 例 程序：二分查找 val = 37, i = 6, j = 4, k =
9、 5 （若val改成37） i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到 10 15 21 28 32 37 44 49 53 57 62 67 71 77 83 jik 观察点 程 序 验 证 实 例 程序：二分查找的主要程序段和断言 int i, j, k, val, am; /此前有#define m = 15 m = 15 n:0m2.an an ji = 2 k = i1 val = ak ) /循环不变式 k = i + (j i)/2;/包括黄色部分 if(val = ak) i = k + 1;
10、m = 15 n:0m2.an an+1 (ij = 2 k = i1 val = ak ij = 1 n:0m1. val != an) 程 序 验 证 实 例 原型系统验证实例 一维数组 快速排序程序、冒泡排序、二分查找、二叉堆等 易变数据结构 下面这些数据类型的插入函数和删除函数等 1、单链表、循环单链表 2、双向变量、循环双向链表 3、二叉排序树、平衡树(AVL tree)、 AA 树、树 堆(treap)、伸展树(splay tree) 原型系统网址 http:/ 小 结 本讲座小结 介绍绍怎样样从Hoare逻辑逻辑 得到一种对应对应 的演算，最 终终得到自动证动证 明程序是否具备备
11、所期望性质质的一种 方法 程序验证的应用情况例举 空客公司在A400M军用航空器以及A380和A350商 用航空器的开发上，已经用形式证明取代了部分 安全攸关嵌入式软件的测试 达索航空公司在健壮性的形式验证方面，有约 15%的断言是用演绎验证方式证明的 相关课程：程序设计语言基础、程序设计语言理论 小 结 研究方向 提高断言语言的表达能力 提高自动定理证明器的证明能力 工具 实验室：ESC/Java、Spec#、Ynot和Why3等 工业界开始应用的有Caveat、 Frama-C和SPARK 参考文献 何伟等译，面向计算机科学的数理逻辑，2007. Yannick Moy, etc. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Software, 30(3):50-57, 2013.