算法及其時間復(fù)雜度可同步形式化推導(dǎo)的方法

摘要：對在長期的算法研究中提出的PAR方法和PAR平臺引入時間謂詞加以擴(kuò)展，不僅可以形式化推導(dǎo)出順序查找和二分查找問題的算法程序，而且這兩個問題關(guān)于時間復(fù)雜度的遞歸方程式也可同步且自然地推導(dǎo)得到。這為開發(fā)并驗證高效率的算法開辟了一條新途徑。

關(guān)鍵詞：分劃遞推方法;形式化推導(dǎo);時間復(fù)雜度;遞歸方程式

中圖分類號：TP301．6文獻(xiàn)標(biāo)志碼：A

文章編號：1001－3695(2008)03－0681－03

對一個具體問題要編寫一個正確的算法不是一件容易的事。Knuth在“The art of computer programming:sorting and searching”中提到，第一個二分搜索算法早在1946年就出現(xiàn)了，但是第一個完全正確的二分搜索算法卻直到1962年才出現(xiàn)。Bentley也在“Writing correct program”中提到，90%的計算機(jī)專家不能在2 h內(nèi)寫出完全正確的二分搜索算法[1]。因此現(xiàn)有的眾多算法設(shè)計與分析、數(shù)據(jù)結(jié)構(gòu)、程序設(shè)計語言教科書中很多算法不能保證完全正確。究其原因，在這些教科書中，對算法的設(shè)計與時間復(fù)雜度分析都是分開進(jìn)行的，一般都是通過半形式化語言（如偽語言）來描述算法設(shè)計過程，最后用某一可執(zhí)行語言來實現(xiàn)；通過自然語言對時間復(fù)雜度進(jìn)行描述與分析，最后歸結(jié)為一個遞歸方程式。兩者都沒有通過嚴(yán)格證明，不能讓人們信服。

筆者通過對傳統(tǒng)算法設(shè)計方法和許多實際問題的長期深入研究，提出了一種統(tǒng)一而有效的算法程序設(shè)計方法——PAR方法[2，3]。它利用一階謂詞邏輯表示功能規(guī)約，使用的主要技術(shù)是分劃和遞推，故也稱做分劃遞推法。使用PAR方法能夠形式化地從規(guī)約逐步推導(dǎo)出算法程序。更進(jìn)一步，在PAR方法中加入關(guān)于時間的謂詞，可以形式化推導(dǎo)出關(guān)于時間復(fù)雜度的遞歸方程式。筆者提出的方法創(chuàng)新點在于既能夠令人信服地形式化推導(dǎo)出算法，又能夠同步地形式化推導(dǎo)出該算法關(guān)于時間復(fù)雜度的遞歸方程式。

E. C.R.Hehner等人[1]提出一種實用的算法程序設(shè)計理論，在形式化算法設(shè)計中最早加入關(guān)于時間的謂詞。但是其理論有兩點與本文不同：a）Hehner的理論是在算法設(shè)計過程中邊猜想邊驗證，對每一個具體問題要作具體分析；PAR方法是一種統(tǒng)一的算法設(shè)計方法，對每一個具體問題使用的主要技術(shù)都是分劃和遞推。算法不是猜想出來的，而是通過在一系列一階謂詞變換規(guī)則上作變換推導(dǎo)而得來的，推導(dǎo)算法的過程即是構(gòu)造證明的過程。b）Hehner的理論算法設(shè)計過程與算法時間復(fù)雜度分析過程不是同步展開的。

1PAR方法開發(fā)步驟

a)用Radl語言精確地描述求解問題的功能規(guī)約〈Q，R〉；

b)將需求解的問題分劃成若干與原問題結(jié)構(gòu)相同但規(guī)模更小的子問題，分解可繼續(xù)直至每個子問題能直接求解;

c)構(gòu)造問題求解序列的遞推關(guān)系Si=F(j)，并給出遞推關(guān)系中出現(xiàn)的函數(shù)和變量初始化條件，再將所有初始化條件和遞推關(guān)系合并成一個算法;

