PM讲义-第7章 程序正确性证明(上).ppt

6.3 证明终止性的良序集方法 例：证明计算z=sqrt(x)的程序的终止性(P(x): x ≥ 0) 证明： 1) 在B’处将循环断开，有： q(x,y1,y2,y3)：y2≤x∧y3>0 2) 取良序集为(N,<), 即具有小于关系的自然数集合，并在B’点定义终止表达式： E(x,y) = x-y2 开始 0,0,1 ? y1,y2,y3 y2>x? y1+1,y3+2 ? y1,y3 y1? z 结束 P(x) A F B’ T D G C y2+y3 ? y2 F q(x,y1,y2,y3) 3) 证明q(x,y)是良断言 对路径A ? B’ 有： P(x) ∧True ? q(x,0,0,1), 即： x ≥ 0 ? 0≤x ∧1>0 对路径B’ ? B’有： q(x,y) ∧y2+y3 ≤x ? q(x,y1+1,y2+y3,y3+2) 即： y2≤x∧y3>0 ∧y2+y3 ≤x ? (y2+y3≤x∧y3+2>0 ) 可以证明上式为真，因此中间断言q(x,y)是良断言。 证明所选取的断言是“良断言”，即： 对于每一个从程序入口到断点j的通路a有： P(x) ∧Ra(x,y) ? qj(x,ra(x,y)) 对于每个有断点i到断点j的通路b有： qi(x, y) ∧Rb(x,y) ? qj(x,rb(x,y)) q(x,y1,y2,y3)=y2≤x∧y3>0 4) 证明E(x,y)是良函数 即 q(x,y) ? E(x,y) ∈N， 即 y2≤x∧y3>0 ? x-y2 ≥ 0 证明终止表达式是“良函数”。即： 对于每一个断言i有： qi(x,y) ?Ei(x,y) ∈W q(x,y1,y2,y3)=y2≤x∧y3>0 E(x,y) = x-y2 5) 证明终止条件成立 与循环有关的通路只有B’?D?B’,因而只需证明： q(x,y) ∧y2+y3 ≤x ? E(x,y) > E(x,y1+1,y2+y3,y3+2) 即： y2≤x∧y3>0 ∧y2+y3 ≤x ? (x-y2) > (x-(y2+y3)) 这样，就证明了程序的终止性 qi(x,y) ∧Ra(x,y) ? [Ei(x,y)>--Ej(x,ra(x,y))] E(x,y) = x-y2 第六章 程序正确性证明 概述 不变式断言法证明程序的部分正确性 良序集方法证明程序的终止性 Hoare公理学方法 6.1 概述 基本概念 非形式化的程序验证是靠程序员阅读理解程序完成的。 程序测试是指测试者特意挑出一批输入数据，通过运行程序，检查每个输入数据所对应的运行结果是否符合预期要求。 Dijkstra说过“程序测试只能证明程序有错，不能说明程序正确”。除非进行穷举行测试。 正确性证明是论证程序达到预期目的的一般性陈述，而该论证与程序输入数据的特定值无关，能够代表穷举性测试。 程序正确性概念 定义1. 如果对于每一个使得P(ā)为真，程序S计算都终止，称程序S对P是终止的。 定义2：对于满足P(ā)为真，且能够使程序S计算终止的每个ā，如果Q(ā, P(ā))为真，则称程序S对于P和Q是部分正确的。 定义3：对于满足P(ā)为真的每个ā ，如果程序S能够计算终止，且Q(ā, P(ā))为真，则称程序S对于P和Q是完全正确的。 主要的程序正确性证明方法 （1）关于部分正确性证明的方法 Floyd 的不变式断言法 Manna的子目标断言法 Hoare的公理化方法 （2）关于终止性证明的方法 Floyd的良序集方法 Knuth的计数器方法 Manna等人的不动点方法 （3）关于完全正确性的证明方法 Hoare的公理化方法（Manna、Pnueli） Bustall的间发断言法 Dijkstra的弱谓词转换方法以及强验证方法。 中间断言 定义1：在程序任一中间点 i 附上谓词 , 如果每当执行到达i时 对于该点的当前值必为真，则 称为 i 点上的中间断言，或称为归纳断言。 定义2：对于循环路径上的断言，因为每次循环执行到达该点时该断言必为真，所以该断言又称为循环不变式，简称不变式。 6.2 不变式断言法--证明部分正确性 开始 x1,x2 ? y1,y2 y1= y2? y1>y2?