应用部分程序正确性证明

应用部分程序正确性证明第一页，共四十二页，2022年，8月28日2.数理逻辑的理论和方法在计算机理论中有如下几方

面应用。

1）准确的理解程序

2）容易的构造程序

3）证明程序的正确性

4）测试系统的可靠性

5）检测程序中的错误

6）提高程序的运行效率

例如：信息奇偶检测法就是数理逻辑学中完成的。

3.编译程序中，语法上的正确及语义上的正确，

但不能保证程序的完全正确。主要原因是逻辑

上的错误，而逻辑错误用调试的方法是不能解

决的。第二页，共四十二页，2022年，8月28日例如：百鸡百钱问题

为代码流程

FORX=0到19

FORY=0到33

判别5X+3Y+Z=100

若满足判别条件则打印一组X、Y、Z然后继续循环

若不满足判别条件则不打印该组X、Y、Z然后继续

循环第三页，共四十二页，2022年，8月28日程序如下：

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显然不对分析原因是逻辑错误第四页，共四十二页，2022年，8月28日解决此问题方法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第五页，共四十二页，2022年，8月28日4.现在也有一些实验程序的验证系统，有许多问题还

没有解决，有待于研究。

例如：计算机的自然语言翻译系统等。

5.1）程序的正确性是指：给定任何的合法输入→程

序最终要停止并要输出结果正确。

2）前者称为终止性问题，后者称为程序的部分正

确性问题。我们只讨论程序的正确性（部分）第六页，共四十二页，2022年，8月28日6.我们知道任何一个程序都是对一组数据的加工I/O

（入/出）

7.定义：设P是一个程序：

1）x1…xn

（记为x）是程序输入数据

2）y1…yn

（记为y）是程序输出数据

3）BODY是该程序的程序行

则可以表示为：

ProgramP：程序整体的描述（开始）

Read（x）；数据输入部分

BODYP；程序体（数据加工部分）

Write（y）；数据输出部分

EndP；程序整体的结束第七页，共四十二页，2022年，8月28日8.定义：输入数据必须满足的条件称为程序的输入条

件。即：输入断言（记为INAP（x））

9.定义：同理数据必须满足的条件称为程序的输出条

件。即：输出断言

（记为OUAP（X，Y，Z））其中z是程序的中间数据,中间数据不是最终结果。

例：计算1+2+3+……+100就有最终结果，与中间

结果。（三角数）第八页，共四十二页，2022年，8月28日根据定义程序可以描述如下：

Programp；：程序整体描述

Read（x）；：数据输入部分

{INAP（x）；}：程序P的输入断言（非执行语句）

BODYP；：程序体

OUTAP{（x，y，z）}：程序P的输出断言

Write（）：程序结果输出部分（非执行语句）

Endp：程序P的整体结束第九页，共四十二页，2022年，8月28日

NOTE：在数理逻辑中应当理解断言部分。

即：{INAP（x）；}与OUTAP{（x，y，z）}

目的是验证I/0数据是否正确，即用来证明程序的

正确性，为了区别我们用花括号括起来。第十页，共四十二页，2022年，8月28日10.程序的部分正确性证明问题可以描述为：

{INAP（x）；}BODYPOUTAP{（x，y,z）}

11.注意：用数理逻辑描述，对于任何x，任何y和任

何z，如果执行BODYP（程序体）前INAP

（x）真，且BODYP执行一定终止，则执行

BODYP后OUTAP{（x，y，z）}真。

12.我们把程序的第三行与第五行为验证公式（程序

段）第十一页，共四十二页，2022年，8月28日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,,Z2

WriteZ1≠0doZ1不等于零做

IfZ2≥Z1thenZ1=Z2-Z1else（Z1，Z2）：=（Z2，Z1）

od其它

Y：=Z2

；

Write（y）

endGCD结束第十二页，共四十二页，2022年，8月28日NOTE：（Z1，Z2）：=（X1，X2）；表示将X1，

X2同时赋给Z1，Z2

（Z1，Z2）：=（X2，X1）；表示交换Z1和

Z2

NOTE：X1≥0∧X2≥0∧（X1≠0∨X2≠0）题意要

求

NOTE：程序中y应当是X1与X2的最大公约数

NOTE：e1≒e2表示e1除尽e2

NOTE：MAXua（u）表示使得a（u）成立的一切u

中的最大者

根据上述约定有：第十三页，共四十二页，2022年，8月28日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≠0do

Do其它

←C点

Y：=Z2；

{y=Y=MAXu（u≒X1∧u≒X2）}

输出断言

Write（y）

EndGCD

NOTE：红笔部分为该程序I/O断言

NOTE：程序流程如下：第十四页，共四十二页，2022年，8月28日

A点

A、B之间为第一段

B点

开始Read（X1，X2）（Z1，Z2）：=（X1，X2）；第十五页，共四十二页，2022年，8月28日↑→→→→→→C点

↑↓

↑判别Z1≥0吗

↑←←←←↓→→→C、C1之间为第二段

↑↓↓

↑C1点↓

↑↓↓

