李賢貞 ，吳茂念 ，楊 靜

（1.貴州大學(xué) 計算機科學(xué)與信息學(xué)院，貴州 貴陽 550025；2.中國科學(xué)院國家天文臺，北京 100012）

算法是計算機科學(xué)的核心，而算法的正確性是近幾年討論的熱點問題，但是效果并不明顯。一般情況下，程序的正確性都是針對已經(jīng)編好的程序，通過測試用例，盡可能地找出程序的漏洞，但這種方法并不能從根本上保證程序的正確性。采用形式化的方法[1]來進行設(shè)計程序，是先將需要解決的問題精確描述出來，再根據(jù)某種形式化規(guī)則進行推理，最終得到正確且結(jié)構(gòu)化的程序。目前存在很多種形式化方法，Dijkstra的最弱前置條件程序推導(dǎo)；英國愛丁堡大學(xué)的Burstall和Darlington所研制的ZAP系統(tǒng)；基于公理語義的Z；基于指稱語義的VDM；基于抽象機的B方法；江西師范大學(xué)提出的PAR（Partition And Recur）方法[2-5]等。

如果能找出一套形式化方法，實現(xiàn)程序的自動化開發(fā)和證明，將使得開發(fā)周期大大縮短，降低程序開發(fā)的成本，也將不再有后期維護的后顧之憂。Dijkstra主張程序開發(fā)和程序證明同時進行，屬于半自動化的形式化方法[6]。需要人為地找出確定描述程序功能的斷言、循環(huán)不變式以及t函數(shù)。若能提出某種方法實現(xiàn)此過程的自動化，將有望找出自動化的形式化推導(dǎo)。

1 形式化推導(dǎo)的基本思想

1.1 {Q}S{R}系統(tǒng)

設(shè)S是一個程序語句，S的前斷言為Q，后斷言為R，記法{Q}S{R}表示如果在 S執(zhí)行之前謂詞Q為真，那么在S執(zhí)行之后謂詞R也真[7]。

1.2 最弱前置條件 wp（S，R）

對于給定的程序S，wp（S，R）是一個狀態(tài)集合，以該集合中任一狀態(tài)作為初始狀態(tài)執(zhí)行程序S都能保證程序終止且滿足后置條件R；反之，能使程序終止，且終止狀態(tài)滿足后置條件 R的初始狀態(tài)必屬于 wp（S，R）所定義的狀態(tài)集合。即對程序S來說，wp（S，R）是屬于后置條件R的最弱前置條件。

1.3 空語句

“skip”表示空語句，即什么都不執(zhí)行。

即對于任意的后置條件R，其空語句下的最弱前置條件也為R。

1.4 賦值語句

賦值語句的語句形式x：=E，指變量x被表達式E所替換。

即對于任意的后置條件R，其賦值語句下的最弱前置條件是將R中所有出現(xiàn)的x都用E來代替。

1.5 分號語句

分號語句的語句形式 S1；S2，指先激活 S1，執(zhí)行結(jié)束后再激活 S2，如式（3）：

即對于任意的后置條件R，其分號語句下的最弱前置條件為R在S2下的最弱前置條件作為S1的后置條件，再在S1下的最弱前置條件。

1.6 選擇語句

“IF”表示選擇語句。語句形式如下：

其中 B1，B2，…，Bn都是警衛(wèi)，選擇所有警衛(wèi)為真的其中一個 Bi，執(zhí)行 SLi語句體，然后 IF終止。

1.7 循環(huán)語句

“DO”表示循環(huán)語句。語句形式如下：

其中 B1，B2，…，Bn都是警衛(wèi)，如果 Bi為真，則執(zhí)行SLi語句體，循環(huán)執(zhí)行，直至所有的警衛(wèi)為假，則循環(huán)終止。

1.8 循環(huán)結(jié)構(gòu)的基本原理

若

則

其中P為循環(huán)不變式[8]，即循環(huán)執(zhí)行之前 P為真，且每次循環(huán)重復(fù)執(zhí)行之后還為真。

1.9 t函數(shù)

t函數(shù)是一個整型函數(shù)，且需滿足以下條件：

