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

《对程序进行推理的逻辑计算机科学导论第二讲.ppt》由会员分享，可在线阅读，更多相关《对程序进行推理的逻辑计算机科学导论第二讲.ppt（57页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、对程序进行推理的逻辑计算机科学导论第二讲,计算机科学技术学院陈意云0551-63607043，http:/,课 程 内 容,课程内容围绕学科理论体系中的模型理论, 程序理论和计算理论1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力2. 程序理论关心的问题给定模型M，如何用模型M解决问题包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3. 计算理论关心的问题给定模型M和一类问题, 解决该类问题需多少资源,2,本次讲座讨论怎样用数学方法证明程序是正确的,讲 座 提 纲,基本知识程序验证、程序逻辑、命题逻辑、谓词逻辑Hoare逻辑

2、Hoare三元式、赋值公理、结构化语句的推理规则、推论规则生成验证条件的演算最弱前条件演算、生成验证条件的演算程序验证实例演示二分查找程序,3,序 曲,近几年软件错误带来危害的事例2012年，美国KCP金融公司由于电子交易系统出现故障，交易算法出错，导致该公司对150支不同的股票高价购进、低价抛出，直接给公司带来了4.4亿美元的损失，当天股票下跌62%2013年9月12日，美联航售票网站一度出现问题，售出票面价格为0-10美元的超低价机票，引发抢购。大约15分钟后，美联航发现错误，关闭售票网站并声称正在进行维护。大约两个多小时后，该公司售票网站恢复正常，并且承认已卖出的票有效,4,序 曲,软件

3、错误带来危害的事例据自然杂志网站报道，广受世界天文学界期待的日本旗舰级天文卫星“瞳”（Hitomi）于2016年2月17日发射升空，但在大约5周之后便出现翻滚失控迹象。经调查后日本方面宣布，事故原因源自底层软件错误。卫星的控制系统在发现飞行姿态失控时，采取了错误的调整，推进器点火时朝向了错误的反方向，导致自身旋转更加严重，最终彻底失控,5,序 曲,软件无处不在全世界有超过10亿辆汽车在行驶，每辆新汽车上都有2080个微处理器，有多达3000万行的代码在运行全世界每年有多达23亿次手术，在每个现代医疗设备上往往会有超过30万行的代码在运行全世界有超过3000辆高速列车在行驶，每辆列车上会有多达6

4、000万行的代码在运行全世界有超过300万架飞机，新型飞机上会有多达2000万行代码在运行如何保证这些代码没有错误？,6,基 本 知 识,程序：在数组a中快速查找某个值int amn:0.m2.an 0) 的各种情况都要测试吗？对a中出现的各个元素都需要测试吗？对a中不出现的元素要测多少种情况？,7,基 本 知 识,程序测试与程序验证测试能发现程序有错；一般而言，测试不能保证程序无错程序验证：用数学的方法来证明程序的性质，提高软件可信程度演绎验证：指用逻辑推理的方法来证明程序具备所期望的性质就所期望的性质而言，演绎验证可保证程序无错程序逻辑：对程序进行推理的逻辑,8,基 本 知 识,命题逻辑程

5、序设计中用到命题逻辑的知识if (0 = 100) ; n = n + 1; !是命题逻辑的一元运算符（下面用而不是 !）,9,基 本 知 识,命题逻辑合式公式（well-formed formula）的归纳定义 := p | | | | | ( )(1) p代表原子命题，例如 x 3, a5 = 10.5 原子命题具体形式与讨论的问题领域有关(2) 代表一般命题，“:=”右部用“| ”分隔的各部分代表命题的构成形式，如 0= x x 100(3) , , 和代表合取、析取、非和蕴涵运算，在确定了它们的运算优先关系后，很多情况下括号可以省略，如p (q1 q2)可简化为p q1 q2备注：蕴涵

