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

对程序进行推理的逻辑 计算机科学导论第二讲,计算机科学技术学院 陈意云 0551-63607043 yiyunustc.edu.cn,课 程 内 容,课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力 2. 程序理论关心的问题 给定模型M，如何用模型M解决问题 包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源,讲 座 提 纲,基本知识 程序验证、程序逻辑、命题逻辑、谓词逻辑 Hoare逻辑 Hoare三元式、赋值公理、结构化语句的推理规则、推论规则 生成验证条件的演算 最弱前条件演算、生成验证条件的演算 程序验证实例演示 二分查找等程序,基 本 知 识,程序测试与程序验证 测试能发现程序有错；一般而言，测试不能保证程序无错 程序验证：用数学的方法来证明程序的性质，提高软件可信程度 演绎验证：指用逻辑推理的方法来证明程序具备所期望的性质 演绎验证可以保证程序无错 程序逻辑：对程序进行推理的逻辑,基 本 知 识,命题逻辑 合式公式（well-formed formula）的归纳定义 := p | ( ) | ( ) | ( ) | ( ) (1) p代表原子命题，例如 x 3, a5 = 10.5 原子命题具体形式与讨论的问题领域有关 (2) 代表一般命题，“:=”右部用“| ”分隔的各部分代表命题的构成形式，如 0= x x 100 (3) , , 和代表合取、析取、非和蕴含运算，在确定了它们的运算优先关系后，很多情况下括号可以省略，如p (q1 q2)可简化为p q1 q2 备注：采用而不是 ， 用于描述函数类型,基 本 知 识,命题逻辑 推理规则 例：有关合取“”运算的推理规则 ( i) (e1) (e2) “ i”表示合取引入规则（i: introduction） “ e”表示合取消去规则（e: elimination） 对和等都有各自的推理规则, ,谓词逻辑 合式公式 (1) 谓词集合、函数集合（包括常量） (2) 基于来定义项集 t := x | c | f(t, , t) ( f ) (3) 归纳地定义基于（ , ）的合式公式 := P(t1, t2, , tn) | ( ) | ( ) | ( ) | ( ) | (x ) | ( x ) ( P ) 增加的规则 全称量词和存在量词的证明规则等,基 本 知 识,Hoare 逻 辑,程序逻辑 对程序进行推理的逻辑 Hoare逻辑是一种程序逻辑 介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的Hoare逻辑推理规则,Hoare 逻 辑,合式公式 语法形式：P S Q，称为Hoare三元式 (1) S是代码段，遵循相应编程语言的语法 (2) P和Q是关于程序状态（变量到值的映射）的断言，分别称为S的前断言和后断言，断言是谓词逻辑的合式公式 (3) 例： x = 1 y 1 y 0 y 5也成立,Hoare 逻 辑,赋值公理 形式：QE/x x = E Q QE/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不成立,Hoare 逻 辑,结构化语句的推理规则 顺序语句 条件语句（也可用其它形式表示） 插曲：推论规则,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) 同理得: true (x y) z = y z = x z = y (4) 得: true if (x y) z = x else z = y z = x z = y,由条件语句 的规则,Hoare 逻 辑,结构化语句的推理规则（续） 循环语句 例：用自然数加法来完成自然数相乘 x = 0; y = 0; while (y n) /循环不变式：(x = my) (y n) x = x + m; y = y + 1; / x = m n,I 被称为 循环不变式,I E 语句S和后断言I的最弱前条件： (x = my y n y n) (x+m = m(y+1) y+1 n),Hoare 逻 辑,小结 用Hoare逻辑，可以对简单程序进行手工证明 手工体现在两方面 (1) 手工用推理规则进行演算或推理 (2) 手工进行定理证明（前例遇到蕴含式的证明） 第一次讲座对自动定理证明已略有介绍 如何走向自动验证（以函数的正确性验证为例） (1) 函数的前条件和后条件必须由验证者给出 (2) 把推理规则改造成能自动演算的演算规则 (3) 借助自动定理证明器,生成验证条件的演算,最弱前条件（Weakest Precondition）演算WP WP : 程序集 断言集 断言集 WP(S, Q)：计算P S Q的最弱前条件P Hoare逻辑的赋值公理是最弱前条件演算的一条规则 (1) 赋值公理：QE/x x = E Q (2) 赋值语句的WP演算规则： WP (x =E, Q) = QE/x,生成验证条件的演算,最弱前条件演算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)称为验证条件,生成验证条件的演算,最弱前条件演算WP WP(x =E, Q) = QE/x QE/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),生成验证条件的演算,最弱前条件演算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, WPi1(while E do S, Q) WP() = WP0 () WP1 () WP2 () ,WP演算在循环语句 这里遇到了困难,生成验证条件的演算,最弱前条件演算WP 一些其他规则 (1) WP(S, false) = false (2) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2) (3) WP(S, Q1 Q2) = WP(S, Q1) WP(S, Q2) (4) (5) WP(S, true) = 保证S终止的最弱前条件 . 下面考虑解决由循环语句引出的问题,生成验证条件的演算,生成验证条件的演算VC(verification condition) 把WP演算放宽为VC演算, 即并非强求最弱前条件 (1) 要求验证者提供循环不变式 (2) VC(S, Q)强于WP(S, Q) (3) VC(S, Q)仍弱于P ，即P VC(S, Q)WP(S, Q),生成验证条件的演算,生成验证条件的演算VC(verification condition) 除了循环语句外，VC演算与WP的一致 循环语句的VC演算如下，其中I是循环不变式 VC(while E do S, Q) = I x1xn( I E VC(S, I) (I E Q) 其中x1, , xn是在S中被修改的所有变量 实际做法 (1) 黄色部分和绿色部分 分别作为循环出口和入口的验证条件 (2) I作为继续逆向VC演算的后断言,程 序 验 证 实 例,void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do x = x + m ; y = y + 1 ; ,例子：用加运算来实现乘运算的函数,程 序 验 证 实 例,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 / 后条件,由程序员提供,由程序员提供,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) / 循环不变式 x = x + m ; y = y + 1 ; x = m n,也由程序员提供,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) / 循环不变式 x = x + m ; y = y + 1 ; x = m n,函数前后条件、循环不变式 都称为断言 它们看上去像编程语言的布 尔表达式,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) x = x + m ; y = y + 1 ; (x = my) (y n) (y n) / 循环结束程序点的断言 x = m n,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) x = x + m ; y = y + 1 ; (x = my) (y n) (y n) (x = mn) x = m n,第1个验证条件,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,通过最弱前条件演算得到,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; y = 0 ; (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n) while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,第2个验证条件,程 序 验 证 实 例,n 0 void mult(int m, int n) x = 0 ; (x = m0) (0 n) y = 0 ; (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n) while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,程 序 验 证 实 例,n 0 void mult(int m, int n) (0 = m0) (0 n) x = 0 ; (x = m0) (0 n) y = 0 ; (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n) while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,程 序 验 证 实 例,n 0 void mult(int m, int n) ( n 0 ) (0 = m0) (0 n) (0 = m0) (0 n) x = 0 ; (x = m0) (0 n) y = 0 ; (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n) while (y n) do (x = my) (y n) (x+m = m(y+1) (y+1) n) x = x + m ; (x = m(y+1) (y+1) n) y = y + 1 ; (x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,第3个验证条件,程 序 验 证 实 例,n 0 void mult(int m, int n) ( n 0 ) (0 = m0) (0 n) x = 0 ; y = 0 ; (x =my) (y n) (y n) (x+m =m(y+1) (y+1) n) while (y n) do (x = my) (y n) x = x + m ; y = y + 1 ; (x = my) (y n) (y n) (x = mn) x = m n,由自动定理证明器完成验证条件的证明,程 序 验 证 实 例,程序：二分查找 val = 38, i = 0, j = 14, k = 7 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,i,j,k,观察点,程 序 验 证 实 例,程序：二分查找 val = 38, i = 0, j = 6, k = 3 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,i,j,k,观察点,程 序 验 证 实 例,程序：二分查找 val = 38, i = 4, j = 6, k = 5 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,i,j,k,观察点,程 序 验 证 实 例,程序：二分查找 val = 38, i = 6, j = 6, k = 6 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,i,j,k,观察点,程 序 验 证 实 例,程序：二分查找 val = 38, i = 6, j = 5, k = 6 i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,i,j,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 没有找到,i,j,k,观察点,程 序 验 证 实 例,程序：二分查找 val = 37, i = 6, j = 4, k = 5 （若val改成37） i = 0; j = 14; while(i = ak) i = k + 1; if (i 1 j) 找到 else 没有找到,j,i,k,观察点,程 序 验 证 实 例,程序：二分查找的主要程序段和断言 int i, j, k, val, am; /此前有#define m = 15 m 0 i = 0 j = m1 n:0m2.an an ji = 2 k = i1 val = ak ) /循环不变式 k = i + (j i)/2; /包括黄色部分 if(val = ak) i = k + 1; 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:/kyhcs.ustcsz.edu.cn/SGL,小 结,本讲座小结 介绍怎样从Hoare逻辑得到一种对应的演算，最终得到自动证明程序是否具备所期望性质的一种方法 程序验证的应用情况例举 空客公司在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.,