应用部分、程序正确性证明.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=20For（y=0；y=33；y+）语句y=0 改为 y=1，y=33改为y=334.现在也有一些实验程序的验证系统，有许多问题还 没有解决，有待于研究。例如：计算机的自然语言翻译系统等。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和 Z2NOTE：X10 X20（X10 X20）题意要 求 NOTE：程序中y应当是X1与X2的最大公约数NOTE：e1e2表示e1除尽e2NOTE：MA X u a（u）表示使得a（u）成立的一切u 中的最大者根据上述约定有：Y=MAX u（u X1，u X2）推出：输入输出断言的该程序是：Program GCP；Read（X1，X2）A 点 X10 X20（X10 X20）输入断言（Z1，Z2）：=（X1，X2）B 点 While Z10 do Do 其它 C 点 Y：=Z2；y=Y=MAX u（u X1u X2）输出断言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 点应 有如下断言:Z10 Z2 0（Z10 Z20）MAX u（u Z1，u Z2）=MAX u（u X1，u X2）（2）C 点：1.可由B 点到达C 点 2.可由C 点经过C1点（可循环多次）在循环的过 程中Z1，Z2的值不断变化但控制达到C 点时 Z1，Z2的最大公约数一直不变且正好是X1，X2的最大公约数也是Z1，Z2仍然不同时为零 的非负整数C 点和B 点处的断言为：Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）（3）D 点：当控制达到D 点时，循环已经结束Z2值应为X1，X2的最大公约数D 点断言为：Z 2=MAX u（u X1u X2）Note：B，C，D 为程序中间，称为中间断言Note：C 点是循环语句内部（循环体内部）且C 点处 断言在循环中不变，称为不变断言，也称为不 变式。可进一步改为：X10 X20（X10 X20）A、B（Z1，Z2）：=（X1，X2）；Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）要注意：“1”为二元谓词表示1 除尽 MAXu a（u）表示“使得a（u）成立的一切 u 中最大者。”While Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）B、D Z10 do If Z 2Z1 then Z2：=Z2Z1 else（Z1，Z2）：=（Z2，Z1）od Z 2=MAX u（u X1u X2）D、E y：=Z2 y=MAX u（u X1u X2）从流程图分为三段来证明：我们可以将（3）式分解为（4）（5）（6）来证 明，即：证明（A B）段（B D）段（D E）段（4）X10 X20（X10 X20）（Z1，Z2）：=（X1，X2）；Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1 u X2）这就是流程图中（A B）段的情形（5）Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）while Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）Z10 do If Z 2Z1 then Z2：=Z2Z1 else（Z1，Z2）：=（Z2，Z1）od Z 2=MAX u（u X1u X2）这就是流程图中（B D）段的情形（6）Z 2=MAX u（u X1u X2）y：=Z2 y=MAX u（u X1u X2）这就是流程图中（D E）段的情形（7）下面证明公式（4）即：要证明输入断言（A，B）段 证：验证公式（4）的含义是：“如果A 点处的输入断言 真，且Z1，Z2是执行（Z1，Z2）：=（x1，x2）的结 果，则B 点处的断言真，”因为赋值语句把x1 Z1中与 x2Z2中所以（4）式可写成：（X10 X20（X10 X20）（X10 X20）（X10 X20）MAX u（u X1 u X2）=MAX u（u X1u X2）在（7）中的蕴涵式中的后件是由B 点处的中间断言中x1 Z1及x2Z2所得到的.故这个公式当然永真。证毕。下面证明公式（6）证明输出断言（D，E）段 证：（6）式的含义是：Z 2=MAX u（u X1 u X2）y是执行y：=Z2的结 果）y=MAX u（u X1u X2）因为执 行y：=Z2后值就是Z2，以这个式可写 成：（8）Z 2=MAX u（u X1u X2）MAX u（u X1u X2）其中的蕴涵式中的后件是由 E 点处的输出 断言中的y换成X2 的结果，这个逻辑公式 当然永真。证毕。下面证明公式（5）循环语句不变断言即：（B D）段（B C），（C1 C），（C D）三段。该断言可分解为：（B C）段，故相应的（5）式也可以分解为 三个式子 证：由流程图得到（9）式均真（9）（Z10 Z 2 0）（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1 u X2）（Z10 Z 2 0（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）证毕。（这是流程图中循环体中的判别部分）（10）证：（c1 c）段即：循环语句不变断言。（Z10 Z 2 0）（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）Z10）（执 行条件语句）If Z 2Z1 then Z2：=Z2Z1 else（Z1，Z2）：=（Z2，Z1）后c处的断言为：（Z10 Z 2 0）（Z10 Z20）MAX u（u Z1u Z2）=MAX u（u X1u X2）根据流程图分析 Z 2Z1 有两种情形即Z 2Z1和Z1 Z 2对于Z 2Z1执行语句 Z2：=Z2Z1 执行该语句 后Z 2的值Z2：=Z2Z1所以我们有:(10)（Z10 Z 20）（Z10 Z10）MAX u（u Z1u Z2）=MAX u（u X1u X2）Z10 Z2Z1）（Z1 0(Z2 Z1)0）Z10(Z2 Z1)0）MAX u（u Z1u Z2）=MAX u（u X1u X2）因为Z10（Z10（Z2 Z1）0）永真 所以 Z 2Z1Z2 Z10 永真 证毕(10)证Z 2Z1的情形（Z10 Z 20）（Z10 Z 20）MAX u（u Z1u Z2）=MAX u（u X1u X2）（Z10 Z2Z1）（Z 20 Z10（Z 20 Z10）MAX u（u Z2 u Z1）=MAX u（u X1u X2）因为当 Z 2Z1，该条件语句执行赋值语句（Z1，Z2）：=（Z2，Z1）即Z1，Z2互换，所以（10）为真，又跟据(10)与(10)均为真所以（10）为真。证毕（11）证：Z1=0，MAX u（u Z1u Z2）=MAX u（u X1u X2），Z 20 MAX u（u 0 u Z2）=MAX u（u X1u X2）MAX u（u Z2）=MAX u（u X1u X2）Z2=MAX u（u X1u X2）所以（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（）Float a，b，c，s，area；Scanf（“%f，%f，%f”&a，&b，&c）；A 点 s=area=sqrt（s（s-a）（s-b）（s-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 若p q r 为真时推出 A=（p，q，r）的指派为（T，T，T）才执行程序否则不执行程序。举例：程序的正确性判别（这里是程序化简问题）有 一高级语言的条件语句为（ALGOL 语言）If A then if B then x Tlse Y tlse if B then x else Y 将其条件语句用逻辑学来化简 解：该程序的流程图如下：ABBXY FT F TT F 1）此段程序执行X 条件为：A B A B 2）执行Y 条件为：A B A B 3）我将1）与2）化简 即：将A B A B 化简=B A B A 根据P Q=Q P=B（A A）根据P（Q R）=（P Q）（P R）=B T=T B=B 将 A B A B 化简=B A B A 根据P Q=Q P=B（A A）根据P（Q R）=（P Q）（P R）=B T=T B=B 根据逻辑化简流程图为：BXYTF故简化为 if then x else y