程序正确性证明1

3-1主要内容程序正确性简介程序测试程序正确性证明第5章程序的正确性证明3-2内容线索程序正确性简介程序测试程序正确性证明3-3程序的正确性所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”程序正确性的严格定义分为三种类型部分正确性终止性完全正确性3-4如何保证程序的正确性要求1、从编程时就应该尽量地避免和减少错误的发生2、当程序编好后要尽量找出错误，纠正错误避免错误的方法1、程序的结构要简单2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法发现错误的方法1、利用测试工具2、利用程序的验证系统3-5内容线索程序正确性简介程序测试程序正确性证明3-6程序测试测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。3-7程序测试的过程…3-8…程序测试的过程3-9程序测试的方法两种常用的测试方法黑盒测试这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。黑盒测试又叫做功能测试或数据驱动测试。白盒测试此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。通过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。3-10黑盒测试…黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误:是否有不正确或遗漏了的功能?在接口上，输入能否正确地接受?能否输出正确的结果?是否有数据结构错误或外部信息(例如数据文件)访问错误?性能上是否能够满足要求?是否有初始化或终止性错误?用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。但这是不可能的。3-11白盒测试…软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：对程序模块的所有独立的执行路径至少测试一次；对所有的逻辑判定，取“真”与取“假”的两种情况都至少测试一次；在循环的边界和运行界限内执行循环体；测试内部数据结构的有效性等。3-12…白盒测试…对一个具有多重选择和循环嵌套的程序，不同的路径数目可能是天文数字。给出一个小程序的流程图，它包括了一个执行20次的循环。包含的不同执行路径数达520条，对每一条路径进行测试需要1毫秒，假定一年工作365×24小时，要想把所有路径测试完，需3170年。3-13…白盒测试语句覆盖判定覆盖条件覆盖判定－条件覆盖条件组合覆盖路径覆盖3-14内容线索程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法子目标断言法Hoare规则公理方法3-15正确性证明测试只能发现程序错误，但不能证明程序无错。原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。3-16正确性证明的发展50年代1967年1969年1973年1975年1976年1979年1980年第一个基于公理和推导规则的自动验证系统出现。Dijkstra提出最弱前置谓词和谓词转换器的概念。出现了用公理化思想定义的程序设计语言——Euclid。同年，Perlis批评程序正确性证明不切实际。Gries综合了以谓词演算为基础的证明系统，称为程序设计科学。首次把程序设计从经验技术升华为科学。Turing等Floyd用断言方法证明框图程序的正确性Hoare定义一个逻辑系统，含有程序公理和推导规则。目的侧重于程序的部分正确性。此系统是一阶谓词逻辑的扩充。这就是著名的Hoare逻辑。Hoare是第一个从正确性证明角度定义程序语言的。Hoare和Wirth把Pascal的大部分公理化。Manna把部分正确性证明和终止性证明归于一体。3-17正确性证明的方法为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。主要方法有：关于部分正确性证明的方法Floyd的不变式断言法(*)Manna的子目标断言法Hoare的公理化方法(*)关于终止性证明的方法Floyd的良序集方法(*)Manna等人的不动点方法Knuth的计数器方法关于完全正确性证明的方法Hoare的公理化方法的推广（Manna，Pnueli）Burstall的间发断言方法Dijkstra最弱前置谓词变换方法以及强验证方法(*)3-18程序正确性理论•程序功能的精确描述1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题程序规约程序3-19预备知识…程序的状态：程序执行到某一时刻，程序中所有变量的一组取值初始状态：所有变量的取值使程序的前置断言为真的状态终止状态：所有变量的取值使程序的后置断言为真的状态程序的执行可以看作是程序状态的变迁逻辑谓词前提条件，初始状态前置断言程序，语句结论，终止状态满足的条件后置断言逻辑谓词3-20程序规约Q{S}R是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。程序正确性定义3-21部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。程序终止：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。完全正确：若对于每个使得Q(i)为真，并且程序S的计算都将终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。程序正确性定义3-22内容线索程序正确性简介程序测试程序正确性证明简介Floyd不变式断言法Hoare规则公理方法Dijkstra最弱前置条件方法Dijkstra最弱前置条件方法3-23R.W.Floyd，1967年提出证明一个程序的部分正确性步骤（1）建立断言前置断言((x))：前提条件，初始状态后置断言((x,z))：最终结论，终止状态满足的条件循环不变式：在循环中选取一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真（2）建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：I∧R=O,其中I为输入断言，R为进入通路的条件，O为输出断言不变式断言法3-24（2）建立检验条件检验条件：程序运行通过该通路时应满足的条件i(x,y)Ri(x,y)i(x,ri(x,y))输入断言输出断言y：一组中间变量x：输入变量xy：蕴含符，即ri(x,y)：通过该通路后y的值通过此路径的条件3-253、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。3-26实例设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=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT3-27证明…(1)建立断言(x)：x10x20(x,z)：z=gcd(x1,x2)在B点建立不变式断言P(x,y)：x10x20y10y20gcd(y1,y2)=gcd(x1,x2)(2)建立检验条件通路1：A--B;通路2：B--D--B通路3：B--E--B;通路4：B--G--C为每一条通过，建立检验条件开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT3-28通路1：A--B无条件，R1(x,y)恒真，结果y取值为x。检验条件为：(x)P(x,y)即[x10x20]x10x20gcd(x1,x2)=gcd(x1,x2)开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT…证明…3-29通路2：B--D--BR2(x,y)=[y1y2y1y2]r2(x,y)=(y1-y2,y2)输入输出均为P(x,y)检验条件为：[P(x,y)y1y2y1y2]P(x,y1-y2,y2)将断言P(x,y)代入，即得[x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2][x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)]开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT…证明…3-30…证明…通路3：B--E--B类似地，得到[P(x,y)y1y2y1y2]P(x,y1,y2-y1)通路4：B--G--C类似地，得到[P(x,y)y1=y2](x,z)开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT3-31…证明(3)证明检验条件通路1：[x10x20]x10x20gcd(x1,x2)=gcd(x1,x2)显然通路2：[x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2][x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)]检验条件前项成立时，y1y2为真，而y1-y20为真且gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)检验条件为真通路3：[P(x,y)y1y2y1y2]P(x,y1,y2-y1)y1y2为真,y1-y20为真,gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2)检验条件为真通路4：[P(x,y)y1=y2](x,z)y1=y2,gcd(y1,y2)=y1=y2,检验条件为真3-32不变式断言法实例对任一给定的自然数x，计算z＝[]，即计算x的平方根取整算法：1＋3＋…(2n+1)=(n+1)2取：y1=n;y3=奇数2n+1；y2=1+3+5+……+(2n+1)=(n+1)2=(y1+1)2;输入断言：I(x):x0输出断言：O(x,z):z2≤x(z+1)2