《電子技術應用》
您所在的位置:首頁 > 其他 > 設計應用 > 循環(huán)結構的形式化推導
循環(huán)結構的形式化推導
來源:微型機與應用2014年第5期
李賢貞1,2,,吳茂念1,,楊 靜1
(1.貴州大學 計算機科學與信息學院,貴州 貴陽 550025,; 2.中國科學院國家天文臺,,北京 1
摘要: 介紹了Dijkstra的形式化推導方法的主要思想、步驟及要點,。該方法主張程序開發(fā)和程序證明同時進行,,先確定好描述程序功能的斷言,再通過形式化方法推導出正確的程序,。選擇具有代表性的循環(huán)結構的實例進行推導證明,,并對循環(huán)結構的形式化推導進行闡述說明。
Abstract:
Key words :

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

 算法是計算機科學的核心,,而算法的正確性是近幾年討論的熱點問題,,但是效果并不明顯。一般情況下,,程序的正確性都是針對已經(jīng)編好的程序,,通過測試用例,盡可能地找出程序的漏洞,,但這種方法并不能從根本上保證程序的正確性,。采用形式化的方法[1]來進行設計程序,是先將需要解決的問題精確描述出來,,再根據(jù)某種形式化規(guī)則進行推理,,最終得到正確且結構化的程序。目前存在很多種形式化方法,,Dijkstra的最弱前置條件程序推導,;英國愛丁堡大學的Burstall和Darlington所研制的ZAP系統(tǒng);基于公理語義的Z,;基于指稱語義的VDM,;基于抽象機的B方法;江西師范大學提出的PAR(Partition And Recur)方法[2-5]等,。
 如果能找出一套形式化方法,,實現(xiàn)程序的自動化開發(fā)和證明,將使得開發(fā)周期大大縮短,,降低程序開發(fā)的成本,也將不再有后期維護的后顧之憂,。Dijkstra主張程序開發(fā)和程序證明同時進行,,屬于半自動化的形式化方法[6]。需要人為地找出確定描述程序功能的斷言,、循環(huán)不變式以及t函數(shù),。若能提出某種方法實現(xiàn)此過程的自動化,將有望找出自動化的形式化推導,。
1 形式化推導的基本思想
1.1 {Q}S{R}系統(tǒng)

 設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í)行,。

 



 嚴格按照形式化推導的方式開發(fā)得出循環(huán)結構,,保證了此程序的完全正確性。
 本文簡要介紹了Dijkstra的最弱前置條件程序推導方法,,并通過開發(fā)并證明任意正整數(shù)的階乘來說明此方法的步驟及其要點,。此例子中,需要人為地尋找出后置條件R,、循環(huán)不變式P,、以及t函數(shù)。自動化的方式推導出R,,P或t函數(shù)可以作為下一步的研究課題,。而自動化生成正確的程序是一個長期性的國際難題,是一項富有創(chuàng)造性和挑戰(zhàn)性的活動,,值得進一步研究更多的算法,,尋找形式化推導的一般規(guī)律,盡可能將創(chuàng)造性勞動變?yōu)榉莿?chuàng)造性勞動,,使形式化方法走出實驗室,,給工程程序的開發(fā)帶來幫助。
參考文獻
[1] 唐稚松,,林惠民.功能描述導引的程序綜合[M].北京:中國學術期刊電子出版社,,1983.
[2] 石海鶴,薛錦云.基于PAR的算法形式化開發(fā)[J].計算機學報,,2009,,32(5):982-991.
[3] 王昕,,袁超偉.一種安全協(xié)議的形式化分析方法[J].計算機工程,2010,,36(7):82-84.
[4] 楊晨,,薛錦云,蘇昭.三個經(jīng)典數(shù)學問題的形式化開發(fā)[J].計算機與現(xiàn)代化,,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] 雷富興,張來順,,石榮剛,,等.循環(huán)條件的形式化推導在程序驗證中的應用[J].計算機工程與設計,2010,,31(14):3193-1397.

此內(nèi)容為AET網(wǎng)站原創(chuàng),,未經(jīng)授權禁止轉(zhuǎn)載。