应用部分、程序正确性证明.ppt

第六章 应用部分、程序正确性证明 1. 前面命题演算和谓词演算重要的是利用其概念建立 了命题及谓词的公理系统。 1）矛盾性 2）永真性 这些问题表面上看来都是比较抽象，好象是无实用 价值，其实则不然。,2. 数理逻辑的理论和方法在计算机理论中有如下几方 面应用。 1）准确的理解程序 2）容易的构造程序 3）证明程序的正确性 4）测试系统的可靠性 5）检测程序中的错误 6）提高程序的运行效率 例如：信息奇偶检测法就是数理逻辑学中完成的。 3. 编译程序中，语法上的正确及语义上的正确， 但不能保证程序的完全正确。主要原因是逻辑 上的错误，而逻辑错误用调试的方法是不能解 决的。,例如：百鸡百钱问题 为代码流程 FOR X=0 到 19 FOR Y=0 到 33 判别 5X+3Y+Z=100 若满足判别条件则打印一组X、Y、Z然后继续循环 若不满足判别条件则不打印该组X、Y、Z然后继续 循环,程序如下： Main（） Int x，y，z； For（x=0；x=19；x+） For（y=0；y =33；y+） Z=100-x-y； If（5*x）+（3*y）+（*z）=100 Printf（“%d%d%d“，x，y，z）； 结果为 公 母 小 0 25 75 4 18 78 8 11 81 12 4 84 分析程序在语法语义均为正确而0、25、75显然不对 分析原因是逻辑错误,解决此问题方法1 将该语句If（5*x）+（3*y）+（*z）=100移到 For（y=0；y =33；y+）之前 解决此问题方法2 在Printf（“%d%d%d“，x，y，z）；语句前加 If（x*y*z）=0 语句 若满足判别条件则不打印继 续循环 解决此问题方法3 将For（x=0；x=19；x+）语句 x=0改为x=1， x =19改为x=20 For（y=0；y =33；y+）语句y=0改为 y=1，y =33改为y =33,4.现在也有一些实验程序的验证系统，有许多问题还 没有解决，有待于研究。 例如：计算机的自然语言翻译系统等。 5. 1）程序的正确性是指：给定任何的合法输入程 序最终要停止并要输出结果正确。 2）前者称为终止性问题，后者称为程序的部分正 确性问题。我们只讨论程序的正确性（部分）,6. 我们知道任何一个程序都是对一组数据的加工I/O （入/出） 7. 定义：设P是一个程序： 1）x1xn （记为x）是程序输入数据 2）y1yn （记为y）是程序输出数据 3）BODY是该程序的程序行 则可以表示为： Program P： 程序整体的描述（开始） Read （x）； 数据输入部分 BODY P； 程序体（数据加工部分） Write （y）； 数据输出部分 End P； 程序整体的结束,8. 定义：输入数据必须满足的条件称为程序的输入条 件。即：输入断言（记为INAP（x） 9. 定义：同理数据必须满足的条件称为程序的输出条 件。 即：输出断言 （记为OUAP （X，Y，Z ） 其中z是程序 的中间数据, 中间数据不是最终结果。 例：计算1+2+3+100就有最终结果，与中间 结果。（三角数）,根据定义程序可以描述如下： Program p； ：程序整体描述 Read（x）； ：数据输入部分 INAP（x）； ：程序P的输入断言（非执行语句） BODY P ； ：程序体 OUTAP（x，y，z ） ：程序P的输出断言 Write（） ：程序结果输出部分（非执行语句） End p ：程序P的整体结束,NOTE：在数理逻辑中应当理解断言部分。 即：INAP（x）；与OUTAP（x，y， z） 目的是验证I/0数据是否正确，即用来证明程序的 正确性，为了区别我们用花括号括起来。,10. 程序的部分正确性证明问题可以描述为： INAP（x）； BODY P OUTAP（x，y, z） 11.注意： 用数理逻辑描述，对于任何x，任何y和任 何z，如果执行BODY P （程序体）前INAP （x）真，且BODY P执行一定终止，则执行 BODY P后OUTAP（x，y，z ） 真。 12. 我们把程序的第三行与第五行为验证公式（程序 段 ）,13. 设P是程序，A与B是两个断言语句，则公式可表示为： APB 其它略 含义为：如果A执行P前A真且P的执行一定终止执行P则 执行P后B真。 14. 举例：计算两个非负且不同时为零的整数x1和x2的最大公 约数Y的程序 Program GCD 整体程序 Read（x1,X2）； 读入X1，X2 （Z1，Z2）：=（X1，X2）； 赋值Z1, Z2 Write Z10 do Z1不等于零做 If Z2Z1 then Z1= Z2- Z1 else （Z1，Z2）：=（Z2，Z1） od 其它 Y：= Z2 ； Write（y） end GCD 结束,NOTE：（Z1，Z2）：=（X1，X2）；表示将X1， X2同时赋给Z1，Z2 （Z1，Z2）：=（X2，X1）；表示交换Z1和 Z2 NOTE：X10X20（X10X20）题意要 求 NOTE：程序中y应当是X1与X2的最大公约数 NOTE：e1e2表示e1除尽e2 NOTE：MA X u a（u）表示使得a（u）成立的一切u 中的最大者 根据上述约定有：,Y=MAX u （uX1，uX2） 推出：输入输出断言的该程序是： Program GCP； Read （X1，X2） A点 X10X20（X10X20） 输入断言 （Z1，Z2）：=（X1，X2） B点 While Z10 do Do 其它 C点 Y：= Z2； y= Y=MAX u （uX1uX2） 输出断言 Write （y） End GCD NOTE：红笔部分为该程序I /O断言 NOTE：程序流程如下：,A点 A、B之间为第一段 B点,开 始,Read（X1，X2）,（Z1，Z2）：=（X1，X2）；, C点 判别Z10吗 C、C1之间为第二段 C1点 If Z2Z1 then Z2：= Z2 Z1 Else（Z1，Z2）：=( Z2, Z1） ,D点 Y：= Z2 D、E之间为第三段 E点 Write（y） 结束 该图为最大公约数的流程图,下面分三段证明 分析：1）控制达到A点时 输入断言成立 2）控制达到E点时 输出断言成立 3）问题如下：（更进一步分析） 控制达到B点、C点、D点时成立否？ （1）当控制由A点达到B点时Z1，Z2最大公约 数也是X1，X2的最大公约数且Z1，Z2也 不同时为零的非负数（根据题义）B点应 有如下断言: Z10Z2 0（Z10 Z20） MAX u （uZ1，uZ2） = MAX u （uX1，uX2）,（2）C点： 1. 可由B点到达C点 2. 可由C点经过C1点（可循环多次）在循环的过 程中Z1，Z2的值不断变化但控制达到C点时 Z1，Z2的最大公约数一直不变且正好是X1， X2的最大公约数也是Z1，Z2仍然不同时为零 的非负整数C点和B点处的断言为： Z10Z 2 0（Z10 Z20） MAX u（uZ1uZ2） = MAX u（uX1uX2）,（3）D点： 当控制达到D点时，循环已经结束Z2值应为X1， X2的最大公约数D点断言为： Z 2= MAX u（uX1u X2） Note：B，C，D为程序中间，称为中间断言 Note：C点是循环语句内部（循环体内部）且C点处 断言在循环中不变，称为不变断言，也称为不 变式。,可进一步改为： X10X20（X10X20） A、B （Z1，Z2）：=（X1，X2）； Z10Z 2 0（Z10 Z20） MAX u（uZ1uZ2） = MAX u （uX1uX2） 要注意：“1 ” 为二元谓词表示1 除尽 MAXu a（u）表示“使得a（u）成立的一切 u中最大者。”,While Z10Z 2 0（Z10 Z20） MAX u（uZ1uZ2） = MAX u（uX1uX2） B、D Z10 do If Z 2Z1 then Z2：= Z2Z1 else （Z1， Z2）：=（Z2，Z1） od, Z 2= MAX u（uX1uX2） D、E y：= Z2 y= MAX u（uX1uX2）,从流程图分为三段来证明： 我们可以将（3）式分解为（4）（5）（6）来证 明，即： 证明（A B）段（B D）段（D E）段（4） X10X20（X10X20） （Z1，Z2）：=（X1，X2）； Z10Z 2 0（Z10 Z20） MAX u（uZ1uZ2）= MAX u （uX1 uX2） 这就是流程图中（A B）段的情形,（5） Z10Z 2 0（Z10 Z20） MAX u （uZ1uZ2） = MAX u（uX1uX2） while Z10Z 2 0（Z10 Z20） MAX u （uZ1uZ2）= MAX u（uX1uX2） Z10 do If Z 2Z1 then Z2：= Z2Z1 else （Z1，Z2）：= （Z2，Z1） od Z 2= MAX u（uX1uX2） 这就是流程图中（B D）段的情形 （6） Z 2= MAX u（uX1uX2） y：= Z2 y= MAX u（uX1uX2） 这就是流程图中（D E）段的情形,（7）下面证明公式（4）即：要证明输入断言（A ，B）段 证：验证公式（4）的含义是：“如果A点处的输入断言 真，且Z1， Z2是执行（Z1，Z2）：=（x1，x2）的结 果，则B点处的断言真，”因为赋值语句把x1 Z1中与 x2Z2中所以（4）式可写成： （X10X20（X10X20） （X10 X20）（X10X20）MAX u （uX1 uX2）= MAX u（uX1uX2） 在（7）中的蕴涵式中的后件是由B点处的中间断言中x1 Z1及x2Z2所得到的. 故这个公式当然永真。 证毕。,下面证明公式（6）证明输出断言（D，E）段 证：（6）式的含义是： Z 2= MAX u （uX1 uX2）y是执行y：= Z2的结 果） y= MAX u（uX1uX2）因为执 行y：= Z2后值就是Z2，以这个式可写 成：,（8）Z 2= MAX u（uX1uX2）MAX u （uX1uX2） 其中的蕴涵式中的后件是由 E点处的输出 断言中的y换成X2 的结果，这个逻辑公式 当然永真。 证毕。 下面证明公式（5）循环语句不变断言即：（B D）段 （B C ），（C1 C ），（C D）三段 。该断言可分解为：（B C）段，故相应的（5）式也可以分解为 三个式子 证： 由流程图得到（9）式均真,（9）（Z10Z 2 0） （Z10 Z20） MAX u（uZ1uZ2）= MAX u （uX1 uX2）（Z10Z 2 0（Z10 Z20） MAX u （uZ1uZ2）= MAX u（uX1uX2） 证毕。（这是流程图中循环体中的判别部分） （10）证：（c1 c）段即：循环语句不变断言。 （Z10Z 2 0）（Z10 Z20） MAX u（uZ1uZ2） = MAX u（uX1uX2）Z10）（执 行条件语句）,If Z 2Z1 then Z2：= Z2Z1 else （Z1，Z2）：=（Z2，Z1） 后c处的断言为： （Z10Z 2 0）（Z10 Z20） MAX u（uZ1uZ2） = MAX u（uX1uX2） 根据流程图分析 Z 2Z1 有两种情形即Z 2Z1和Z1 Z 2对于Z 2Z1执行语句 Z2：= Z2Z1 执行该语句 后Z 2的值Z2：= Z2Z1所以我们有:,(10) （Z10Z 20 ）（Z10 Z10 ） MAX u（uZ1uZ2） = MAX u（uX1uX2） Z10Z2Z1 ）（Z1 0 (Z2 Z1) 0） Z10 (Z2 Z1) 0） MAX u （uZ1uZ2） = MAX u（uX1uX2） 因为Z10（Z10 （Z2 Z1）0）永真 所以 Z 2Z1Z2 Z10永真 证毕,(10) 证Z 2Z1的情形 （Z10Z 20 ）（Z10 Z 20 ） MAX u（uZ1uZ2） = MAX u（uX1uX2） （Z10Z2Z1 ） （Z 20Z10（Z 20Z10） MAX u（uZ2 u Z1） = MAX u（uX1uX2） 因为当 Z 2Z1，该条件语句执行赋值语句 （Z1，Z2）：=（Z2，Z1） 即Z1，Z2互换，所以（10）为真，又跟据(10) 与 (10)均为真所以（10）为真。 证毕,（11） 证： Z1=0，MAX u（uZ1uZ2） = MAX u（uX1uX2），Z 20 MAX u（u0uZ2） = MAX u（uX1uX2） MAX u （uZ2） = MAX u（uX1uX2） Z2 = MAX u（uX1uX2） 所以（11）永真。 全部证毕。,程序正确性方法的总结（部分） 总结：1）要将程序分段证明给出中间断言 2）给出输入输出断言 3）给出循环不变式 4）产生相应的断言语句并证明真假 5）要严格的逻辑推理 6）对所要证明的对象要深刻理解 7）将程序的断言点要合理 若证明出有一个断言为假，则程序是不正确的。,Note1：由为对循环次数不确定的证明方法目前有大 量没有解决，这需要几代人的努力。 Note2：目前在此领域较先进的是：美国、印度等。 Note3：这个领域研究进展不大。,举例：判别程序正确性 计算三角形面积C语言程序如下： 我们知道三角形面积公式为： S=（ ss（s-a）（s-b）（s-c）1/2,其中s=,#include math。h #include stodio。h Main