6、采用而不是 ， 用于描述函数类型,10,基 本 知 识,命题逻辑推理规则例：有关合取“”运算的推理规则( i)(e1) (e2)“ i”表示合取引入规则（i: introduction）“ e”表示合取消去规则（e: elimination）对和等也都有各自的推理规则, ,11,谓词逻辑程序设计中用到谓词逻辑的知识谓词：结果类型为bool的函数bool even(int m) /用编程语言写的谓词，与数理 if (m/2 * 2 = m) return true; /逻辑中的有区别 else return false; if(even(x) & even(y) 、=、=、!= 等关系算符都是谓

7、词,基 本 知 识,12,谓词逻辑合式公式(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,Hoare 逻 辑,程序逻辑对程序进行推理的逻辑Hoare逻辑是一种程序逻辑介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的Hoare逻辑推理规则,14,Ho

8、are 逻 辑,合式公式（well-formed formula）语法形式：P S Q，称为Hoare三元式(1) S是代码段，遵循相应编程语言的语法(2) P和Q是关于程序状态（变量到值的映射）的断言，分别称为S的前断言和后断言，断言是谓词逻辑的合式公式(3) 例： x = 1 y 1 y 0 y 5也成立,15,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都可作为前

9、断言，因都强于x 5x 5.1 x 5 并且x 7 x 5(2) 若x 4.9作为前断言，则三元式不成立，因为x 4.9 x 5不成立,16,Hoare 逻 辑,结构化语句的推理规则顺序语句条件语句（也可用其它形式表示）插曲：推论规则,17,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

10、 = 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,由条件语句的规则,18,Hoare 逻 辑,结构化语句的推理规则（续）循环语句例：用自然数加法来完成自然数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 被称为 循环不变式,19,/循环不变式I：(x = my) (y n),Hoare 逻 辑,结构化语句的推

11、理规则（续）循环语句例：用自然数加法来完成自然数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 被称为 循环不变式,20,/循环不变式I：(x = my) (y n),分两步看，对于y = y + 1,Hoare 逻 辑,结构化语句的推理规则（续）循环语句例：用自然数加法来完成自然数m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 演算得到语句S和后断言I的最弱前条件

12、：x+m = m(y+1) y+1 n,I 被称为 循环不变式,21,/循环不变式I：(x = my) (y n),分两步看，对于x = x + m,Hoare 逻 辑,结构化语句的推理规则（续）循环语句例：用自然数加法来完成自然数m和n相乘x = 0; y = 0;while (y n) x = x + m; y = y + 1; / x = m n 证明I E 语句S和后断言I的最弱前条件：,I 被称为 循环不变式,22,/循环不变式I：(x = my) (y n),(x = my y n y n) (x+m = m(y+1) y+1 n),最后一行称为验证条件,Hoare 逻 辑,小结用

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

14、是最弱前条件演算的一条规则(1) 赋值公理：QE/x x = E Q(2) 赋值语句的WP演算规则： WP (x =E, Q) = QE/x,24,生成验证条件的演算,最弱前条件演算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蕴涵最弱前条件即可, 不必要求等于后者,

15、25,生成验证条件的演算,最弱前条件演算WPWP(x =E, Q) = QE/xQE/x x = E QWP(S1;S2, Q) = WP (S1, WP(S2, Q)WP(if E then S1 else S2, Q) =(WP(S1, Q) E) (WP(S2, Q) E),26,生成验证条件的演算,最弱前条件演算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(whi

16、le E do S, Q) = WP0 () WP1 () WP2 () ,WP演算在循环语句这里遇到了困难,27,生成验证条件的演算,最弱前条件演算WP一些其他规则(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终止的最弱前条件 . 下面考虑解决由循环语句引出的问题,28,生成验证条件的演算,生成验证条件的演算VC(verification condition)

17、 (1) 观察P和WP之间的关系(2) 寻找两者之间的一种称为VC(S, Q)的演算(3) 即P VC(S, Q)WP(S, Q)(4) VC演算的特点：要求验证者提供循环不变式,false,true,strong,weak,Precondition(S, Q),最弱前条件 WP(S, Q),验证者提供的前条件P,29,生成验证条件的演算,生成验证条件的演算VC(verification condition)除了循环语句外，VC演算与WP的一致循环语句的VC演算如下，其中I是循环不变式VC(while E do S, Q) = I x1xn( I E VC(S, I) (I E Q)其中x1,

18、 , xn是在S中被修改的所有变量实际做法(1) 黄色部分和绿色部分 分别作为循环出口和入口的验证条件(2) I作为继续逆向VC演算的后断言,30,程 序 验 证 实 例,void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do x = x + m ;y = y + 1 ; ,例子：用加运算来实现乘运算的函数,31,程 序 验 证 实 例,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 / 后条件,由程序员提

19、供,由程序员提供,32,程 序 验 证 实 例,n 0void 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,也由程序员提供,33,程 序 验 证 实 例,n 0void 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,函数前后条件、循环不变式都称为断言它们看上去像编程语言的布尔表达式

20、,34,程 序 验 证 实 例,n 0void 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 I E,35,程 序 验 证 实 例,n 0void 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 =

21、 m nI E Q（Q是函数后条件）,第1个验证条件,36,程 序 验 证 实 例,n 0void 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,通过最弱前条件演算得到,37,程 序 验 证 实 例,n 0void mult(int m, int n) x = 0 ; y = 0 ;while (y n) do (x = m

22、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 = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,38,程 序 验 证 实 例,n 0void mult(int m, int n) x = 0 ; y = 0 ; I E VC(S, I)（S是循环体） (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)

23、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个验证条件,39,程 序 验 证 实 例,n 0void 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)

24、 y = y + 1 ;(x = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,40,程 序 验 证 实 例,n 0void 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

25、n) (x = my) (y n) (y n) (x = mn) x = m n,41,程 序 验 证 实 例,n 0 P VC(S, I) 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

26、 = my) (y n) (x = my) (y n) (y n) (x = mn) x = m n,第3个验证条件,P是函数前条件，S是循环之前的语句序列,42,程 序 验 证 实 例,n 0void 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,由自动定理证明器完成验

27、证条件的证明,43,程 序 验 证 实 例,程序：二分查找#define m 15int amn:0.m2.an an+1用二分法在数组a15中快速查找38,44,程 序 验 证 实 例,程序：二分查找val = 38, i = 0, j = 14, k = 7i = 0; j = 14;while(i = ak) i = k + 1;if (i 1 j) 找到 else 没有找到,i,j,k,观察点,45,程 序 验 证 实 例,程序：二分查找val = 38, i = 0, j = 6, k = 3i = 0; j = 14;while(i = ak) i = k + 1;if (i 1

28、j) 找到 else 没有找到,i,j,k,观察点,46,程 序 验 证 实 例,程序：二分查找val = 38, i = 4, j = 6, k = 5i = 0; j = 14;while(i = ak) i = k + 1;if (i 1 j) 找到 else 没有找到,i,j,k,观察点,循环不变性： a0到ai-1都小于38 aj+1到a14都大于38,47,程 序 验 证 实 例,程序：二分查找val = 38, i = 6, j = 6, k = 6i = 0; j = 14;while(i = ak) i = k + 1;if (i 1 j) 找到 else 没有找到,i,j,

29、k,观察点,循环不变性： a0到ai-1都小于38 aj+1到a14都大于38,48,程 序 验 证 实 例,程序：二分查找val = 38, i = 6, j = 5, k = 6i = 0; j = 14;while(i = ak) i = k + 1;if (i 1 j) 找到 else 没有找到,i,j,k,条件不成立,49,程 序 验 证 实 例,程序：二分查找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,观察点,循

30、环不变性： a0到ai-1都小于38 aj+1到a14都大于38,50,程 序 验 证 实 例,程序：二分查找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,条件不成立,51,程 序 验 证 实 例,程序：二分查找的主要程序段和断言int i, j, k, val, am; /此前有#define m 15m = 15 (n:0.m2.an an) ji = 2 k = i1 val = ak ) /循环不变式, 含黄色部分 k

31、 = i + (j i)/2; if(val = ak) i = k + 1;m = 15 (n:0.m2.an an+1) (ij = 2 k = i1 val = ak ij = 1 n:0.m1. val != an) ,52,程 序 验 证 实 例,正在开发的程序验证系统的验证实例数组快速排序、冒泡排序、二分查找、二叉堆、矩阵乘、矩阵分块乘等易变数据结构下面这些数据类型的插入函数和删除函数等1、单链表、循环单链表2、双向变量、循环双向链表3、二叉排序树、平衡树(AVL tree)、 AA 树、树堆(treap)、伸展树(splay tree)演示二分查找的例子,53,程 序 验 证 实

32、 例,正在开发的程序验证系统的验证实例验证二分查找需用到的引理lemma 1: int m. int bm. int value. int k.( int n: 0.m-2. bn bk 0 bn)lemma 2: int m. int bm. int value. int k.( int n: 0.m-2. bn bn+1) value bk 0 = k m ( int n: k.m-1. value bn)自动定理证明器发现不了这样的归纳性质,54,小 结,本讲座小结介绍怎样从Hoare逻辑得到对应的演算，最终得到自动证明程序是否具备所期望性质的一种方法程序验证的应用情况例举空客公司在A4

33、00M军用航空器以及A380和A350商用航空器的开发上，已经用形式证明取代了部分安全攸关嵌入式软件的测试达索航空公司在健壮性的形式验证方面，有约15%的断言是用演绎验证方式证明的工具VeriFast完成4个工业应用案例的安全性验证相关课程：程序设计语言基础、程序设计语言理论,55,小 结,研究方向提高断言语言的表达能力提高自动定理证明器的证明能力工具实验室：Dafny、Spec#、Ynot和Why3等工业界开始应用的有Caveat、 Frama-C和 SPARK2014,56,小 结,参考文献何伟等译，面向计算机科学的数理逻辑，2007.Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications to VerificationYannick Moy, etc. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Software, 30(3):50-57, 2013.本次讲座的基础知识部分来自上面第1篇参考文献,57,