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

《应用部分、程序正确性证明》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

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

2、FORY=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（

3、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）前者称为终止性问题，后者称为程序的部分正确性问题。我

4、们只讨论程序的正确性（部分）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是程序的中间

5、数据,中间数据不是最终结果。例：计算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.程序的部分正确性证明问题可以描

6、述为：{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（Z

7、1，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的最大公约