摘  要： 介紹了Dijkstra的形式化推導(dǎo)方法的主要思想,、步驟及要點(diǎn)。該方法主張程序開發(fā)和程序證明同時(shí)進(jìn)行,，先確定好描述程序功能的斷言,，再通過形式化方法推導(dǎo)出正確的程序。選擇具有代表性的循環(huán)結(jié)構(gòu)的實(shí)例進(jìn)行推導(dǎo)證明,，并對(duì)循環(huán)結(jié)構(gòu)的形式化推導(dǎo)進(jìn)行闡述說明,。
關(guān)鍵詞： 形式化方法；程序正確性,；循環(huán)不變式,；界函數(shù)

　算法是計(jì)算機(jī)科學(xué)的核心，而算法的正確性是近幾年討論的熱點(diǎn)問題,，但是效果并不明顯,。一般情況下，程序的正確性都是針對(duì)已經(jīng)編好的程序,，通過測(cè)試用例,，盡可能地找出程序的漏洞，但這種方法并不能從根本上保證程序的正確性,。采用形式化的方法[1]來進(jìn)行設(shè)計(jì)程序,，是先將需要解決的問題精確描述出來，再根據(jù)某種形式化規(guī)則進(jìn)行推理,，最終得到正確且結(jié)構(gòu)化的程序,。目前存在很多種形式化方法，Dijkstra的最弱前置條件程序推導(dǎo),；英國愛丁堡大學(xué)的Burstall和Darlington所研制的ZAP系統(tǒng),；基于公理語義的Z；基于指稱語義的VDM,；基于抽象機(jī)的B方法,；江西師范大學(xué)提出的PAR（Partition And Recur）方法[2-5]等,。
　如果能找出一套形式化方法，實(shí)現(xiàn)程序的自動(dòng)化開發(fā)和證明,，將使得開發(fā)周期大大縮短,，降低程序開發(fā)的成本，也將不再有后期維護(hù)的后顧之憂,。Dijkstra主張程序開發(fā)和程序證明同時(shí)進(jìn)行,，屬于半自動(dòng)化的形式化方法[6]。需要人為地找出確定描述程序功能的斷言,、循環(huán)不變式以及t函數(shù),。若能提出某種方法實(shí)現(xiàn)此過程的自動(dòng)化，將有望找出自動(dòng)化的形式化推導(dǎo),。
1 形式化推導(dǎo)的基本思想
1.1 {Q}S{R}系統(tǒng)
　設(shè)S是一個(gè)程序語句,，S的前斷言為Q，后斷言為R,，記法{Q}S{R}表示如果在S執(zhí)行之前謂詞Q為真,，那么在S執(zhí)行之后謂詞R也真[7]。
1.2 最弱前置條件wp（S,，R）
　對(duì)于給定的程序S,，wp（S，R）是一個(gè)狀態(tài)集合,，以該集合中任一狀態(tài)作為初始狀態(tài)執(zhí)行程序S都能保證程序終止且滿足后置條件R,；反之，能使程序終止,，且終止?fàn)顟B(tài)滿足后置條件R的初始狀態(tài)必屬于wp（S,，R）所定義的狀態(tài)集合。即對(duì)程序S來說,，wp（S,，R）是屬于后置條件R的最弱前置條件。
1.3 空語句
　“skip”表示空語句,，即什么都不執(zhí)行。

　嚴(yán)格按照形式化推導(dǎo)的方式開發(fā)得出循環(huán)結(jié)構(gòu),，保證了此程序的完全正確性,。
　本文簡要介紹了Dijkstra的最弱前置條件程序推導(dǎo)方法，并通過開發(fā)并證明任意正整數(shù)的階乘來說明此方法的步驟及其要點(diǎn),。此例子中,，需要人為地尋找出后置條件R、循環(huán)不變式P,、以及t函數(shù),。自動(dòng)化的方式推導(dǎo)出R,，P或t函數(shù)可以作為下一步的研究課題。而自動(dòng)化生成正確的程序是一個(gè)長期性的國際難題,，是一項(xiàng)富有創(chuàng)造性和挑戰(zhàn)性的活動(dòng),，值得進(jìn)一步研究更多的算法，尋找形式化推導(dǎo)的一般規(guī)律,，盡可能將創(chuàng)造性勞動(dòng)變?yōu)榉莿?chuàng)造性勞動(dòng),，使形式化方法走出實(shí)驗(yàn)室，給工程程序的開發(fā)帶來幫助,。
參考文獻(xiàn)
[1] 唐稚松,，林惠民.功能描述導(dǎo)引的程序綜合[M].北京：中國學(xué)術(shù)期刊電子出版社，1983.
[2] 石海鶴,，薛錦云.基于PAR的算法形式化開發(fā)[J].計(jì)算機(jī)學(xué)報(bào),，2009，32（5）：982-991.
[3] 王昕,，袁超偉.一種安全協(xié)議的形式化分析方法[J].計(jì)算機(jī)工程,，2010，36（7）：82-84.
[4] 楊晨,，薛錦云,，蘇昭.三個(gè)經(jīng)典數(shù)學(xué)問題的形式化開發(fā)[J].計(jì)算機(jī)與現(xiàn)代化，2010,，180（8）：1-4.
[5] 王昌晶,，薛錦云.算法及其時(shí)間復(fù)雜度可同步形式化推導(dǎo)的方法[J].計(jì)算機(jī)應(yīng)用研究，2008,，25（3）：681-683.
[6] WYBE D E. A Discipline of programming[M]. America,，1976.
[7] 楊帆，翟巖慧,，曲開社,，等.基于形式概念分析的詞義解釋研究[J].計(jì)算機(jī)科學(xué)，2011,，38（10）：189-191.
[8] 雷富興,，張來順，石榮剛,，等.循環(huán)條件的形式化推導(dǎo)在程序驗(yàn)證中的應(yīng)用[J].計(jì)算機(jī)工程與設(shè)計(jì),，2010，31（14）：3193-1397.