资源描述：
《最新A P(X1,X2,Y1,Y2) B C O(X,Y,Z) D E G 通路划分 - READ幻灯片.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、AP(X1,X2,Y1,Y2)BCO(X,Y,Z)DEG通路划分-READ什么样的程序才是正确的？如何来保证程序是正确的？程序正确性概述关于程序正确性的认识根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。什么样的程序才是正确的？“测试”或“调试”方法采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。程序规约的基本分类非形式化程序规约非形式化程序规约采用自然语言描述程序功能，简
2、单、方便，但存在二义性，因此，不利于程序的正确性证明。形式化程序规约采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。程序规约的实例（1/2）在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。例1：求数组b[0:n-1]中所有元素的最大值。[inn:integer;inb[0:n-1]:arrayofinteger;outy:integer]Q:{n≥1}SR:{y＝MAX（i:0≤i＜n;b[i])}例2：求两个非负
3、整数的最大公约数。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX（i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0):i)}程序规约的实例（2/2）程序正确性定义（1/3）衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。程序设计过程：问题程序规约程序对程序的正确性理解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。从狭义而言，如果一个程序满足了它的程序规约
4、就是正确的。程序规约Q{S}R是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。程序正确性定义（2/3）部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。程序终止：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。完全正确：若对于每个使得Q(i)为真，并且程序S的计算都将终止的输入信
5、息i，R(i,S(i))都为真，则称程序S关于Q和R是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。程序正确性定义（3/3）（1）证明部分正确性的方法A.Floyd的不变式断言法B.Manna的子目标断言法C.Hoare的公理化方法（2）终止性证明的方法A.Floyd的良序集方法B.Knuth的计数器方法C.Manna等人的不动点方法（3）完全正确性的方法A.Hoare公理化方法的推广B.Burstall的间发断言法C.Dijkstra的弱谓词变换方法以及强验证方法程序正确性的证明方法分类循环不变式断言把
6、反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。例带余整数除法问题：设x为非负整数，y为正整数，求x除以y的商q，以及余数r。程序：q＝0；r＝x；while(r≥y)//该循环不变式断言：{//(x＝y×q＋r)∧r≥0r＝r－y；q＝q＋1；}不变式断言法证明步骤：1、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言2、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：I∧R=>O
7、,其中I为输入断言，R为进入通路的条件，O为输出断言3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。不变式断言法实例例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer);vary1,y2,z:Integer;Beginy1:=x1;y2:=x1;whiley1<>y2doify1>y2theny1:=y1-y2elsey2:=y2-y1end;z:=y1;write(z);End.START(
8、x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不变式断言法实例(建立断言)输入断言：I(x1,x2):x1>0^x2>0输出断言：O(x1,x2,z):z=gcd(x1,x2)循环
