應(yīng)用部分程序正確性證明

應(yīng)用部分程序正確性證明第1頁，課件共42頁，創(chuàng)作于2023年2月2.數(shù)理邏輯的理論和方法在計(jì)算機(jī)理論中有如下幾方

面應(yīng)用。

1）準(zhǔn)確的理解程序

2）容易的構(gòu)造程序

3）證明程序的正確性

4）測試系統(tǒng)的可靠性

5）檢測程序中的錯(cuò)誤

6）提高程序的運(yùn)行效率

例如：信息奇偶檢測法就是數(shù)理邏輯學(xué)中完成的。

3.編譯程序中，語法上的正確及語義上的正確，

但不能保證程序的完全正確。主要原因是邏輯

上的錯(cuò)誤，而邏輯錯(cuò)誤用調(diào)試的方法是不能解

決的。第2頁，課件共42頁，創(chuàng)作于2023年2月例如：百雞百錢問題

為代碼流程

FORX=0到19

FORY=0到33

判別5X+3Y+Z=100

若滿足判別條件則打印一組X、Y、Z然后繼續(xù)循環(huán)

若不滿足判別條件則不打印該組X、Y、Z然后繼續(xù)

循環(huán)第3頁，課件共42頁，創(chuàng)作于2023年2月程序如下：

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）；

}}}

結(jié)果為公母小

02575418788118112484分析程序在語法語義均為正確而0、25、75顯然不對分析原因是邏輯錯(cuò)誤第4頁，課件共42頁，創(chuàng)作于2023年2月解決此問題方法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語句若滿足判別條件則不打印繼續(xù)循環(huán)

解決此問題方法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第5頁，課件共42頁，創(chuàng)作于2023年2月4.現(xiàn)在也有一些實(shí)驗(yàn)程序的驗(yàn)證系統(tǒng)，有許多問題還

沒有解決，有待于研究。

例如：計(jì)算機(jī)的自然語言翻譯系統(tǒng)等。

5.1）程序的正確性是指：給定任何的合法輸入→程

序最終要停止并要輸出結(jié)果正確。

2）前者稱為終止性問題，后者稱為程序的部分正

確性問題。我們只討論程序的正確性（部分）第6頁，課件共42頁，創(chuàng)作于2023年2月6.我們知道任何一個(gè)程序都是對一組數(shù)據(jù)的加工I/O

（入/出）

7.定義：設(shè)P是一個(gè)程序：

1）x1…xn

（記為x）是程序輸入數(shù)據(jù)

2）y1…yn

（記為y）是程序輸出數(shù)據(jù)

3）BODY是該程序的程序行

則可以表示為：

ProgramP：程序整體的描述（開始）

Read（x）；數(shù)據(jù)輸入部分

BODYP；程序體（數(shù)據(jù)加工部分）

Write（y）；數(shù)據(jù)輸出部分

EndP；程序整體的結(jié)束第7頁，課件共42頁，創(chuàng)作于2023年2月8.定義：輸入數(shù)據(jù)必須滿足的條件稱為程序的輸入條

件。即：輸入斷言（記為INAP（x））

9.定義：同理數(shù)據(jù)必須滿足的條件稱為程序的輸出條

件。即：輸出斷言

（記為OUAP（X，Y，Z））其中z是程序的中間數(shù)據(jù),中間數(shù)據(jù)不是最終結(jié)果。

例：計(jì)算1+2+3+……+100就有最終結(jié)果，與中間

結(jié)果。（三角數(shù)）第8頁，課件共42頁，創(chuàng)作于2023年2月根據(jù)定義程序可以描述如下：

Programp；：程序整體描述

Read（x）；：數(shù)據(jù)輸入部分

{INAP（x）；}：程序P的輸入斷言（非執(zhí)行語句）

BODYP；：程序體

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

Write（）：程序結(jié)果輸出部分（非執(zhí)行語句）

Endp：程序P的整體結(jié)束第9頁，課件共42頁，創(chuàng)作于2023年2月

NOTE：在數(shù)理邏輯中應(yīng)當(dāng)理解斷言部分。

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

目的是驗(yàn)證I/0數(shù)據(jù)是否正確，即用來證明程序的

正確性，為了區(qū)別我們用花括號(hào)括起來。第10頁，課件共42頁，創(chuàng)作于2023年2月10.程序的部分正確性證明問題可以描述為：

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

11.注意：用數(shù)理邏輯描述，對于任何x，任何y和任

何z，如果執(zhí)行BODYP（程序體）前INAP

（x）真，且BODYP執(zhí)行一定終止，則執(zhí)行

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

12.我們把程序的第三行與第五行為驗(yàn)證公式（程序