d)基于文獻(xiàn)[4]中提出的循環(huán)不變式的新定義和新策略構(gòu)造循環(huán)不變式;

e)基于所得的算法和循環(huán)不變式開發(fā)Apla算法程序；

f)將Alpa算法程序通過自動化工具轉(zhuǎn)換成等價的某一可執(zhí)行語言程序，如Java、C#、VB.NET、C++、Delphi。

2引入時間謂詞

定義1計算步是一條語句或一組語句的一次執(zhí)行。

一次循環(huán)的迭代和一次遞歸程序的遞歸調(diào)用都可以認(rèn)為是一個計算步。

定義2遞推時間度量是對時間的抽象，它并不度量實際的執(zhí)行時間，其優(yōu)點在于不必了解實現(xiàn)細(xì)節(jié)。在遞推時間度量中規(guī)定：a)每一個計算步花費(fèi)一個時間單位；b）其余執(zhí)行不花時間。

這種度量方法忽略了順序和分支程序的執(zhí)行時間， 只考慮循環(huán)和遞歸程序的執(zhí)行時間。

定義3遞歸方程式用來對算法時間復(fù)雜度進(jìn)行分析。若使用分劃遞推法將規(guī)模為n的問題分成k個規(guī)模為n/m的子問題。假定解規(guī)模為1的問題耗費(fèi)1個單位時間，再設(shè)將原問題分解為k個子問題以及將k個子問題的解合并為原問題的解需要f(n)個單位時間。用T（n）表示解規(guī)模為n的問題所需的計算時間，則有遞歸方程式為

在此可以在PAR方法中引入時間。只需要在后置斷言R中加入一個關(guān)于時間的謂詞：t(n)=a(j:0≤j＜n:1)。其中：a為一常量；t(n)的含義是算法所需花費(fèi)的單位時間，它能刻畫時間依算法的變化規(guī)律。假設(shè)原來的后置斷言R為謂詞p(n)，則引入時間的后置斷言R為謂詞pt(n)=p(n)∧t(n)。

3兩個實例

下面推導(dǎo)出兩個引入時間問題的算法程序，以此來說明在形式化推導(dǎo)出算法的同時，可以同步而又自然地推導(dǎo)出關(guān)于時間復(fù)雜度的遞歸方程式。

3．1順序查找問題

問題描述：在數(shù)組a[n]中順序查找一個元素key。若key在數(shù)組中，則輸出key在數(shù)組中的位置；否則，輸出n。其執(zhí)行時間為O(n)。

4結(jié)束語

本文的推導(dǎo)過程建立在嚴(yán)格的一階謂詞邏輯演算上，讓人信服，這也提高了算法程序的可靠性。下面的工作是在遞歸時間度量的基礎(chǔ)上進(jìn)一步引入真實時間度量，有望在實時軟件系統(tǒng)形式化開發(fā)和驗證中得到應(yīng)用。

參考文獻(xiàn)：

［1］HEHNER E C R，鄭宇華，萬劍怡.一種實用的程序設(shè)計理論[M].New York:SpringerVerlag，1993.

[2]XUE Jinyun.A unified approach for developing efficien algorithmic programs[J].Journal of Computer Science and Technology，1997，12(4):314－329.

[3]XUE Jinyun. A practicable approach for formal development of algorithmic programs[C]//Proc of ISFST’99.Japan:Software Association，1999.

［4］XUE Jinyun.Two new strategies for developing loop invariants and its applications[J].Journal of Computer Science and Technology，1993，8(2):147154.

[5]XUE Jinyun，DAVIS R.A derivation and proof of Knuth’ binary to decimal program[J].

SoftwareConcepts and Tools，1997，8(4):149－156.

[6]XUE Jinyun. Formal development of graph algorithmic programs using partitionandrecur[J].Journal of Computer Science and Technology，1998，13(6):553－561.

[7]徐家福，陳道蓄，呂建，等.軟件自動化[M].北京：清華大學(xué)出版社，1994.

[8]王曉東.計算機(jī)算法設(shè)計與分析[M].2版.北京：電子工業(yè)出版社，2001.

“本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文”