自然數(shù)階乘算法程序正確性的形式化證明

梁元貞 林燕芬 耿江濤

摘 要：程序正確性與可信性是各類計(jì)算機(jī)系統(tǒng)中最重要的核心問(wèn)題。在開(kāi)展“C程序設(shè)計(jì)”課程雙語(yǔ)教學(xué)、以及精品在線開(kāi)放課程建設(shè)的實(shí)踐中，培養(yǎng)計(jì)算思維的意識(shí)和能力是核心任務(wù)。本文選擇體現(xiàn)計(jì)算思維本質(zhì)特征的“自然數(shù)階乘算法”這個(gè)典型程序?yàn)樽ナ郑高^(guò)程序調(diào)試與測(cè)試的表象，直擊程序正確性與可信性的核心，通過(guò)程序的完全正確性證明，為開(kāi)展計(jì)算思維的形式化方法教育、培養(yǎng)視野及思維開(kāi)闊的國(guó)際化人才，進(jìn)行了有益的實(shí)踐。

關(guān)鍵詞：階乘算法;程序正確性;形式化證明;計(jì)算思維;雙語(yǔ)教學(xué)

1 引言

實(shí)施雙語(yǔ)教學(xué)，是“互聯(lián)網(wǎng)+”及智能時(shí)代培養(yǎng)國(guó)際化人才的重要舉措。廣州涉外學(xué)院發(fā)揮“涉外”特色優(yōu)勢(shì)，采用愛(ài)爾蘭都柏林工業(yè)大學(xué)Paul Kelly編著的中國(guó)教育部雙語(yǔ)教學(xué)示范教材[1]，在計(jì)算機(jī)應(yīng)用及軟件技術(shù)專業(yè)強(qiáng)化雙語(yǔ)教學(xué)，取得顯著成效[2]。在進(jìn)一步開(kāi)展“雙語(yǔ)C程序設(shè)計(jì)”精品在線開(kāi)放課程的建設(shè)實(shí)踐中，更需要注重將“計(jì)算思維”的意識(shí)培養(yǎng)和方法應(yīng)用貫穿人才培養(yǎng)和實(shí)踐教學(xué)的全過(guò)程。

計(jì)算思維被認(rèn)為是數(shù)學(xué)邏輯思維、物理實(shí)證思維后的第三種思維方式，由美國(guó)計(jì)算機(jī)科學(xué)家周以真教授首次提出[3]：計(jì)算思維是與形式化問(wèn)題及其解決方法相關(guān)的思維過(guò)程，是運(yùn)用計(jì)算機(jī)科學(xué)的基礎(chǔ)概念進(jìn)行問(wèn)題求解、系統(tǒng)設(shè)計(jì)、以及人類行為理解等思維活動(dòng)，根本特征是抽象和自動(dòng)化。形式化方法用嚴(yán)格的符號(hào)系統(tǒng)和數(shù)學(xué)模型描述和驗(yàn)證一個(gè)目標(biāo)軟件系統(tǒng)的行為和特性[4]，使用嚴(yán)格精確的數(shù)學(xué)語(yǔ)言、無(wú)二義的語(yǔ)法語(yǔ)義，以及一組定義其語(yǔ)法語(yǔ)義的形式化規(guī)則，采用嚴(yán)謹(jǐn)?shù)难堇[推理法完成邏輯分析和證明。

程序設(shè)計(jì)課程是培養(yǎng)計(jì)算思維最有效的工具。中國(guó)九校（首批“985工程”建設(shè)高校）聯(lián)盟在計(jì)算機(jī)基礎(chǔ)教學(xué)發(fā)展戰(zhàn)略聯(lián)合聲明中，把培養(yǎng)計(jì)算思維能力作為計(jì)算機(jī)基礎(chǔ)教學(xué)的核心任務(wù)[5]。而自然數(shù)的階乘算法，可用“循環(huán)結(jié)構(gòu)”與“遞歸函數(shù)”兩種程序?qū)崿F(xiàn)，體現(xiàn)了計(jì)算思維中“自動(dòng)化”的本質(zhì)特征，成為培養(yǎng)計(jì)算思維能力的最好抓手。

2 程序正確性概述

程序的正確性是衡量一個(gè)程序正常工作的基本條件。然而，程序所描述的動(dòng)態(tài)計(jì)算過(guò)程是無(wú)法直接用程序本身的靜態(tài)結(jié)構(gòu)進(jìn)行正確性證明。因此，程序含有錯(cuò)誤是難免的。為盡量減少錯(cuò)誤[6]，首先應(yīng)使用結(jié)構(gòu)化程序設(shè)計(jì)方法，并在程序調(diào)試時(shí)采用軟件測(cè)試的方法去跟蹤程序的運(yùn)行，從而發(fā)現(xiàn)與改正錯(cuò)誤，但更重要的是采用程序正確性證明的理論進(jìn)行證明。

