程序正确性证明.ppt

程序正确性证明 主要内容 程序正确性简介 程序测试 程序正确性证明 内容线索 程序正确性简介 程序测试 程序正确性证明 程序的正确性 所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。 或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。 通俗地说，“做了它该做的事，没有做它不该做的事” 程序正确性的严格定义分为三种类型 部分正确性 终止性 完全正确性 如何保证程序的正确性 要求 1、从编程时就应该尽量地避免和减少错误的发生 2、当程序编好后要尽量找出错误，纠正错误 避免错误的方法 1、程序的结构要简单 2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法 发现错误的方法 1、利用测试工具 2、利用程序的验证系统 内容线索 程序正确性简介 程序测试 程序正确性证明 程序测试 测试是程序的执行过程，目的在于发现错误。 一个好的测试用例在于能发现至今未发现的错误； 一个成功的测试是发现了至今未发现的错误的测试。 测试的原则 1. 应当 “尽早地和不断地进行软件测试” 。 2. 测试用例应由测试输入数据和对应的预期输出结果组成。 3. 程序员应避免检查自己的程序。 4. 在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。 5. 充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。 6. 严格执行测试计划，排除测试的随意性。 7. 应当对每一个测试结果做全面检查。 8. 妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。 内容线索 程序正确性简介 程序测试 程序正确性证明 简介 Floyd不变式断言法 Hoare规则公理方法 Dijkstra最弱前置条件方法 正确性证明 测试只能发现程序错误，但不能证明程序无错。即所谓“挂一漏万”。 原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。 正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。 正确性证明的发展 正确性证明的方法 为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。 主要方法有： 关于部分正确性证明的方法 Floyd的不变式断言法(*) Manna的子目标断言法 Hoare的公理化方法(*) 关于终止性证明的方法 Floyd的良序集方法(*) Manna等人的不动点方法 Knuth的计数器方法 关于完全正确性证明的方法 Hoare的公理化方法的推广（ Manna ，Pnueli） Burstall的间发断言方法 Dijkstra最弱前置谓词变换方法以及强验证方法(*) 预备知识… 前置(输入)断言:输入应满足的条件 后置(输出)断言:输入出应满足的条件 程序规范：程序的前置断言和程序的后置断言组成 程序的状态：程序执行到某一时刻，程序中所有变量的一组取值 初始状态：所有变量的取值使程序的前置断言为真的状态 终止状态：所有变量的取值使程序的后置断言为真的状态 程序的执行可以看作是程序状态的变迁 …预备知识 1、完全正确性断言：程序S的执行开始于满足P的状态，则该执行必定能在有限的时间内终止，且终止的状态满足Q，则称完全正确性断言，记为{P}S{Q} 2、部分正确性断言：程序S的执行开始于满足P的状态，若此执行能在有限的时间内终止，则终止时的状态满足Q，则称部分正确性断言，记为[P]S[Q] 程序正确性概念 定义1. 如果对于每一个使得P(ā)为真的输入ā ，程序S计算都终止，称程序S对P是终止的。 定义2：对于满足P(ā)为真，且能够使程序S计算终止的每个ā，如果Q(ā, P(ā))为真，则称程序S对于P和Q是部分正确的。记为[P] S [Q]。 定义3：对于满足P(ā)为真的每个ā ，如果程序S能够计算终止，且Q(ā, P(ā))为真，则称程序S对于P和Q是完全正确的。记为 {P} S{Q} 不变式断言法 R.W.Floyd，1967年提出 证明一个程序的部分正确性 步骤 （1）建立断言 输入断言(?(x))：前提条件，初始状态 输出断言(?(x,z))：最终结论，终止状态满足的条件 循环不变式：在每次循环的前后均为真的谓词 （2）建立检验条件 检验条件：程序运行通过该通路时应满足的条件 （3）证明检验条件 适合对象：程序流程图 实例 设x1,x2是正整数，求它们的最大公约数z=gcd(x1,x2)。我们知道，对于任意正整数y1,y2，有下列关系： 证明… (1)建立断言 ?(x)： x10 ? x2 0 ?(x,z)： z=gcd(x1,x2) P(x,y)： x10 ?