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

《应用部分、程序正确性证明.ppt》由会员分享，可在线阅读，更多相关《应用部分、程序正确性证明.ppt（42页珍藏版）》请在三一办公上搜索。

1、第六章 应用部分、程序正确性证明1.前面命题演算和谓词演算重要的是利用其概念建立 了命题及谓词的公理系统。1）矛盾性 2）永真性 这些问题表面上看来都是比较抽象，好象是无实用 价值，其实则不然。,2.数理逻辑的理论和方法在计算机理论中有如下几方 面应用。1）准确的理解程序 2）容易的构造程序 3）证明程序的正确性 4）测试系统的可靠性 5）检测程序中的错误 6）提高程序的运行效率 例如：信息奇偶检测法就是数理逻辑学中完成的。3.编译程序中，语法上的正确及语义上的正确，但不能保证程序的完全正确。主要原因是逻辑 上的错误，而逻辑错误用调试的方法是不能解 决的。,例如：百鸡百钱问题 为代码流程 FO

2、R 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

3、）+（*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=20For（y=0；y=33；y+）语句y=0改为 y=1，y=33改为y=33,4.现在也有一些实验程序的验证系统，有许多问题还 没有解决，有待于研究。例如：计算机的自然语言翻译系统等。5.1）程序的正确性是指：给定任何的合法输入程 序最终要停止并要输出结果正确。2）前者称为终止性问题，后者称为程序的部分

4、正 确性问题。我们只讨论程序的正确性（部分）,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）

5、其中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.程序的部分正确性证明问

6、题可以描述为：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（

7、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和 Z2NOTE：X10X20（X10X20）题意要 求 NOTE：程序中y应当是X1与X2的最大公约数NOTE：e1e2表示e1除尽e2NOTE：MA X u a（u）表示使得a（u）成立的一切u 中的最大者根据上述约定有：,Y=MAX

8、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,

9、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的值不断变化但控

10、制达到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

11、 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）X10X

12、20（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=

13、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）式的含义

14、是：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

15、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：=Z2

16、Z1 执行该语句 后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

17、 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）对所要证明的对象要深刻理解

18、 7）将程序的断言点要合理若证明出有一个断言为假，则程序是不正确的。,Note1：由为对循环次数不确定的证明方法目前有大 量没有解决，这需要几代人的努力。Note2：目前在此领域较先进的是：美国、印度等。Note3：这个领域研究进展不大。,举例：判别程序正确性 计算三角形面积C语言程序如下：我们知道三角形面积公式为：S=（ss（s-a）（s-b）（s-c）1/2,其中s=,#include math。h#include stodio。h Main（）Float a，b，c，s，area；Scanf（“%f，%f，%f”&a，&b，&c）；A点 s=area=sqrt（s（s-a）（s-b）（s

19、-c）；printf（“%f“，area）；B点,为程序逻辑完全正确 A点 If（a+b）c（a+c）b（b+c）a）B点 Else printf（“it is not area”）；即：设p：（a+b）c Y：（a+c）b R：（b+c）a 若pqr为真时推出 A=（p，q，r）的指派为（T，T，T）才执行程序否则不执行程序。,举例：程序的正确性判别（这里是程序化简问题）有 一高级语言的条件语句为（ALGOL语言）If A then if B then x Tlse Y tlse if B then x else Y 将其条件语句用逻辑学来化简,解：该程序的流程图如下：,A,B,B,X,Y,F,T,F,T,T,F,1）此段程序执行X条件为：A B AB 2）执行Y条件为：A BAB 3）我将1）与2）化简 即：将A B AB 化简=BABA 根据PQ=QP=B（AA）根据P（QR）=（PQ）（PR）=BT=T B=B,将 A BAB 化简=BABA 根据PQ=QP=B（AA）根据P（QR）=（PQ）（PR）=BT=TB=B 根据逻辑化简流程图为：,B,X,Y,T,F,故简化为 if then x else y,