然而，這些早期的奠基性工作仍有很多不足之處[4]，在應(yīng)用中異常繁瑣且較難掌握。但其中采用形式化方法構(gòu)建正確及可信的程序，則有利于提高計(jì)算思維能力，便于從理論上指導(dǎo)設(shè)計(jì)出正確的程序。

程序規(guī)約是對(duì)程序所實(shí)現(xiàn)功能的精確描述，是程序正確性的判斷依據(jù)，由程序的前置斷言和后置斷言兩部分組成。前置斷言是程序執(zhí)行前的輸入應(yīng)滿足的條件，用一階邏輯公式Pre表示。后置斷言是程序執(zhí)行后的輸出應(yīng)滿足的條件，用一階邏輯公式Post表示。若用P表示問(wèn)題求解的實(shí)現(xiàn)程序，則程序規(guī)約可用Floyd-Hoare邏輯公式表示為{Pre}P{Post}，根據(jù)此邏輯表達(dá)式的布爾值，對(duì)程序正確性做以下定義：

（1）部分正確：若對(duì)于每個(gè)使Pre（i）為真，且能使程序P計(jì)算終止的輸入信息i，Post（i，P（i））都為真，則稱程序P關(guān)于Pre和Post是部分正確的。

（2）程序終止：若對(duì)于每個(gè)使Pre（i）為真的輸入i，程序P的計(jì)算都終止，則稱程序P關(guān)于Pre是終止的。

（3）完全正確：若對(duì)于每個(gè)使Pre（i）為真的輸入信息i，程序P的計(jì)算都將終止，并且Post（i，P（i））都為真，則稱程序P關(guān)于Pre和Post是完全正確的。

一個(gè)程序的完全正確，等價(jià)于該程序是部分正確，同時(shí)又是終止的。

3 自然數(shù)階乘算法的遞歸實(shí)現(xiàn)及正確性證明

自然數(shù)階乘的C語(yǔ)言遞歸程序P如下[1]：

int fact（ int n ）

{

int x = 1;

if （ n > 0 ）

x = n * fact（n-1）;

return x;

}

證：使用廣義數(shù)學(xué)歸納法，容易證明程序正確，此處從略。

4 自然數(shù)階乘算法的循環(huán)實(shí)現(xiàn)及正確性證明

自然數(shù)階乘的C語(yǔ)言循環(huán)程序P如下[1]：

int fact（ int y ）

{

int x = 1;

while （ y > 0 ）

x = y * x， y = y-1;

return x;

}

證：① 首先使用Hoare公理法證明程序部分正確性。

采用Hoare邏輯三元組描述程序?yàn)椋?/p>

[ y ≥ 0 ?y = n ] ?F ?[x = n！] （4-1）

由此可見(jiàn)：P： y ≥ 0 ?y = n

Q： x = n！

首先， y > 0 ?x × y！ = n！ ?→ ?y > 0 ?（ y × x ） × （y - 1）！ = n！ ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? （4-2）

根據(jù)賦值公理，用 x 代替 y × x 可得到以下表達(dá)式：

[ y > 0 ?（ y × x ） × （y - 1）！ = n！ ] ?x = y * x ?[ y > 0 ?x × （y - 1）！ = n！ ] ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? （4-3）

由式（4-2）和式（4-3）利用結(jié)論規(guī)則，可得

[ y > 0 ?x × y！ = n！ ] ?x = y * x ?[ y > 0 ?x × （y - 1）！ = n！ ] ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? （4-4）

同理，由賦值公理可得

[ y > 0 ?x × （y - 1）！ = n！ ] ?y = y - 1 ?[ y ≥ 0 ?x × y！ = n！ ] ? ? ? ? ? ? ? ? ? ? （4-5）

由式（4-4）和式（4-5）利用順序規(guī)則，可得

[ y > 0 ?x × y！ = n！ ] ?x = y * x， y = y - 1 ?[ y ≥ 0 ?x × y！ = n！ ] （4-6）

根據(jù)式（4-6），利用循環(huán)規(guī)則中 P = y > 0 ?x × y！ = n！，R = y > 0，可得

[y ≥ 0 ?x × y！ = n！ ] ?while （y>0） x = y * x， y = y - 1 [ y≥0 ?x × y！ = n！ ?y≤0 ] （4-7）

因?yàn)?y = n ?x = 1 ?→ ?x × y！ = n！ （4-8）

由式（4-7）和式（4-8）利用結(jié)論規(guī)則，可得

[ y ≥ 0 ?y = n ?x = 1] while （y > 0） x = y * x， y = y - 1 [ y≥0 ?x × y！ = n！ ?y≤0 ] （4-9）

又因?yàn)?0！ = 1，所以

y ≥ 0 ?x × y！ = n！ ?y ≤ 0 ?→ ?y=0 ?x × y！ = n！ ?→ ?x = n！ ? ? （4-10）

由式（4-9）和式（4-10）利用結(jié)論規(guī)則，可得