↑IfZ2≥Z1thenZ2：=Z2—Z1

↑Else（Z1，Z2）：=(Z2,Z1）

↑↓↓

↑↓↓

←←←←↓第十六页，共四十二页，2022年，8月28日

D点

↓

Y：=Z2

↓D、E之间为第三段

E点

↓

Write（y）

↓

结束

该图为最大公约数的流程图第十七页，共四十二页，2022年，8月28日下面分三段证明

分析：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）第十八页，共四十二页，2022年，8月28日（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）第十九页，共四十二页，2022年，8月28日（3）D点：

当控制达到D点时，循环已经结束→Z2值应为X1，

X2的最大公约数→D点断言为：

Z2=MAXu（u≒X1∧u≒X2）

Note：B，C，D为程序中间，称为中间断言

Note：C点是循环语句内部（循环体内部）且C点处

断言在循环中不变，称为不变断言，也称为不

变式。第二十页，共四十二页，2022年，8月28日

可进一步改为：

{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中最大者。”第二十一页，共四十二页，2022年，8月28日While{Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）∧

MAXu（u≒Z1∧u≒Z2）

=MAXu（u≒X1∧u≒X2）}

B、DZ1≠0do

IfZ2≥Z1thenZ2：=Z2—Z1else（Z1，

Z2）：=（Z2，Z1）

od

{Z2=MAXu（u≒X1∧u≒X2）}D、Ey：=Z2

{y=MAXu（u≒X1∧u≒X2）}

第二十二页，共四十二页，2022年，8月28日从流程图分为三段来证明：

我们可以将（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）段的情形第二十三页，共四十二页，2022年，8月28日（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≠0do

IfZ2≥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）段的情形第二十四页，共四十二页，2022年，8月28日（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所得到的.

故这个公式当然永真。

证毕。

第二十五页，共四十二页，2022年，8月28日下面证明公式（6）证明输出断言（D，E）段

证：（6）式的含义是：Z2=MAXu（u≒X1

∧u≒X2）∧y是执行y：=Z2的结

果）→

y=MAXu（u≒X1∧u≒X2））因为执

行y：=Z2后值就是Z2，以这个式可写

成：第二十六页，共四十二页，2022年，8月28日（8）Z2=MAXu（u≒X1∧u≒X2））→MAXu

（u≒X1∧u≒X2）

其中的蕴涵式中的后件是由E点处的输出

断言中的y换成X2

的结果，这个逻辑公式

当然永真。

证毕。

下面证明公式（5）循环语句不变断言即：（BD）段

（BC），（C1C），（CD）三段。该断言可分解为：（BC）段，故相应的（5）式也可以分解为

三个式子

证：由流程图得到（9）式均真第二十七页，共四十二页，2022年，8月28日（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）→（执

行条件语句）第二十八页，共四十二页，2022年，8月28日

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和Z1

>Z2对于Z2≥Z1执行语句Z2：=Z2—Z1

执行该语句

后Z2的值Z2：=Z2—Z1所以我们有:第二十九页，共四十二页，2022年，8月28日

(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永真

证毕第三十页，共四十二页，2022年，8月28日(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）∧MAX

u（u≒Z2∧u≒Z1）

=MAXu（u≒X1∧u≒X2）

因为当Z2≥Z1，该条件语句执行赋值语句

（Z1，Z2）：=（Z2，Z1）

即Z1，Z2互换，所以（10``）为真，又跟据(10’)

与(10``)均为真所以（10）为真。

证毕第三十一页，共四十二页，2022年，8月28日（11）

证：

Z1=0，MAXu（u≒Z1∧u≒Z2）

=MAXu（u≒X1∧u≒X2），Z2＞0

├MAXu（u≒0∧u≒Z2）

=MAXu（u≒X1∧u≒X2）

├MAXu（u≒Z2）

=MAXu（u≒X1∧u≒X2）

├Z2=MAXu（u≒X1∧u≒X2）

所以（11）永真。

全部证毕。第三十二页，共四十二页，2022年，8月28日程序正确性方法的总结（部分）

总结：1）要将程序分段证明给出中间断言

2）给出输入输出断言

3）给出循环不变式

4）产生相应的断言语句并证明真假

5）要严格的逻辑推理

6）对所要证明的对象要深刻理解

7）将程序的断言点要合理

若证明出有一个断言为假，则程序是不正确的。第三十三页，共四十二页，2022年，8月28日Note1：由为对循环次数不确定的证明方法目前有大

量没有解决，这需要几代人的努力。

Note2：目前在此领域较先进的是：美国、印度等。

Note3：这个领域研究进展不大。第三十四页，共四十二页，2022年，8月28日举例：判别程序正确性

计算三角形面积C语言程序如下：

我们知道三角形面积公式为：

S=（s×s（s-a）×（s-b）×（s-c））1/2

其中s=

第三十五页，共四十二页，2022年，8月28日

#include‹math。h›

#include‹stodio。h›

Main（）

{

Floata，b，c，s，area；

Scanf（“%f，%f，%f”&a，&b，&c