段）第11頁，課件共42頁，創(chuàng)作于2023年2月13.設(shè)P是程序，A與B是兩個(gè)斷言語句，則公式可表示為：

{A}P{B}其它略

含義為：如果A執(zhí)行P前A真且P的執(zhí)行一定終止執(zhí)行P→則

執(zhí)行P后B真。

14.舉例：計(jì)算兩個(gè)非負(fù)且不同時(shí)為零的整數(shù)x1和x2的最大公

約數(shù)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結(jié)束第12頁，課件共42頁，創(chuàng)作于2023年2月NOTE：（Z1，Z2）：=（X1，X2）；表示將X1，

X2同時(shí)賦給Z1，Z2

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

Z2

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

求

NOTE：程序中y應(yīng)當(dāng)是X1與X2的最大公約數(shù)

NOTE：e1≒e2表示e1除盡e2

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

中的最大者

根據(jù)上述約定有：第13頁，課件共42頁，創(chuàng)作于2023年2月Y=MAXu（u≒X1，∧u≒X2）

推出：輸入輸出斷言的該程序是：

ProgramGCP；

Read（X1，X2）

←A點(diǎn)

{X1≥0∧X2≥0∧（X1≠0∨X2≠0）}輸入斷言

（Z1，Z2）：=（X1，X2）

←B點(diǎn)

WhileZ1≠0do

Do其它

←C點(diǎn)

Y：=Z2；

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

輸出斷言

Write（y）

EndGCD

NOTE：紅筆部分為該程序I/O斷言

NOTE：程序流程如下：第14頁，課件共42頁，創(chuàng)作于2023年2月

A點(diǎn)

A、B之間為第一段

B點(diǎn)

開始Read（X1，X2）（Z1，Z2）：=（X1，X2）；第15頁，課件共42頁，創(chuàng)作于2023年2月↑→→→→→→C點(diǎn)

↑↓

↑判別Z1≥0嗎

↑←←←←↓→→→C、C1之間為第二段

↑↓↓

↑C1點(diǎn)↓

↑↓↓

↑IfZ2≥Z1thenZ2：=Z2—Z1

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

↑↓↓

↑↓↓

←←←←↓第16頁，課件共42頁，創(chuàng)作于2023年2月

D點(diǎn)

↓

Y：=Z2

↓D、E之間為第三段

E點(diǎn)

↓

Write（y）

↓

結(jié)束

該圖為最大公約數(shù)的流程圖第17頁，課件共42頁，創(chuàng)作于2023年2月下面分三段證明

分析：1）控制達(dá)到A點(diǎn)時(shí)→輸入斷言成立

2）控制達(dá)到E點(diǎn)時(shí)→輸出斷言成立

3）問題如下：（更進(jìn)一步分析）

控制達(dá)到B點(diǎn)、C點(diǎn)、D點(diǎn)時(shí)成立否？

（1）當(dāng)控制由A點(diǎn)達(dá)到B點(diǎn)時(shí)Z1，Z2最大公約

數(shù)也是X1，X2的最大公約數(shù)且Z1，Z2也

不同時(shí)為零的非負(fù)數(shù)（根據(jù)題義）→B點(diǎn)應(yīng)

有如下斷言:

Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）

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

=MAXu（u≒X1，∧u≒X2）第18頁，課件共42頁，創(chuàng)作于2023年2月（2）C點(diǎn)：

1.可由B點(diǎn)到達(dá)C點(diǎn)

2.可由C點(diǎn)經(jīng)過C1點(diǎn)（可循環(huán)多次）在循環(huán)的過

程中Z1，Z2的值不斷變化但控制達(dá)到C點(diǎn)時(shí)

Z1，Z2的最大公約數(shù)一直不變且正好是X1，

X2的最大公約數(shù)也是Z1，Z2仍然不同時(shí)為零

的非負(fù)整數(shù)→C點(diǎn)和B點(diǎn)處的斷言為：

Z1≥0∧Z2≥0∧（Z1≠0∨Z2≠0）

∧MAXu（u≒Z1∧u≒Z2）

=MAXu（u≒X1∧u≒X2）第19頁，課件共42頁，創(chuàng)作于2023年2月（3）D點(diǎn)：

當(dāng)控制達(dá)到D點(diǎn)時(shí)，循環(huán)已經(jīng)結(jié)束→Z2值應(yīng)為X1，

X2的最大公約數(shù)→D點(diǎn)斷言為：

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

Note：B，C，D為程序中間，稱為中間斷言

Note：C點(diǎn)是循環(huán)語句內(nèi)部（循環(huán)體內(nèi)部）且C點(diǎn)處

斷言在循環(huán)中不變，稱為不變斷言，也稱為不

變式。第20頁，課件共42頁，創(chuàng)作于2023年2月

可進(jìn)一步改為：

