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

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

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

　　1 引言

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

　　計(jì)算思維被認(rèn)為是數(shù)學(xué)邏輯思維、物理實(shí)證思維后的第三種思維方式，由美國計(jì)算機(jī)科學(xué)家周以真教授首次提出[3]：計(jì)算思維是與形式化問題及其解決方法相關(guān)的思維過程，是運(yùn)用計(jì)算機(jī)科學(xué)的基礎(chǔ)概念進(jì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é)語言、無二義的語法語義，以及一組定義其語法語義的形式化規(guī)則，采用嚴(yán)謹(jǐn)?shù)难堇[推理法完成邏輯分析和證明。

　　程序設(shè)計(jì)課程是培養(yǎng)計(jì)算思維最有效的工具。中國九校(首批“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ì)算過程是無法直接用程序本身的靜態(tài)結(jié)構(gòu)進(jìn)行正確性證明。因此，程序含有錯(cuò)誤是難免的。為盡量減少錯(cuò)誤[6]，首先應(yīng)使用結(jié)構(gòu)化程序設(shè)計(jì)方法，并在程序調(diào)試時(shí)采用軟件測試的方法去跟蹤程序的運(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表示問題求解的實(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語言遞歸程序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語言循環(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)

　　由此可見：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é)語

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

　　參考文獻(xiàn)：

　　[1] Paul Kelly等，雙語版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].中國大學(xué)教學(xué)，2010(9)： 5-9.

　　推薦閱讀：如何投稿軟件測試方面論文