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

　　摘 要：程序正確性與可信性是各類計算機系統中最重要的核心問題。在開展“C程序設計”課程雙語教學、以及精品在線開放課程建設的實踐中，培養計算思維的意識和能力是核心任務。本文選擇體現計算思維本質特征的“自然數階乘算法”這個典型程序為抓手，透過程序調試與測試的表象，直擊程序正確性與可信性的核心，通過程序的完全正確性證明，為開展計算思維的形式化方法教育、培養視野及思維開闊的國際化人才，進行了有益的實踐。

　　關鍵詞：階乘算法;程序正確性;形式化證明;計算思維;雙語教學

　　1 引言

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

　　計算思維被認為是數學邏輯思維、物理實證思維后的第三種思維方式，由美國計算機科學家周以真教授首次提出[3]：計算思維是與形式化問題及其解決方法相關的思維過程，是運用計算機科學的基礎概念進行問題求解、系統設計、以及人類行為理解等思維活動，根本特征是抽象和自動化。形式化方法用嚴格的符號系統和數學模型描述和驗證一個目標軟件系統的行為和特性[4]，使用嚴格精確的數學語言、無二義的語法語義，以及一組定義其語法語義的形式化規則，采用嚴謹的演繹推理法完成邏輯分析和證明。

　　程序設計課程是培養計算思維最有效的工具。中國九校(首批“985工程”建設高校)聯盟在計算機基礎教學發展戰略聯合聲明中，把培養計算思維能力作為計算機基礎教學的核心任務[5]。而自然數的階乘算法，可用“循環結構”與“遞歸函數”兩種程序實現，體現了計算思維中“自動化”的本質特征，成為培養計算思維能力的最好抓手。

　　2 程序正確性概述

　　程序的正確性是衡量一個程序正常工作的基本條件。然而，程序所描述的動態計算過程是無法直接用程序本身的靜態結構進行正確性證明。因此，程序含有錯誤是難免的。為盡量減少錯誤[6]，首先應使用結構化程序設計方法，并在程序調試時采用軟件測試的方法去跟蹤程序的運行，從而發現與改正錯誤，但更重要的是采用程序正確性證明的理論進行證明。

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

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

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

　　(2)程序終止：若對于每個使Pre(i)為真的輸入i，程序P的計算都終止，則稱程序P關于Pre是終止的。

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

　　一個程序的完全正確，等價于該程序是部分正確，同時又是終止的。

　　3 自然數階乘算法的遞歸實現及正確性證明

　　自然數階乘的C語言遞歸程序P如下[1]：

　　int fact( int n )

　　{

　　int x = 1;

　　if ( n > 0 )

　　x = n * fact(n-1);

　　return x;

　　}

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

　　4 自然數階乘算法的循環實現及正確性證明

　　自然數階乘的C語言循環程序P如下[1]：

　　int fact( int y )

　　{

　　int x = 1;

　　while ( y > 0 )

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

　　return x;

　　}

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

　　采用Hoare邏輯三元組描述程序為：

　　[ 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)

　　根據賦值公理，用 x 代替 y × x 可得到以下表達式：

　　[ y > 0 ( y × x ) × (y - 1)! = n! ] x = y * x [ y > 0 x × (y - 1)! = n! ] (4-3)

　　由式(4-2)和式(4-3)利用結論規則，可得

　　[ 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)利用順序規則，可得

　　[ y > 0 x × y! = n! ] x = y * x， y = y - 1 [ y ≥ 0 x × y! = n! ] (4-6)

　　根據式(4-6)，利用循環規則中 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 x = 1 → x × y! = n! (4-8)

　　由式(4-7)和式(4-8)利用結論規則，可得

　　[ y ≥ 0 y = n x = 1] while (y > 0) x = y * x， y = y - 1 [ y≥0 x × y! = n! y≤0 ] (4-9)

　　又因為 0! = 1，所以

　　y ≥ 0 x × y! = n! y ≤ 0 → y=0 x × y! = n! → x = n! (4-10)

　　由式(4-9)和式(4-10)利用結論規則，可得

　　[ y ≥ 0 y = n x = 1 ] while ( y > 0 ) x = y * x， y = y - 1 [ x = n! ] (4-11)

　　根據賦值公理可得

　　[ y≥0 y = n] x = 1 [ y≥0 y = n x = 1 ] (4-12)

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

　　[ y ≥ 0 y = n ] x = 1; while ( y > 0 ) x = y * x， y = y - 1 [ x = n! ] (4-13)

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

　　② 再用 Kruth計數器方法證明程序終止性。

　　選取 N(y) = y

　　輸入斷言： I(y)： y > 0

　　當第一次進入循環時有 y > 0

　　根據程序算法容易看出：循環體內始終滿足 y > 0，于是就有N(y) > 0;

　　而每執行一次循環，N(y)是遞減的;

　　因而，循環只能執行有限次，必定終止，程序的終止性得證。

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

　　5 結語

　　計算思維的形式化方法能夠嚴格分析、處理、證明程序及其性質，對于確保程序正確性和提高可信性具有基礎性的作用。當前，形式化方法教育已在歐美教育界進行了相關的實踐，因此我國高校計算機教育強調計算思維的同時，更要注重其內涵形式化方法的教育作用。

　　參考文獻：

　　[1] Paul Kelly等，雙語版C程序設計[M]， 2017，電子工業出版社

　　[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]. 軟件學報， 2019， 30(01)：33-61.

　　[5] 何欽銘等.計算機基礎教學的核心任務是計算思維能力的培養[J].中國大學教學，2010(9)： 5-9.

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