{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中最大者?！钡?1頁，課件共42頁，創(chuàng)作于2023年2月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）}

第22頁，課件共42頁，創(chuàng)作于2023年2月從流程圖分為三段來證明：

我們可以將（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）段的情形第23頁，課件共42頁，創(chuàng)作于2023年2月（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）段的情形第24頁，課件共42頁，創(chuàng)作于2023年2月（7）下面證明公式（4）即：要證明輸入斷言（A，B）段

證：驗(yàn)證公式（4）的含義是：“如果A點(diǎn)處的輸入斷言

真，且Z1，Z2是執(zhí)行（Z1，Z2）：=（x1，x2）的結(jié)

果，則B點(diǎn)處的斷言真，”因?yàn)橘x值語句把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）中的蘊(yùn)涵式中的后件是由B點(diǎn)處的中間斷言中x1

→Z1及x2→Z2所得到的.

故這個(gè)公式當(dāng)然永真。

證畢。

第25頁，課件共42頁，創(chuàng)作于2023年2月下面證明公式（6）證明輸出斷言（D，E）段

證：（6）式的含義是：Z2=MAXu（u≒X1

∧u≒X2）∧y是執(zhí)行y：=Z2的結(jié)

果）→

y=MAXu（u≒X1∧u≒X2））因?yàn)閳?zhí)

行y：=Z2后值就是Z2，以這個(gè)式可寫

成：第26頁，課件共42頁，創(chuàng)作于2023年2月（8）Z2=MAXu（u≒X1∧u≒X2））→MAXu

（u≒X1∧u≒X2）

其中的蘊(yùn)涵式中的后件是由E點(diǎn)處的輸出

斷言中的y換成X2

的結(jié)果，這個(gè)邏輯公式

當(dāng)然永真。

證畢。

下面證明公式（5）循環(huán)語句不變斷言即：（BD）段

（BC），（C1C），（CD）三段。該斷言可分解為：（BC）段，故相應(yīng)的（5）式也可以分解為

三個(gè)式子

證：由流程圖得到（9）式均真第27頁，課件共42頁，創(chuàng)作于2023年2月（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）

證畢。（這是流程圖中循環(huán)體中的判別部分）

（10）證：（c1c）段即：循環(huán)語句不變斷言。

（（Z1≥0∧Z2≥0）∧（Z1≠0

∨Z2≠0））∧MAXu（u≒Z1∧u≒Z2）

=MAXu（u≒X1∧u≒X2）∧Z1≠0）→（執(zhí)

行條件語句）第28頁，課件共42頁，創(chuàng)作于2023年2月

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）

根據(jù)流程圖分析Z2≥Z1

有兩種情形即Z2≥Z1和Z1

>Z2對于Z2≥Z1執(zhí)行語句Z2：=Z2—Z1

執(zhí)行該語句

后Z2的值Z2：=Z2—Z1所以我們有:第29頁，課件共42頁，創(chuàng)作于2023年2月

(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）

因?yàn)閆1≠0→（Z1≠0∨（Z2

－Z1）≠0）永真

所以Z2≥Z1→Z2—Z1≥0永真

證畢第30頁，課件共42頁，創(chuàng)作于2023年2月(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）

因?yàn)楫?dāng)Z2≥Z1，該條件語句執(zhí)行賦值語句

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

即Z1，Z2互換，所以（10``）為真，又跟據(jù)(10’)

與(10``)均為真所以（10）為真。

證畢第31頁，課件共42頁，創(chuàng)作于2023年2月（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）永真。

全部證畢。第32頁，課件共42頁，創(chuàng)作于2023年2月程序正確性方法的總結(jié)（部分）

總結(jié)：1）要將程序分段證明給出中間斷言

2）給出輸入輸出斷言

3）給出循環(huán)不變式

4）產(chǎn)生相應(yīng)的斷言語句并證明真假

5）要嚴(yán)格的邏輯推理

6）對所要證明的對象要深刻理解

7）將程序的斷言點(diǎn)要合理

若證明出有一個(gè)斷言為假，則程序是不正確的。第33頁，課件共42頁，創(chuàng)作于2023年2月Note1：由為對循環(huán)次數(shù)不確定的證明方法目前有大

量沒有解決，這需要幾代人的努力。

Note2：目前在此領(lǐng)域較先進(jìn)的是：美國、印度等。

Note3：這個(gè)領(lǐng)域研究進(jìn)展不大。第34頁，課件共42頁，創(chuàng)作于2023年2月舉例：判別程序正確性

計(jì)算三角形面積C語言程序如下：

我們知道三角形面積公式為：

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

其中s=

第35頁，課件共42頁，創(chuàng)作于2023年2月

#include?math。h?

#include?stodio。h?

Main（）

{

Floata，b，c，s，area；

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