摘 要： 介紹了Dijkstra的形式化推導方法的主要思想、步驟及要點。該方法主張程序開發和程序證明同時進行，先確定好描述程序功能的斷言，再通過形式化方法推導出正確的程序。選擇具有代表性的循環結構的實例進行推導證明，并對循環結構的形式化推導進行闡述說明。
關鍵詞： 形式化方法；程序正確性；循環不變式；界函數
算法是計算機科學的核心，而算法的正確性是近幾年討論的熱點問題，但是效果并不明顯。一般情況下，程序的正確性都是針對已經編好的程序，通過測試用例，盡可能地找出程序的漏洞，但這種方法并不能從根本上保證程序的正確性。采用形式化的方法[1]來進行設計程序，是先將需要解決的問題精確描述出來，再根據某種形式化規則進行推理，最終得到正確且結構化的程序。目前存在很多種形式化方法，Dijkstra的最弱前置條件程序推導；英國愛丁堡大學的Burstall和Darlington所研制的ZAP系統；基于公理語義的Z；基于指稱語義的VDM；基于抽象機的B方法；江西師范大學提出的PAR（Partition And Recur）方法[2-5]等。
如果能找出一套形式化方法，實現程序的自動化開發和證明，將使得開發周期大大縮短，降低程序開發的成本，也將不再有后期維護的后顧之憂。Dijkstra主張程序開發和程序證明同時進行，屬于半自動化的形式化方法[6]。需要人為地找出確定描述程序功能的斷言、循環不變式以及t函數。若能提出某種方法實現此過程的自動化，將有望找出自動化的形式化推導。
1 形式化推導的基本思想
1.1 {Q}S{R}系統
設S是一個程序語句，S的前斷言為Q，后斷言為R，記法{Q}S{R}表示如果在S執行之前謂詞Q為真，那么在S執行之后謂詞R也真[7]。
1.2 最弱前置條件wp（S，R）
對于給定的程序S，wp（S，R）是一個狀態集合，以該集合中任一狀態作為初始狀態執行程序S都能保證程序終止且滿足后置條件R；反之，能使程序終止，且終止狀態滿足后置條件R的初始狀態必屬于wp（S，R）所定義的狀態集合。即對程序S來說，wp（S，R）是屬于后置條件R的最弱前置條件。
1.3 空語句
“skip”表示空語句，即什么都不執行。
嚴格按照形式化推導的方式開發得出循環結構，保證了此程序的完全正確性。
本文簡要介紹了Dijkstra的最弱前置條件程序推導方法，并通過開發并證明任意正整數的階乘來說明此方法的步驟及其要點。此例子中，需要人為地尋找出后置條件R、循環不變式P、以及t函數。自動化的方式推導出R，P或t函數可以作為下一步的研究課題。而自動化生成正確的程序是一個長期性的國際難題，是一項富有創造性和挑戰性的活動，值得進一步研究更多的算法，尋找形式化推導的一般規律，盡可能將創造性勞動變為非創造性勞動，使形式化方法走出實驗室，給工程程序的開發帶來幫助。
參考文獻
[1] 唐稚松，林惠民.功能描述導引的程序綜合[M].北京：中國學術期刊電子出版社，1983.
[2] 石海鶴，薛錦云.基于PAR的算法形式化開發[J].計算機學報，2009，32（5）：982-991.
[3] 王昕，袁超偉.一種安全協議的形式化分析方法[J].計算機工程，2010，36（7）：82-84.
[4] 楊晨，薛錦云，蘇昭.三個經典數學問題的形式化開發[J].計算機與現代化，2010，180（8）：1-4.
[5] 王昌晶，薛錦云.算法及其時間復雜度可同步形式化推導的方法[J].計算機應用研究，2008，25（3）：681-683.
[6] WYBE D E. A Discipline of programming[M]. America，1976.
[7] 楊帆，翟巖慧，曲開社，等.基于形式概念分析的詞義解釋研究[J].計算機科學，2011，38（10）：189-191.
[8] 雷富興，張來順，石榮剛，等.循環條件的形式化推導在程序驗證中的應用[J].計算機工程與設計，2010，31（14）：3193-1397.