第5章程序正确性证明.ppt

5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法－－计数器法 5.1 程序正确性概述 关于程序正确性的认识 什么样的程序才是正确的？ “测试”或“调试”方法 根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。 程序正确性证明发展历程 20世纪50年代 Turing开始研究。 1967年，Floyd和Naur提出不变式断言法。 1969年，Hoare提出公理化方法。 1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。 程序正确性理论 程序设计的一般过程 程序正确性理论 程序功能的精确描述 1、程序规约：对程序所实现功能的精确描述， 由程序的前置断言和后置断言两部分组成。 2、前置断言：程序执行前的输入应满足的条件， 又称为输入断言。 3、后置断言：程序执行后的输出应满足的条件， 又称为输出断言。 程序规约的基本分类 非形式化程序规约 非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。 形式化程序规约 采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。 程序规约的实例 在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。 程序规约的实例 程序正确性定义 衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。 对程序的正确性理解，可以分为两个层次： 从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。 从狭义而言，如果一个程序满足了它的程序规约就是正确的。 程序正确性定义 程序规约Q{S}R是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为 “程序S，关于前置断言Q和后置断言R是完全正确的”。 程序正确性定义 部分正确： 若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。 程序终止： 若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。 完全正确： 若对于每个使得Q(i)为真的输入信息i，程序S的计算都将终止，并且R(i,S(i))都为真，则称程序S关于Q和R是完全正确的。 一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。 程序正确性的证明方法分类 证明部分正确性的方法 A. Floyd的不变式断言法 B. Manna的子目标断言法 C. Hoare的公理化方法 终止性证明的方法 A. Floyd的良序集方法 B. Knuth的计数器方法 C.Manna等人的不动点方法 完全正确性的方法 A. Hoare公理化方法的推广 B. Burstall的间发断言法 C. Dijkstra的弱谓词变换方法以及强验证方法 5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法－－计数器法 循环不变式断言 把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。 5.2 不变式断言法 证明步骤： 1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。 2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式： I ∧ R = O 其中I为输入断言，R为进入通路的条件，O为输出断言。 3、证明检验条件 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。 不变式断言法实例1 例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。 不变式断言法实例1(建立断言) 输入断言： I(x1,x2): x10 ∧x20 输出断言： O(x1,x2,z):z=gcd(x1,x2) 循环不变式断言： P(x