第六章 应用部分、程序正确性证明

第六章应用部分、程序正确性证明1.前面命题演算和谓词演算重要的是利用其概念建立了命题及谓词的公理系统。1）矛盾性2）永真性这些问题表面上看来都是比较抽象，好象是无实用价值，其实则不然。2.数理逻辑的理论和方法在计算机理论中有如下几方面应用。1）准确的理解程序2）容易的构造程序3）证明程序的正确性4）测试系统的可靠性5）检测程序中的错误6）提高程序的运行效率例如：信息奇偶检测法就是数理逻辑学中完成的。3.编译程序中，语法上的正确及语义上的正确，但不能保证程序的完全正确。主要原因是逻辑上的错误，而逻辑错误用调试的方法是不能解决的。例如：百鸡百钱问题为代码流程FORX=0到19FORY=0到33判别5X+3Y+Z=100若满足判别条件则打印一组X、Y、Z然后继续循环若不满足判别条件则不打印该组X、Y、Z然后继续循环程序如下：Main（）{Intx，y，z；For（x=0；x‹=19；x++）{For（y=0；y‹=33；y++）{Z=100-x-y；If（（（5*x）+（3*y）+（*z）==100Printf（“%d%d%d“，x，y，z）；}}}结果为公母小02575418788118112484分析程序在语法语义均为正确而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）x1…xn（记为x）是程序输入数据2）y1…yn（记为y）是程序输出数据3）BODY是该程序的程序行则可以表示为：ProgramP：程序整体的描述（开始）Read（x）；数据输入部分BODYP；程序体（数据加工部分）Write（y）；数据输出部分EndP；程序整体的结束8.定义：输入数据必须满足的条件称为程序的输入条件。即：输入断言（记为INAP（x））9.定义：同理数据必须满足的条件称为程序的输出条件。即：输出断言（记为OUAP（X，Y，Z））其中z是程序的中间数据,中间数据不是最终结果。例：计算1+2+3+……+100就有最终结果，与中间结果。（三角数）根据定义程序可以描述如下：Programp；：程序整体描述Read（x）；：数据输入部分{INAP（x）；}：程序P的输入断言（非执行语句）BODYP；：程序体OUTAP{（x，y，z）}：程序P的输出断言Write（）：程序结果输出部分（非执行语句）Endp：程序P的整体结束NOTE：在数理逻辑中应当理解断言部分。即：{INAP（x）；}与OUTAP{（x，y，z）}目的是验证I/0数据是否正确，即用来证明程序的正确性，为了区别我们用花括号括起来。10.程序的部分正确性证明问题可以描述为：{INAP（x）；}BODYPOUTAP{（x，y,z）}11.注意：用数理逻辑描述，对于任何x，任何y和任何z，如果执行BODYP（程序体）前INAP（x）真，且BODYP执行一定终止，则执行BODYP后OUTAP{（x，y，z）}真。12.我们把程序的第三行与第五行为验证公式（程序段）13.设P是程序，A与B是两个断言语句，则公式可表示为：{A}P{B}其它略含义为：如果A执行P前A真且P的执行一定终止执行P→则执行P后B真。14.举例：计算两个非负且不同时为零的整数x1和x2的最大公约数Y的程序ProgramGCD整体程序Read（x1,X2）；读入X1，X2（Z1，Z2）：=（X1，X2）；赋值Z1,,Z2WriteZ1≠0doZ1不等于零做IfZ2≥Z1thenZ1=Z2-Z1else（Z1，Z2）：=（Z2，Z1）od其它Y：=Z2；Write（y）endGCD结束NOTE：（Z1，Z2）：=（X1，X2）；表示将X1，X2同时赋给Z1，Z2（Z1，Z2）：=（X2，X1）；表示交换Z1和Z2NOTE：X1≥0∧X2≥0∧（X1≠0∨X2≠0）题意要求NOTE：程序中y应当是X1与X2的最大公约数NOTE：e1≒e2表示e1除尽e2NOTE：MAXua（u）表示使得a（u）成立的一切u中的最大者根据上述约定有：Y=MAXu（u≒X1，∧u≒X2）推出：输入输出断言的该程序是：ProgramGCP；Read（X1，X2）←A点{X1≥0∧X2≥0∧（X1≠0∨X2≠0）}输入断言（Z1，Z2）：=（X1，X2）←B点WhileZ1≠0doDo其它←C点Y：=Z2；{y=Y=MAXu（u≒X1∧u≒X2）}输出断言Write（y）EndGCDNOTE：红笔部分为该程序I/O断言NOTE：程序流程如下：A点A、B之间为第一段B点开始Read（X1，X2）（Z1，Z2）：=（X1，X2）；↑→→→→→→C点↑↓↑判别Z1≥0吗↑←←←←↓→→→C、C1之间为第二段↑↓↓↑C1点↓↑↓↓↑IfZ2≥Z1thenZ2：=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点应有如下断言:Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1，∧u≒Z2）=MAXu（u≒X1，∧u≒X2）（2）C点：1.可由B点到达C点2.可由C点经过C1点（可循环多次）在循环的过程中Z1，Z2的值不断变化但控制达到C点时Z1，Z2的最大公约数一直不变且正好是X1，X2的最大公约数也是Z1，Z2仍然不同时为零的非负整数→C点和B点处的断言为：Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）（3）D点：当控制达到D点时，循环已经结束→Z2值应为X1，X2的最大公约数→D点断言为：Z2=MAXu（u≒X1∧u≒X2）Note：B，C，D为程序中间，称为中间断言Note：C点是循环语句内部（循环体内部）且C点处断言在循环中不变，称为不变断言，也称为不变式。可进一步改为：{X1≥0∧X2≥0∧（X1≠0∨X2≠0）}A、B（Z1，Z2）：=（X1，X2）；{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）}要注意：“ｅ1≒ｅ２”为二元谓词表示ｅ1除尽ｅ２MAXua（u）表示“使得a（u）成立的一切u中最大者。”While{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）}B、DZ1≠0doIfZ2≥Z1thenZ2：=Z2—Z1else（Z1，Z2）：=（Z2，Z1）od{Z2=MAXu（u≒X1∧u≒X2）}D、Ey：=Z2{y=MAXu（u≒X1∧u≒X2）}从流程图分为三段来证明：我们可以将（3）式分解为（4）（5）（6）来证明，即：证明（AB）段（BD）段（DE）段（4）{X1≥0∧X2≥0∧（X1≠0∨X2≠0）}（Z1，Z2）：=（X1，X2）；{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）}这就是流程图中（AB）段的情形（5）{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）while{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）}Z1≠0doIfZ2≥Z1thenZ2：=Z2—Z1else（Z1，Z2）：=（Z2，Z1）od{Z2=MAXu（u≒X1∧u≒X2）}这就是流程图中（BD）段的情形（6）{Z2=MAXu（u≒X1∧u≒X2）}y：=Z2{y=MAXu（u≒X1∧u≒X2）}这就是流程图中（DE）段的情形（7）下面证明公式（4）即：要证明输入断言（A，B）段证：验证公式（4）的含义是：“如果A点处的输入断言真，且Z1，Z2是执行（Z1，Z2）：=（x1，x2）的结果，则B点处的断言真，”因为赋值语句把x1→Z1中与x2→Z2中所以（4）式可写成：（X1≥0∧X2≥0∧（X1≠0∨X2≠0））→（（X1≥0∧X2≥0）∧（X1≠0∨X2≠0）∧MAXu（u≒X1∧u≒X2））=MAXu（u≒X1∧u≒X2）在（7）中的蕴涵式中的后件是由B点处的中间断言中x1→Z1及x2→Z2所得到的.故这个公式当然永真。证毕。下面证明公式（6）证明输出断言（D，E）段证：（6）式的含义是：Z2=MAXu（u≒X1∧u≒X2）∧y是执行y：=Z2的结果）→y=MAXu（u≒X1∧u≒X2））因为执行y：=Z2后值就是Z2，以这个式可写成：（8）Z2=MAXu（u≒X1∧u≒X2））→MAXu（u≒X1∧u≒X2）其中的蕴涵式中的后件是由E点处的输出断言中的y换成X2的结果，这个逻辑公式当然永真。证毕。下面证明公式（5）循环语句不变断言即：（BD）段（BC），（C1C），（CD）三段。该断言可分解为：（BC）段，故相应的（5）式也可以分解为三个式子证：由流程图得到（9）式均真（9）（Z1≥0∧Z2≥0）∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2））→（（Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0））∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）证毕。（这是流程图中循环体中的判别部分）（10）证：（c1c）段即：循环语句不变断言。（（Z1≥0∧Z2≥0）∧（Z1≠0∨Z2≠0））∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）∧Z1≠0）→（执行条件语句）IfZ2≥Z1thenZ2：=Z2—Z1else（Z1，Z2）：=（Z2，Z1）后c处的断言为：（Z1≥0∧Z2≥0）∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）根据流程图分析Z2≥Z1有两种情形即Z2≥Z1和Z1Z2对于Z2≥Z1执行语句Z2：=Z2—Z1执行该语句后Z2的值Z2：=Z2—Z1所以我们有:(10’)（Z1≥0∧Z2≥0）∧（Z1≠0∨Z1≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）∧Z1≠0∧Z2≥Z1）→（Z1≥0∧(Z2—Z1)≥0）Z1≠0∨(Z2—Z1)≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）因为Z1≠0→（Z1≠0∨（Z2－Z1）≠0）永真所以Z2≥Z1→Z2—Z1≥0永真证毕(10``)证Z2＜Z1的情形（Z1≥0∧Z2≥0）∧（Z1≠0∨Z2≠0）∧MAXu（u≒Z1∧u≒Z2）=MAXu（u≒X1∧u≒X2）∧（Z1≠0∧Z2﹤Z1）→（Z2≥0∧Z1≥0∧（Z2≠0∨Z1≠0）∧MAXu（u≒Z2∧u≒Z1）=MAXu（u≒X1∧u≒X2）因为当Z2≥Z1，该条件语句执行赋值语句（Z1，Z2）：=（Z2，Z1）即Z1，Z2互换，所以（10``）为真，又跟据(10’)与(10`