程序正确性证明课件

程序正确性证明,1,PPT学习交流,主要内容,程序正确性简介程序测试程序正确性证明,2,PPT学习交流,内容线索,程序正确性简介程序测试程序正确性证明,3,PPT学习交流,程序的正确性,所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”程序正确性的严格定义分为三种类型部分正确性终止性完全正确性,4,PPT学习交流,如何保证程序的正确性,要求1、从编程时就应该尽量地避免和减少错误的发生2、当程序编好后要尽量找出错误，纠正错误避免错误的方法1、程序的结构要简单2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法发现错误的方法1、利用测试工具2、利用程序的验证系统,5,PPT学习交流,内容线索,程序正确性简介程序测试程序正确性证明,6,PPT学习交流,程序测试,测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。,7,PPT学习交流,内容线索,程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法,8,PPT学习交流,正确性证明,测试只能发现程序错误，但不能证明程序无错。即所谓“挂一漏万”。原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。,9,PPT学习交流,正确性证明的发展,10,PPT学习交流,正确性证明的方法,为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。主要方法有：关于部分正确性证明的方法Floyd的不变式断言法(*)Manna的子目标断言法Hoare的公理化方法(*)关于终止性证明的方法Floyd的良序集方法(*)Manna等人的不动点方法Knuth的计数器方法关于完全正确性证明的方法Hoare的公理化方法的推广（Manna，Pnueli）Burstall的间发断言方法Dijkstra最弱前置谓词变换方法以及强验证方法(*),11,PPT学习交流,预备知识,前置(输入)断言:输入应满足的条件后置(输出)断言:输入出应满足的条件程序规范：程序的前置断言和程序的后置断言组成程序的状态：程序执行到某一时刻，程序中所有变量的一组取值初始状态：所有变量的取值使程序的前置断言为真的状态终止状态：所有变量的取值使程序的后置断言为真的状态程序的执行可以看作是程序状态的变迁,12,PPT学习交流,预备知识,1、完全正确性断言：程序S的执行开始于满足P的状态，则该执行必定能在有限的时间内终止，且终止的状态满足Q，则称完全正确性断言，记为PSQ2、部分正确性断言：程序S的执行开始于满足P的状态，若此执行能在有限的时间内终止，则终止时的状态满足Q，则称部分正确性断言，记为PSQ,13,PPT学习交流,程序正确性概念定义1.如果对于每一个使得P()为真的输入，程序S计算都终止，称程序S对P是终止的。定义2：对于满足P()为真，且能够使程序S计算终止的每个，如果Q(,P()为真，则称程序S对于P和Q是部分正确的。记为PSQ。,14,PPT学习交流,定义3：对于满足P()为真的每个，如果程序S能够计算终止，且Q(,P()为真，则称程序S对于P和Q是完全正确的。记为PSQ,15,PPT学习交流,不变式断言法,R.W.Floyd，1967年提出证明一个程序的部分正确性步骤（1）建立断言输入断言(x)：前提条件，初始状态输出断言(x,z)：最终结论，终止状态满足的条件循环不变式：在每次循环的前后均为真的谓词（2）建立检验条件检验条件：程序运行通过该通路时应满足的条件（3）证明检验条件适合对象：程序流程图,i(x,y)Ri(x,y)i(x,ri(x,y),输入断言,输出断言,y：一组中间变量x：输入变量xy：蕴含符，即ri(x,y)：通过该通路后y的值,通过此路径的条件,16,PPT学习交流,实例,设x1,x2是正整数，求它们的最大公约数z=gcd(x1,x2)。我们知道，对于任意正整数y1,y2，有下列关系：,(1)若y1y2，gcd(y1,y2)=gcd(y1-y2,y2)(2)若y2y1，gcd(y1,y2)=gcd(y1,y2-y1)(1)若y1=y2，gcd(y1,y2)=y1=y2,开始,(x1,x2)(y1,y2),y1=y2,y1y2,y1-y2y1,y2-y1y2,A(x),BP(x,y),y1z,G,结束,C(x,z),D,E,T,F,F,T,17,PPT学习交流,证明,(1)建立断言(x)：x10x20(x,z)：z=gcd(x1,x2)P(x,y)：x10x20y10y20gcd(y1,y2)=gcd(x1,x2)(2)建立检验条件通路1：A-B;通路2：B-D-B通路3：B-E-B;通路4：B-G-C为每一条通过，建立检验条件通路1：A-B无条件，R1(x,y)恒真，结果y取值为x。检验条件为：(x)P(x,y)即x10x20x10x20y10y20gcd(x1,x2)=gcd(x1,x2),18,PPT学习交流,证明,通路2：B-D-BR2(x,y)=y1y2y1y2r2(x,y)=(y1-y2,y2)P(x,y)输入输出均为P(x,y)检验条件为：P(x,y)y1y2y1y2P(x,(y1-y2,y2)将断言P(x,y)代入，即得x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)通路3：B-E-B类似地，得到P(x,y)y1y2y1y2P(x,y1,y2-y1)通路4：B-G-C类似地，得到P(x,y)y1=y2(x,z),19,PPT学习交流,证明,(3)证明检验条件通路1：x10x20x10x20gcd(x1,x2)=gcd(x1,x2)显然通路2：x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)检验条件前项成立时，y1y2为真，而y1-y20为真且gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)检验条件为真通路3：P(x,y)y1y2y1y2P(x,y1-y2,y2-y1)y1y2为真,y1-y2x,(y1+1,y3+2)(y1,y3),A(x),BP(x,y),y1z,结束,C(x,z),D,T,F,y2+y3y2,B,21,PPT学习交流,内容线索,程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法,22,PPT学习交流,程序正确性验证Hoare公理学方法,1990年IEEE计算机先驱奖1980年图灵奖英国牛津大学计算机科学家查尔斯.霍尔(CharlesAntonyRichardHoare)发明Quicksort算法、CASE语句1963年实现了Algol语言1969年1月，在Comm.OfACM上发表“AnAxiomaticbasisforComputerProgramming”,提出公理语义学操作系统的MonitorACM在1983年评出在近25年在CACM上发表的25篇里程碑式的论文25篇，2人2篇，Hoare是其一,23,PPT学习交流,Hoare公理学方法,在Floyd的归纳法断言基础上，C.A.R.Hoare于1969年发表了“计算机程序设计的公理基础”一文，提出了另一种程序验证的方法，他的成功在于使用了简洁的符号和提出了定义程序语义的公理系统。Hoare公理系统和Hoare逻辑是十多年来引人注目的重要工作。Hoare系统是一个关于形如PSQ的断言的逻辑系统。PSQ是为了区别于完全正确的PSQ断言的部分正确性断言的表示方法。这是方法是针对WHILE型程序提出的。,24,PPT学习交流,Hoare公理学方法-部分正确性证明,1.WHILE型程序WHILE型程序是由一个有限的语句序列组成，每个语句之间的分号隔开，即：B0；B1；.Bn其中，B0是程序中唯一的开始语句：STARTyf(x)Bi(1=i=n)是下列语句之一：,25,PPT学习交流,程序正确性验证Hoare公理学方法,1)赋值语句：yg(x,y)2)条件语句：ifRthenF1elseF2或ifRthenF13)复合：BeginF1，F2，.，FnEnd4)循环语句：whileRdoF15)停机语句：Zh(x,y)HALT其中，语句R是逻辑表达式，F1，F2，.，Fn是上列语句中的任何一种。,26,PPT学习交流,程序正确性验证Hoare公理学方法,例如：计算Z=sqrt(x)的程序：START(y1,y2,y3)(0,1,1);While(y2=0(y1,y2,y3)(0,1,1);While(y2=x)dop(x,y):y12=xandy2=(y1+1)2andy3=2*y1+1(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;Q(x,z):z2x，有：PI,P(x,y)y2xQ.(8)得：P(x,y)While(y2x.(9)(While规则)5)根据并置规则，有：x0(y1,y2,y3)(0,1,1);While(y2x（10）,38,PPT学习交流,程序正确性验证Hoare公理学方法,6）Q(x,y1)Zy1Q(x,z)(赋值公理)得：P(x,y)y2xZy1Q(x,z)(11)7）由(10),(11)得：x=0(y1,y2,y3)(0,1,1);While(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;Q(x,z)证明完毕,39,PPT学习交流,程序正确性验证Hoare公理学方法,正向证明的讨论：引理就是不变式断言法中的检验条件但是，推理过程可以由建立的引理和赋值公理及推理规则，形成完整的程序，如果程序正确的话。Hoare已经将PASCAL语言全部公理化，并建立了一个公理化验证系统,40,PPT学习交流,程序正确性验证Hoare公理学方法,例2：利用Hoare公理化方法证明程序的部分正确性STARTP(X):x00y00x00y00x,yx0,y0;whilexneq0dop(x,y):x0y0(x00y00)(gcd(x,y)=gcd(x0,y0)ifyxthenyy-x;elses,x,yx,y,s;y=gcd(x0,y0)zy;Q(x,z):z=gcd(x0,y0)HALT,41,PPT学习交流,程序正确性验证Hoare公理学方法,反向证明：要证明程序A的部分正确性，只要证明：Goal1:P(x)BodyAQ(x,z)1.1P(x)x,yx0,y0p(x,y)1.1.1P(x)p(x0,y0).(1)1.2p(x,y)whilex0doifyxtheny=y-xelses,x,yx,y,s;y=gcd(x0,y0)1.3y=gcd(x0,y0)zyQ(x,z)1.3.1y=gcd(x0,y0)Q(x,y).(2),42,PPT学习交流,程序正确性验证Hoare公理学方法,1.2p(x,y)whilex0doifyxtheny=y-xelses,x,yx,y,s;y=gcd(x0,y0)1.2.1p(x,y)x0ifyxtheny=y-xelses,x,yx,y,sp(x,y)1.2.1.1p(x,y)x0yxy=y-xp(x,y)1.2.1.1.1p(x,y)x0yxp(x,y-x).(3)1.2.1.2p(x,y)x0yxs,x,yx,y,sp(x,y)1.2.1.2.1p(x,y)x0yxp(y,x).(4)1.2.2(p(x,y)x=0)(y=gcd(x0,y0).(5)最后，只要证明上面最后得到的5个谓词表达式为真即可,43,PPT学习交流,程序正确性验证Hoare公理学方法,反向证明过程讨论:反向证明过程开始于寻找一条适当规则W1,W2,WnW把证明目标W分解为子目标W1,W2,Wn,然后又把子目标Wi用同样的方法再细分，直至最后的子目标或归根于公理或问底于论域的定理。这个过程的每一步可用图表示为：,WW1W2W3Wn,44,PPT学习交流,程序正确性验证Hoare公理学方法,练习1.用反向证明方法证明例1.2.用正向证明方法证明例2.,45,PPT学习交流,小结,Floyd的断言归纳法证明部分正确性Floyd的良序集断言法证明终止性Hoare的公理学方法证明部分正确性,46,PPT学习交流,证明终止性的良序集方法,R.W.Floyd在1967年提出的良序集的概念1)偏序集设有一个非空集合W和一个定义在W上的二元关系-,且这个关系满足下列性质：a)传递性：a,b,cW,如果a-b,b-c,则有a-cb)反对称性：a,bW,如果a-b,则有b-ac)反自反性：aW,a-a称W为具有关系-的偏序集，记为（W，-）例：具有小于关系（-.称（W,-）是一个良序集。例：若N是自然数的集合，那么（N，）是良序集，而上面的（A，）和（B,）不是良序集。若W是非负整数对的集合，在其上定义字典顺序-。即：如果xixj或者xi=xjandyiyj则说（xi,yi）-(xj,yj)这样规定的（W，-）是良序集,48,PPT学习交流,证明终止性的良序集方法,如果(W,-)是良序集，则（Wn，n-）也是良序集。这里Wn是W元素的所有n元组的集合，而n-是Wn上的正规字典序。例：具有小于关系的自然数集合N，即（N，）是良序集。因此，自然数的所有序偶的集合（N2，2）也是良序集。具有小于关系的字母表=A，B，.,Z是良序集，因此长度为3的字符串的集合(3，3)也是良序集。,2)良序集（续）,49,PPT学习交流,证明终