即如果BB滿足t＞0，且衛(wèi)式命令的每次執(zhí)行都會使得t至少減1，則程序是可終止的。

2 循環(huán)結(jié)構(gòu)形式化推導(dǎo)的一般步驟

（1）對于給定的實際問題，經(jīng)過分析用形式化的方法寫出后置條件R，找出循環(huán)不變式P，以及保證程序終止的函數(shù)t。

（2）由于終止條件時必須滿足后置條件R，即從而找出警衛(wèi)BB，即循環(huán)結(jié)構(gòu)的條件。

（3）根據(jù)循環(huán)不變式P和后置條件R尋找可行的初始化條件。

（4）根據(jù)循環(huán)結(jié)構(gòu)的基本原理，由

得出循環(huán)體和Bj。

3 用形式化推導(dǎo)過程求任意正整數(shù)的階乘

（1）用變量W來存最后求得的值。則后置條件

因為程序必須滿足所有的正整數(shù)，如果不采用循環(huán)語句就很難看出R是如何得到的。所以需尋求一個循環(huán)不變式，最好能比較容易建立，而最終又要有（P and non BB）=＞R。選擇一個稍弱于 R的式子，也就是得到終態(tài)的一個泛化。而泛化一個式子的典型做法就是用一個變量來代替一個常量，所以用變量j來代替常量n，并加入變量范圍，則循環(huán)不變式

而t函數(shù)每次都需單調(diào)遞減，可設(shè)t函數(shù)：

（2）由循環(huán)不變式P和后置條件R可得出：

則

（3）為了驗證這個P是否有效，首先必須有一個比較易行的方式來開始。由

則初始化為

（4）由于式（14）、式（15），則

結(jié)合式（16），可知t函數(shù)滿足了式（9）。

為了保證t至少減 1，可以讓j加 1，那么W就要乘以（j+1），則

所以

則滿足循環(huán)結(jié)構(gòu)基本原理的前提條件式（6），再由

則

即

從而得出了BB

（5）程序段為：

嚴格按照形式化推導(dǎo)的方式開發(fā)得出循環(huán)結(jié)構(gòu)，保證了此程序的完全正確性。

本文簡要介紹了Dijkstra的最弱前置條件程序推導(dǎo)方法，并通過開發(fā)并證明任意正整數(shù)的階乘來說明此方法的步驟及其要點。此例子中，需要人為地尋找出后置條件R、循環(huán)不變式P、以及t函數(shù)。自動化的方式推導(dǎo)出R，P或t函數(shù)可以作為下一步的研究課題。而自動化生成正確的程序是一個長期性的國際難題，是一項富有創(chuàng)造性和挑戰(zhàn)性的活動，值得進一步研究更多的算法，尋找形式化推導(dǎo)的一般規(guī)律，盡可能將創(chuàng)造性勞動變?yōu)榉莿?chuàng)造性勞動，使形式化方法走出實驗室，給工程程序的開發(fā)帶來幫助。

[1]唐稚松，林惠民.功能描述導(dǎo)引的程序綜合[M].北京：中國學(xué)術(shù)期刊電子出版社，1983.

[2]石海鶴，薛錦云.基于 PAR的算法形式化開發(fā)[J].計算機學(xué)報，2009，32（5）：982-991.

[3]王昕，袁超偉.一種安全協(xié)議的形式化分析方法[J].計算機工程，2010，36（7）：82-84.

[4]楊晨，薛錦云，蘇昭.三個經(jīng)典數(shù)學(xué)問題的形式化開發(fā)[J].計算機與現(xiàn)代化，2010，180（8）：1-4.

[5]王昌晶，薛錦云.算法及其時間復(fù)雜度可同步形式化推導(dǎo)的方法[J].計算機應(yīng)用研究，2008，25（3）：681-683.

[6]WYBE D E.A Discipline of programming[M].America，1976.

[7]楊帆，翟巖慧，曲開社，等.基于形式概念分析的詞義解釋研究[J].計算機科學(xué)，2011，38（10）：189-191.

[8]雷富興，張來順，石榮剛，等.循環(huán)條件的形式化推導(dǎo)在程序驗證中的應(yīng)用 [J].計算機工程與設(shè)計，2010，31（14）：3193-1397.