[ y ≥ 0 ?y = n ?x = 1 ] ?while （ y > 0 ） ?x = y * x， y = y - 1 ?[ x = n！ ] （4-11）

根據(jù)賦值公理可得

[ y≥0 ?y = n] ?x = 1 ?[ y≥0 ?y = n ?x = 1 ] ? （4-12）

最后，由式（4-11）和式（4-12）利用順序規(guī)則，可得

[ y ≥ 0 ?y = n ] ?x = 1; ?while （ y > 0 ） ?x = y * x， y = y - 1 ?[ x = n！ ] （4-13）

可以看出，式（4-13）和式（4-1）相同且成立，程序的部分正確性得證。

② 再用 Kruth計(jì)數(shù)器方法證明程序終止性。

選取 N（y） = y

輸入斷言： I（y）： y > 0

當(dāng)?shù)谝淮芜M(jìn)入循環(huán)時(shí)有 y > 0

根據(jù)程序算法容易看出：循環(huán)體內(nèi)始終滿足 y > 0，于是就有N（y） > 0;

而每執(zhí)行一次循環(huán)，N（y）是遞減的;

因而，循環(huán)只能執(zhí)行有限次，必定終止，程序的終止性得證。

完全正確性：綜合上述證明，程序是部分正確的且也是終止的，故程序是完全正確的。

5 結(jié)語(yǔ)

計(jì)算思維的形式化方法能夠嚴(yán)格分析、處理、證明程序及其性質(zhì)，對(duì)于確保程序正確性和提高可信性具有基礎(chǔ)性的作用。當(dāng)前，形式化方法教育已在歐美教育界進(jìn)行了相關(guān)的實(shí)踐，因此我國(guó)高校計(jì)算機(jī)教育強(qiáng)調(diào)計(jì)算思維的同時(shí)，更要注重其內(nèi)涵形式化方法的教育作用。

參考文獻(xiàn)：

[1] Paul Kelly等，雙語(yǔ)版C程序設(shè)計(jì)[M]， 2017，電子工業(yè)出版社

[2]Jiangtao Geng etc. Research on Speeding up the Internationalization of Private High Vocational Education[J].International Journal of Technology Management 2017（4）：7-9

[3] Jeannette M. Wing. Computational Thinking[J]. Communication of the ACM. 2006， 49，（3）：33-35.

[4] 王戟等. 形式化方法概貌[J]. 軟件學(xué)報(bào)， 2019， 30（01）：33-61.

[5] 何欽銘等.計(jì)算機(jī)基礎(chǔ)教學(xué)的核心任務(wù)是計(jì)算思維能力的培養(yǎng)[J].中國(guó)大學(xué)教學(xué)，2010（9）： 5-9.

[6] 馬曉星等. 軟件開(kāi)發(fā)方法發(fā)展回顧與展望[J]. 軟件學(xué)報(bào)， 2019， 30（01）：3-21.

作者簡(jiǎn)介：

梁元貞（1983.12-），女，講師，碩士，廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院計(jì)算機(jī)應(yīng)用教研室主任。研究方向：雙語(yǔ)教學(xué)、課程研究、計(jì)算機(jī)課程教學(xué)。

林燕芬（1974.7-），女，助理研究員，廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院高教研究室。研究方向：高職教育研究、精品課程建設(shè)。

*通訊作者：耿江濤（1965.12-），男，副教授，高級(jí)工程師，華南師范大學(xué)博士生，廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院華文與國(guó)際教育學(xué)院院長(zhǎng)。研究方向：大數(shù)據(jù)應(yīng)用技術(shù)、高職教育國(guó)際化、雙語(yǔ)教學(xué)。

基金項(xiàng)目：1.廣東省教育廳2017年度廣東省特色創(chuàng)新項(xiàng)目“粵港合作背景下高職院校國(guó)際化人才培養(yǎng)研究”（項(xiàng)目編號(hào)：2017GWTSCX061）階段性成果 2.廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院2018年校級(jí)質(zhì)量工程重點(diǎn)項(xiàng)目“廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院精品在線開(kāi)放課程管理與建設(shè)研究”（項(xiàng)目編號(hào)：SWZL201807）成果 3.廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院2019年校級(jí)質(zhì)量工程重點(diǎn)項(xiàng)目“基于大數(shù)據(jù)智慧教育平臺(tái)的計(jì)算機(jī)課程雙語(yǔ)教學(xué)改革的實(shí)踐研究”（項(xiàng)目編號(hào)：SWZL2019008）成果 4.廣州涉外經(jīng)濟(jì)職業(yè)技術(shù)學(xué)院2019年校級(jí)教研重點(diǎn)項(xiàng)目“基于學(xué)者網(wǎng)平臺(tái)構(gòu)建對(duì)分課堂模式實(shí)施程序設(shè)計(jì)課程的雙語(yǔ)教學(xué)改革”（項(xiàng)目編號(hào)：2019JY01）成果