二叉樹隊列關(guān)系問題非遞歸算法的推導(dǎo)及形式化證明

左正康,方 越,黃志鵬,黃 箐,王昌晶

(江西師范大學(xué)計算機(jī)信息工程學(xué)院,江西 南昌 330022)

0 引言

二叉樹是在計算機(jī)科學(xué)中一種經(jīng)典的非線性數(shù)據(jù)結(jié)構(gòu),它不僅能夠提供有規(guī)律的數(shù)據(jù)存儲還能支持強(qiáng)大的搜索算法.二叉樹遞歸算法簡單、易理解,但它需要更多的運(yùn)行時間和存儲空間;而非遞歸算法的效率要遠(yuǎn)高于遞歸算法,因此二叉樹非遞歸算法的推導(dǎo)及形式化證明具有重要的價值.通過分析被求解二叉樹問題的背景知識和相關(guān)數(shù)學(xué)特性,對二叉樹類問題進(jìn)行分劃,確定二叉樹可以用2種方式來求解序列的遞推關(guān)系:棧和隊列.本文給出了二叉樹隊列關(guān)系問題推導(dǎo)和形式化證明策略,結(jié)合具有隊列遞推關(guān)系(簡稱“隊列關(guān)系”)的這一類問題來驗(yàn)證策略的正確性和實(shí)用性.由于二叉樹非遞歸算法的代碼復(fù)雜、難以理解,而且證明過程晦澀難懂,正確性得不到保證[1],因此如何推導(dǎo)及形式化證明二叉樹隊列關(guān)系問題非遞歸算法成為一大難點(diǎn).

開發(fā)二叉樹非遞歸算法的循環(huán)不變式一直是形式化開發(fā)的難點(diǎn)[2],循環(huán)不變式是理解、推導(dǎo)和證明循環(huán)程序的基礎(chǔ)[3-4].文獻(xiàn)[5-6]提供了前序遍歷二叉樹非遞歸算法的循環(huán)不變式,但是表達(dá)十分煩瑣,邏輯關(guān)系較為復(fù)雜,沒有很好的可行性和實(shí)用性.本文通過開發(fā)眾多二叉樹隊列關(guān)系問題非遞歸算法的循環(huán)不變式,發(fā)現(xiàn)循環(huán)不變式之間的共性和特性.由此,提出了開發(fā)二叉樹隊列關(guān)系問題循環(huán)不變式的3種策略和二叉樹隊列關(guān)系問題通用循環(huán)不變式的模板.

本文通過推導(dǎo)3類派生問題為代表,分別是基于層次遍歷二叉樹派生出的問題、基于求二叉樹深度派生出的問題以及基于層次遍歷二叉樹和求二叉樹深度共同派生出的問題,得到遞推關(guān)系表達(dá)式和循環(huán)不變式,由此導(dǎo)出抽象程序設(shè)計語言Apla(Abstract Programming Language)[2,4,7]程序,極大地提高了算法的開發(fā)效率;然后,用Dijkstra-Gries標(biāo)準(zhǔn)程序證明方法證明了這些算法的正確性;最后通過“Apla到C++程序自動生成系統(tǒng)”自動生成可執(zhí)行程序[8].

1 相關(guān)工作

開發(fā)正確的算法程序是計算機(jī)科學(xué)的核心.通常人們是針對已編好的程序來測試驗(yàn)證該程序是否正確,盡可能地找出程序的漏洞,但是該方法無法從根本上保證算法程序的正確性.于是,出現(xiàn)了越來越多的形式化推導(dǎo)方法,將待解決問題精確地描述出來,再根據(jù)各方法的形式化規(guī)則進(jìn)行推理,最終得出正確的結(jié)構(gòu)化程序[9].目前,存在著大量的形式化推導(dǎo)方法,其中E. W. Djkstra[6]提出的最弱前置謂詞方法wp(Q,R)是程序求解變換的經(jīng)典方法之一.給出程序規(guī)約,并將驗(yàn)證程序正確性的理論融入開發(fā)過程中,在開發(fā)過程中保證了程序的正確性.該方法自動化程度低,對于復(fù)雜的算法難以進(jìn)行推導(dǎo).D.L. Chaudhari等[10]提出的推導(dǎo)方法是在最弱謂詞方法的基礎(chǔ)上,將后置斷言不斷拆分,直至開發(fā)出循環(huán)不變式,但該方法在處理復(fù)雜問題上還是存在著較大的困難.D.G. Kourie等[11]提出了一種結(jié)合Dijkstra的GCL和Morgan的細(xì)化演算規(guī)則的方法,依靠經(jīng)驗(yàn)推測循環(huán)不變式,這導(dǎo)致在推導(dǎo)過程中非常依賴循環(huán)不變式,存在很大的不確定性.D.L. Chaudhari等[12]無縫地將自下而上的技術(shù)結(jié)合到自上而下的推導(dǎo)方法中,以此避免不必要的回溯和相關(guān)的返工,提出了新的推導(dǎo)策略,以捕捉在自上而下階段中所做的假設(shè),并隨后將這些假設(shè)反向傳播到適當(dāng)?shù)某绦蛭恢?并在 CAPS 系統(tǒng)中實(shí)現(xiàn)了這種方法.

開發(fā)正確迭代程序的關(guān)鍵是循環(huán)不變式,這已經(jīng)被程序設(shè)計和形式化方法方面的專家所認(rèn)可,循環(huán)不變式是程序設(shè)計理論中的一個重要概念,在形式化證明中承擔(dān)著至關(guān)重要的作用[13].循環(huán)不變式不僅可以用來分析程序的性質(zhì),而且可以用來證明循環(huán)程序的正確性,但是開發(fā)循環(huán)不變式的標(biāo)準(zhǔn)策略僅僅適用于一些簡單的算法程序,對于復(fù)雜的算法程序仍無較好的辦法.T. Hoare認(rèn)為循環(huán)不變式不能通過簡單的規(guī)則計算來驗(yàn)證.為了獲得適當(dāng)?shù)难h(huán)不變式,通常需要人工干預(yù)才能完成.目前只能針對特定的情況提出了一些啟發(fā)式的方法,沒有一種通用的方法可以對所有的情況得到正確的結(jié)果[14].一般來說,對于一個給定函數(shù)的前置斷言和后置斷言,循環(huán)不變式并不是唯一的,開發(fā)者往往會逐步得到循環(huán)不變式:首先猜測出粗略的循環(huán)不變式,然后通過觀察程序的行為逐步精化循環(huán)不變式,最后證明需要的信息是否正確[15].開發(fā)循環(huán)不變式一般的方法是假定程序中的變量在無限范圍上求值.然而,變量在程序執(zhí)行過程中由有限長度的位向量表示.在無限范圍上的循環(huán)不變量式可能不再是在有限范圍程序中的循環(huán)不變量式,反之也是如此[16].采用消元法對程序進(jìn)行驗(yàn)證[17],可生成非線性循環(huán)不變式,并判定循環(huán)程序的終止性,如基于Dixon結(jié)式.M.D. Ernst等[18]提出了循環(huán)不變式的動態(tài)探測技術(shù),并設(shè)計了動態(tài)監(jiān)測器來實(shí)現(xiàn)此技術(shù).

二叉樹是計算機(jī)科學(xué)中一種經(jīng)典的非線性數(shù)據(jù)結(jié)構(gòu),有強(qiáng)大的功能和效率,因此二叉樹的推導(dǎo)和形式化證明具有非常重要的意義.D. Gries[5]對E.W. Dijkstra[6]提出的構(gòu)造循環(huán)不變式開發(fā)策略進(jìn)行了補(bǔ)充和解釋,提供了前序遍歷二叉樹非遞歸算法的循環(huán)不變式.在二叉樹非遞歸算法的形式化驗(yàn)證上,秦勝潮等[19]用HIP/SLEEK形式化驗(yàn)證了AVL樹和二叉搜索樹.

目前,二叉樹的推導(dǎo)是基于最弱前置謂詞方法,其推導(dǎo)過程煩瑣,循環(huán)不變式較為復(fù)雜.本文提出的推導(dǎo)方法是基于嚴(yán)格的數(shù)理邏輯,對原算法程序規(guī)約進(jìn)行了一系列的求精變換步驟.每一步都減少了一定的抽象程度或增加了一定的程序可執(zhí)行性,大大降低了在算法求精過程中的創(chuàng)造性工作.并且,開發(fā)循環(huán)不變式的策略是一種基于遞歸定義技術(shù)來開發(fā)具有固有遞歸性質(zhì)的迭代程序的循環(huán)不變式,提高了開發(fā)效率.

2 二叉樹隊列關(guān)系問題推導(dǎo)及形式化證明策略

2.1 求解步驟

對二叉樹類問題進(jìn)行分劃,尋找遞推關(guān)系.關(guān)于求解序列的遞推關(guān)系為隊列的這類問題,通過推導(dǎo)及形式化證明,總結(jié)出如下7個步驟:

(i)構(gòu)造算法程序規(guī)約.構(gòu)造形式化規(guī)約來明確二叉樹隊列關(guān)系問題的任務(wù)目標(biāo),程序規(guī)約是由程序的前置斷言(AQ)和后置斷言(AR)構(gòu)成.對于二叉樹隊列關(guān)系問題的非遞歸算法,前置斷言均為給定1個有限的二叉樹T;后置斷言根據(jù)求解問題的定義和實(shí)現(xiàn)的功能以形式化語言描述程序達(dá)到所要的目的.雖然后置斷言只有1個,但是為了供后續(xù)更容易地推導(dǎo)算法,可以分劃出求解問題的關(guān)鍵功能,對這部分功能構(gòu)造出新的形式化規(guī)約.

(ii)分劃原問題.二叉樹隊列關(guān)系問題的算法或遞推關(guān)系均由分劃決定,不同的算法會有不同的分劃,可以從步驟(i)中形式規(guī)約得到分劃二叉樹隊列關(guān)系問題的啟示:劃分二叉樹,得到一定數(shù)量的子樹,子樹需滿足結(jié)構(gòu)與原二叉樹相同但規(guī)模比原二叉樹更小的特征,再把子樹進(jìn)行相同方式劃分,直到求解出每一個子樹.

(iii)尋找遞推關(guān)系.通過分析二叉樹問題的背景知識和數(shù)學(xué)特性,確定其求解序列的遞推關(guān)系和所需的全部循環(huán)變量,用謂詞精確表達(dá)它們的變化規(guī)律.二叉樹擁有2種求解序列的遞推關(guān)系:棧和隊列.

對于隊列,可以看成是一個序列q[0…#q-1],并規(guī)定q[0]端為隊頭,q[#q-1]為隊尾,則隊列的常用操作可以用如下序列的操作加以實(shí)現(xiàn):

(a)測試隊列是否為空,即#q=0;

(b)引用隊列頭元素,即X:=q[0];

(c)對隊列q實(shí)施進(jìn)隊,即q:=q↑[X];

(d)對隊列q實(shí)施出隊,即q:=q[1…].

將隊列及其運(yùn)算封裝在一起構(gòu)成抽象數(shù)據(jù)類型,用量詞轉(zhuǎn)換法推導(dǎo)出隊列問題求解序列的遞推關(guān)系Si=F(Sj),Si是其子解Sj的函數(shù),其中1

(iv)構(gòu)造循環(huán)不變式.通過步驟(iii)構(gòu)造的遞推關(guān)系表達(dá)式,采用本文提出的開發(fā)二叉樹隊列關(guān)系問題循環(huán)不變式的策略,使用循環(huán)不變式遞歸定義技術(shù),并結(jié)合二叉樹隊列關(guān)系問題通用循環(huán)不變式模板,根據(jù)不同問題的特性和要求,以此開發(fā)該問題的循環(huán)不變式.

(v)導(dǎo)出非遞歸算法Apla程序.依據(jù)步驟(iii)統(tǒng)一的遞推關(guān)系和步驟(iv)統(tǒng)一的循環(huán)不變式,推導(dǎo)出二叉樹隊列關(guān)系問題的Apla算法程序.

(vi)形式化證明.通過Dijkstra-Gries標(biāo)準(zhǔn)程序證明法證明Apla算法程序的正確性.

(vii)生成C++程序.通過“Apla到C++程序自動生成系統(tǒng)”自動生成C++可執(zhí)行程序.

2.2 改進(jìn)循環(huán)不變式

E.W. Dijkstra和D. Gries給出了4個循環(huán)不變式的傳統(tǒng)開發(fā)策略[20],D. Gries對其進(jìn)行了解釋和補(bǔ)充,開發(fā)了前序遍歷二叉樹非遞歸算法的循環(huán)不變式[5-6]:

ρ:0≤c≤#p∧fpreorder(p)=b[0:c-1]|fpreorder(r0)|fpreporder(r1)…|fpreorder(rr-1).

觀察該循環(huán)不變式,看出此循環(huán)不變式用“…”表示顯得冗長、不易理解.于是,使用循環(huán)不變式的遞歸定義技術(shù),重新對前序遍歷二叉樹非遞歸算法的循環(huán)不變式進(jìn)行開發(fā)[4]:

ρ:HPre(T)=X↑HPre(q)↑F(S),

該循環(huán)不變式引進(jìn)了3個輔助變量:X,S,q.其中X存放已遍歷的結(jié)點(diǎn)序列;S是起堆棧作用的變量,用于存放尚待遍歷的T的右子樹;q用于存放正準(zhǔn)備遍歷的T的子樹.

比較以上2個循環(huán)不變式,可以很清晰地發(fā)現(xiàn)本文的循環(huán)不變式更簡單、精確.因此,以文獻(xiàn)[21-22]提出的開發(fā)循環(huán)不變式的新定義和新的開發(fā)策略為基礎(chǔ),提出了對二叉樹隊列關(guān)系問題開發(fā)循環(huán)不變式的策略.

先寫出其前置斷言和后置斷言,前置斷言均為“給定一個有限的二叉樹T”,而后置斷言的不同則決定著每個問題是屬于什么輸出類型,再根據(jù)問題的實(shí)現(xiàn)思路,并結(jié)合后置斷言,可將開發(fā)二叉樹隊列關(guān)系問題循環(huán)不變式的策略分為3種.

策略1輸出結(jié)果為結(jié)點(diǎn)序列的問題.

通過分析求解問題的特性,確定后置斷言為X=算法F(T)形式,以表明輸出結(jié)果為結(jié)點(diǎn)序列.通過分劃遞推,尋找序列變量和隊列存放待求解子問題的變化規(guī)律,以此推導(dǎo)出遞推關(guān)系,并確定循環(huán)變量,采用遞歸定義技術(shù)定義序列變量和隊列中的內(nèi)容,即構(gòu)成所需的循環(huán)不變式.

策略2輸出結(jié)果為固定值的問題.

根據(jù)求解問題的定義和實(shí)現(xiàn)的功能,確定后置斷言為算法F(T)=固定值,以表明輸出結(jié)果為固定值.通過分劃遞推,尋找能判別待求解子問題的固定值變化規(guī)律是否均滿足求解問題需實(shí)現(xiàn)功能的約束條件的這一規(guī)律,以此推導(dǎo)出遞推關(guān)系,并結(jié)合隊列存放待求解子問題的變化規(guī)律,確定循環(huán)變量,采用遞歸定義技術(shù)定義固定值、序列變量和隊列中元素的組成,即構(gòu)成所需的循環(huán)不變式.

策略3輸出結(jié)果為屬性判斷的問題.

根據(jù)求解問題的定義和實(shí)現(xiàn)的功能,確定后置斷言為算法F(T)=對于任一結(jié)點(diǎn)的該問題的屬性判斷均為真,以表明輸出結(jié)果為true或false.通過分劃遞推,尋找待求解子問題的屬性判斷變化規(guī)律是否均滿足求解問題需實(shí)現(xiàn)功能的約束條件的這一規(guī)律,以此推導(dǎo)出遞推關(guān)系,并結(jié)合隊列存放待求解子問題的變化規(guī)律,確定循環(huán)變量,再采用遞歸定義技術(shù)定義屬性判斷、序列變量和隊列中元素的組成,即構(gòu)成所需的循環(huán)不變式.

2.3 二叉樹隊列關(guān)系問題通用循環(huán)不變式模板

在推導(dǎo)出眾多二叉樹隊列關(guān)系問題得出的循環(huán)不變式過程中,發(fā)現(xiàn)每個問題的循環(huán)不變式都存在共性.因此,構(gòu)造一個二叉樹隊列關(guān)系問題通用循環(huán)不變式模板,供后續(xù)開發(fā)更多的二叉樹隊列關(guān)系問題.該模板形式為

ρ:HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧P(x),

其中HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])為層次遍歷二叉樹的循環(huán)不變式.序列變量X用于存放已訪問的結(jié)點(diǎn)標(biāo)志序列,當(dāng)有限二叉樹遍歷結(jié)束時,X=HLay(T);S為隊列,用來存放待訪問的頂點(diǎn);h為序列頭的域名;q用于存放正在訪問的頂點(diǎn).在隊列S中的首元素為即將訪問的頂點(diǎn),且在被訪問后,該頂點(diǎn)的未被遍歷的相鄰頂點(diǎn)要作為待訪問頂點(diǎn)進(jìn)入隊列.所以S中的內(nèi)容由函數(shù)F定義為

F([])=[],

(1)

F(S)=[S.h]↑F(S[h+1..t]↑[S[h].l]↑

[S[h].r]);

(2)

當(dāng)q未訪問時,

F([q↑S])=[q.d]↑F(S↑[q.l]↑[q.r]),

(3)

當(dāng)q已訪問時,

F([q↑S])=F(S).

(4)

P(x)是指根據(jù)不同問題的特性和要求,合取滿足條件的斷言.

2.4 預(yù)定義ADT

抽象程序設(shè)計語言Apla[4]提供了序列(list)和二叉樹(btree)預(yù)定義的ADT類型,下面給出本文中所用的序列和二叉樹ADT相關(guān)數(shù)據(jù)和操作說明.

2.4.1 序列 關(guān)于序列的定義和操作如下:

varh,t:integer:=0,0;//t表示序列尾的域名;

varS,T:list:=[],[];//S和T為序列;

X:data;i,j:integer;//X是序列中的元素;

[]//序列為空;

[X]//序列中有一個元素X;

#(S)//計算S中元素的個數(shù);

S[i]//S的第i個元素,S.h≤i≤S.t;

S[i..j]//S的子序列,S.h≤i,j≤S.t;

S↑T//S的尾和T的頭用“↑”運(yùn)算合成一個新序列.

2.4.2 二叉樹 關(guān)于二叉樹的定義和操作如下:

T.d//產(chǎn)生二叉樹T的根結(jié)點(diǎn);

T.l//產(chǎn)生二叉樹T的左子樹;

T.r//產(chǎn)生二叉樹T的右子樹;

n+T//把結(jié)點(diǎn)n加到T中,使T成為和T結(jié)構(gòu)相同的新樹;

ReadNode(n)//建立結(jié)點(diǎn)n;

WriteNode(n)//輸出結(jié)點(diǎn)n.

2.5 二叉樹隊列關(guān)系問題的3類派生問題

通過深入研究大量二叉樹隊列關(guān)系問題非遞歸算法,思考各個問題的思想和數(shù)據(jù)結(jié)構(gòu)特性,尋找它們的共性和特性,發(fā)現(xiàn)很多算法可以在實(shí)現(xiàn)母算法功能的同時增添符合該問題的功能實(shí)現(xiàn)條件,以此最終實(shí)現(xiàn)該問題.因此,將層次遍歷二叉樹和求二叉樹深度作為母算法,將二叉樹隊列關(guān)系問題分為3類派生問題(見圖1).

(i)基于層次遍歷二叉樹派生出的問題:以判斷完滿二叉樹為例.在層次遍歷二叉樹的同時判斷當(dāng)前結(jié)點(diǎn)有幾個孩子,若有2個或0個則繼續(xù)判斷隊列中的下一個結(jié)點(diǎn);若有1個則不是完滿二叉樹.直至層次遍歷完所有結(jié)點(diǎn),若所有節(jié)點(diǎn)均滿足條件,則該二叉樹為完滿二叉樹.

(ii)基于求二叉樹深度派生出的問題:以判斷一顆具有xsize個結(jié)點(diǎn)二叉樹是否為滿二叉樹為例.在求出二叉樹深度為xheight后,若滿足2xheight-1=xsize,則是滿二叉樹,否則不是滿二叉樹.

(iii)基于層次遍歷二叉樹和求二叉樹深度共同派生出的問題:以判斷平衡二叉樹為例.在層次遍歷二叉樹的同時以當(dāng)前結(jié)點(diǎn)作為根結(jié)點(diǎn),通過求二叉樹深度的功能判斷左右子樹的深度之差的絕對值是否小于等于1,若滿足則繼續(xù)判斷隊列中的下一個結(jié)點(diǎn),若不滿足則不是平衡二叉樹.直至層次遍歷完所有結(jié)點(diǎn),若所有節(jié)點(diǎn)均滿足條件,則該二叉樹為平衡二叉樹.

圖1 3類派生問題

3 二叉樹隊列關(guān)系問題非遞歸算法推導(dǎo)

3.1 母算法

層次遍歷二叉樹和求二叉樹深度對二叉樹隊列關(guān)系問題非遞歸算法的推導(dǎo)起著至關(guān)重要的作用.若2個母算法成功推導(dǎo),則這便于派生問題的推導(dǎo),也有助于更好地發(fā)現(xiàn)3類派生問題循環(huán)不變式的共性和特性.因此,需要先對這2個母算法進(jìn)行推導(dǎo).

3.1.1 層次遍歷二叉樹 文獻(xiàn)[23]已經(jīng)成功推導(dǎo)出層次遍歷二叉樹非遞歸算法的循環(huán)不變式:

ρ:HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])

以及非遞歸算法Apla程序:

do ┐(q=%)→S,X,q:=S↑[q.l]↑[q.r],X↑[q.d],%;

[] ┐(S=[])→q,S:=S[h],S[h+1..t];

od.

3.1.2 求二叉樹深度 文獻(xiàn)[23]已經(jīng)成功推導(dǎo)出求二叉樹深度非遞歸算法的循環(huán)不變式:

ρ:h=[(N,n:0≤n:n=#(S))-1]∧HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])

以及非遞歸算法Apla程序:

do (num≥1)→q,S:=S[S.h],S[S.h+1..S.t];

X:=X↑[q.d];

if (q.l≠%)→S:=S↑[q.l];fi;

if (q.r≠%)→S:=S↑[q.r];fi;

n:=n-1;

[] ┐(q=%)→n,h,q:=#(S),h+1,%;

od.

3.2 形式推導(dǎo)實(shí)例

限于篇幅,本節(jié)以判斷平衡二叉樹為實(shí)例,完整地展現(xiàn)如何基于母算法推導(dǎo)派生問題.

(i)算法程序規(guī)約.用HLay(T)表示T的層次遍歷產(chǎn)生的結(jié)點(diǎn)序列,存放已訪問的結(jié)點(diǎn)標(biāo)志序列在序列變量X中,X=HLay(T).LDepth(T)表示T的深度.abs() 函數(shù)表示返回數(shù)字的絕對值.用abs(LDepth(q.l)-LDepth(q.r))≤1來判斷當(dāng)前結(jié)點(diǎn)q左右子樹的深度之差的絕對值是否符合判斷條件,若滿足abs(LDepth(q.l)-LDepth(q.r))≤1,則繼續(xù)層次遍歷下一個結(jié)點(diǎn),重復(fù)此操作,直至遍歷結(jié)束.若fBalance(T)=true,則T是平衡二叉樹;若fBalance(T)=false,則T不是平衡二叉樹.即求解問題的算法規(guī)約:

|[X:list (integer,40);T:btree (integer,40);msize:integer]|;

AQ:給定一個有限的二叉樹T;

AR:fBalance(T)=?(a:a∈HLay(T):abs(LDepth(a.l)-LDepth(a.r))≤1).

創(chuàng)建布爾變量isbalance(a)函數(shù)記錄abs(LDepth(a.l)-LDepth(a.r))≤1的判斷結(jié)果.

(ii)尋找遞推關(guān)系.根據(jù)判斷完全二叉樹的算法程序規(guī)約,僅需尋找fPerfect(T)的遞推關(guān)系:

若T=%,則fBalance(T)=true;

若T≠%,則為了得到一個非遞歸的算法程序,分劃fBalance(T),得到遞推關(guān)系為

fBalance(T)=(isbalance(T)=true)∧fBalance(T.l)∧fBalance(T.r)=(isbalance(T)=true)∧(isbalance(T.l)=true)∧fBalance(T.l.l)∧fBalance(T.l.r)∧fBalance(T.r)=….

由以上遞推關(guān)系發(fā)現(xiàn):該過程是通過層次遍歷二叉樹HLay(T)來表示二叉樹T中所有結(jié)點(diǎn)構(gòu)成的一個序列X.在實(shí)現(xiàn)過程中,必須使用隊列S存放待訪問的頂點(diǎn),q用于存放正在訪問的頂點(diǎn),序列變量X用來存放已訪問的結(jié)點(diǎn)標(biāo)志序列,當(dāng)有限二叉樹遍歷結(jié)束時,X=HLay(T).

(iii)構(gòu)造循環(huán)不變式.由于X存放了層次遍歷后的結(jié)點(diǎn)序列,因此flag的值始終依賴于X中的結(jié)點(diǎn),即有如下性質(zhì)成立:

flag=?(a:a∈X:isbalance(a)=true).

因此,上式與HLay(T)的循環(huán)不變式合取即構(gòu)成本問題算法程序的循環(huán)不變式:

ρ:HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true).

(iv)非遞歸算法Apla程序.通過遞推關(guān)系(ii)和循環(huán)不變式(iii),簡捷地導(dǎo)出Apla語言過程:

procedurefBalance(T:btree(integer,40);varX:list(integer,40));

begin

X,S,q,flag:=[],[],T,true;

{ρ:HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true)};

doflag∧(┐(q=%)∨┐(S=[]))→if (q≠%)∧(isbalance(q)=true)→flag,X,S,q:=true,X↑[q.d],S↑[q.l]↑[q.r],%;

[] (q≠%)∧(isbalance(q)=false)→flag,X,S,q:=false,X↑[q.d],S↑[q.l]↑[q.r],%;

[] (q=%)∧┐(S=[])→q,S:=S[S.h],S[S.h+1..S.t];fi;

od;

if(flag=true)→ writeln(“是平衡二叉樹”);

[]→writeln(“不是平衡二叉樹”);

fi;

end.

4 二叉樹隊列關(guān)系問題非遞歸算法形式化證明

Dijkstra-Gries標(biāo)準(zhǔn)程序證明法是形式化證明的重要方法,通過證明{Q}S{R}的正確性,以此來驗(yàn)證算法程序的正確性.S表示語句,Q表示謂詞公式或S的前置斷言,R表示謂詞公式或S的后置斷言.對于二叉樹隊列關(guān)系問題,由于此類問題是循環(huán)語句do的一般形式,所以基于在Dijkstra-Gries標(biāo)準(zhǔn)程序證明法中循環(huán)語句do的證明條件來證明二叉樹隊列關(guān)系問題.本節(jié)以判斷平衡二叉樹為例,詳細(xì)地展現(xiàn)如何形式化證明二叉樹隊列關(guān)系問題.

(i)證明在執(zhí)行循環(huán)之前ρ是正確的.

由于斷言中給出的AQ并非do語句中的AQ,而是整個程序的AQ.因此,若為保證do語句執(zhí)行開始迭代之前ρ為真,使得AQ?ρ,則必須保證如下斷言成立:

語句S0為S,X,q,flag:=[],[],T,true,

AQ?wp(S0,ρ)≡(HLay(T)=X↑[q.d]↑F(S↑

HLay(T)=[]↑[T.d]↑F([T.l]↑[T.r])∧true=?(a:a∈X:isbalance(a)=true);

{使用遞推關(guān)系式(4)}≡true.

將聲明S0中的3個變量賦值給ρ,顯然實(shí)現(xiàn)AQ?wp(S0,ρ),顯然上述斷言成立.

(ii)證明ρ是循環(huán)不變式.

用布爾變量flag記錄fBalance(T)的判斷結(jié)果,可更深地進(jìn)行細(xì)化,便于下面形式化證明:

?(a:a∈HLay(T):isbalance(a)=true)→flag=true∨?(a:a∈HLay(T):isbalance(a)=false)→flag=false.

(a)針對循環(huán)體中的第1個條件子句:

條件C1為flag∧(┐(q=%)∨┐(S=[]))∧(q≠%)∧(isbalance(q)=true)

語句S1為flag,X,S,q:=true,X↑[q.d],S↑[q.l]↑[q.r],%;

[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true)∧flag∧(┐(q=%)∨┐(S=[]))∧(q≠%)∧(isbalance(q)=true)?HLay(T)=X↑F(S)∧true=?(a:a∈X↑[%]:isbalance(a)=true);

{使用遞推關(guān)系式(4)}≡true.

將聲明S1中的3個變量賦值給ρ,實(shí)現(xiàn)ρ∧C1?wp(S1,ρ),顯然第1個條件子句成立.

(b)針對循環(huán)體中的第2個條件子句:

條件C2為flag∧(┐(q=%)∨┐(S=[]))∧(q≠%)∧(isbalance(q)=false);

語句S2為flag,X,S,q:=false,X↑[q.d],S↑[q.l]↑[q.r],%;

{使用遞推關(guān)系式(3)和遞推關(guān)系式(4)}≡HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true)∧flag∧(┐(q=%)∨┐(S=[]))∧(q≠%)∧(isbalance(q)=false)?HLay(T)=X↑F(S)∧false=?(a:a∈X↑[%]:isbalance(a)=true)≡true.

將聲明S2中的2個變量賦值給ρ,實(shí)現(xiàn)ρ∧C2?wp(S2,ρ),顯然第2個條件子句成立.

(c)針對循環(huán)體中的第3條件子句:

條件C3為flag∧(┐(q=%)∨┐(S=[]))∧(q=%)∧┐(S=[]);

語句S3為q,S:=S[S.h],S[S.h+1..S.t];

{使用遞推關(guān)系式(3)和遞推關(guān)系式(4)}≡HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true)∧flag∧(┐(q=%)∨┐(S=[]))∧(q=%)∧┐(S=[])?(HLay(T)=X↑F(S)∧flag=?(a:a∈X:isbalance(a)=true)≡true.

將聲明S3中的2個變量賦值給ρ,實(shí)現(xiàn)ρ∧C3?wp(S3,ρ),顯然第3個條件子句成立.

(iii)證明后置斷言R在循環(huán)終止時必須為真.

ρ∧┐ (flag∧(┐(q=%)∨┐(S=[])))?AR≡ρ∧(┐flag∨((q=%)∧(S=[])))?fbalance(T)=?(a:a∈HLay(T):abs(Ldepth(a.l)-Ldepth(a.r))≤1)≡ρ∧(┐flag∨(flag∧(q=%)∧(S=[])))?fbalance(T)=?(a:a∈HLay(T):abs(Ldepth(a.l)-Ldepth(a.r))≤1)≡HLay(T)=X↑[q.d]↑F(S↑[q.l]↑[q.r])∧flag=?(a:a∈X:isbalance(a)=true)∧(flag∧(q=%)∧(S=[]))?fbalance(T)=?(a:a∈HLay(T):abs(Ldepth(a.l)-Ldepth(a.r))≤1)≡HLay(T)=X∧true=?(a:a∈X:isbalance(a)=true)∧(flag∧(q=%)∧(S=[]))?fbalance(T)=?(a:a∈Lay(T):abs(Ldepth(a.l)-Ldepth(a.r))≤1)≡true∧true=?(a:a∈X:isbalance(a)=true)∧(flag∧(q=%)∧(S=[]))?fbalance(T)=?(a:a∈HLay(T):abs(Ldepth(a.l)-Ldepth(a.r))≤1)≡true.

(iv)循環(huán)的終止性顯然成立.

至此, 完成了此程序的正確性證明.

5 二叉樹隊列關(guān)系問題C++程序的自動生成

本實(shí)驗(yàn)室研究團(tuán)隊已經(jīng)開發(fā)了一個“Apla到C++程序自動生成系統(tǒng)”[7],可以實(shí)現(xiàn)Apla到C++程序的自動轉(zhuǎn)換,實(shí)現(xiàn)算法程序的機(jī)器無關(guān)性.“Apla到C++程序自動生成系統(tǒng)”總體結(jié)構(gòu)如圖2所示.

圖2 “Apla到C++程序自動生成系統(tǒng)”總體結(jié)構(gòu)圖

通過“Apla到C++程序自動生成系統(tǒng)”,可將推導(dǎo)并形式化證明的Apla算法程序作為源語言,自動生成對應(yīng)的C++可執(zhí)行程序[22],本文的實(shí)例均可自動生成對應(yīng)的C++可執(zhí)行程序,以判斷平衡二叉樹為例(見圖3).“Apla到C++程序自動生成系統(tǒng)”集詞法分析、語法分析、語義一致性分析、轉(zhuǎn)換、編譯、運(yùn)行為一體.Apla語言中抽象數(shù)據(jù)的操作均基于簡單數(shù)據(jù)類型及其操作,為了轉(zhuǎn)換一些簡單數(shù)據(jù)類型及其操作,于是,先構(gòu)造了一個簡單的程序轉(zhuǎn)換系統(tǒng),稱為“核心轉(zhuǎn)換器”,然后通過抽象數(shù)據(jù)類型的操作推導(dǎo)得到Apla程序,再用“核心轉(zhuǎn)換器”轉(zhuǎn)換為C++程序,作為相應(yīng)的C++可重用部件庫中的操作,最后通過這種方式C++可重用部件庫的正確性就得到了保證.由此,Apla算法程序自動生成C++程序的正確性也得到了保證,最終實(shí)現(xiàn)了從抽象規(guī)約到具體的可執(zhí)行程序的完整求精過程[9].

圖3 Apla到C++程序自動生成系統(tǒng)生成判斷平衡二叉樹的C++程序

圖3代碼為判斷平衡二叉樹非遞歸算法的Apla程序,通過左邊的Apla代碼自動生成對應(yīng)的C++可執(zhí)行程序如下:

flag=true;

do {

if (flag && (!(q.Equa(tempTree0.SetEmpty0))||!(S.Equal(tempList1.SetEmpty0)))) {

if ((q!tempTree0.SetEmpty0)&&(isbalance(q)==true)){

flag=true;

X.Copy(X.Concat(OneitemList(q.Data0)));

S.Copy(S.Concat(OneitemList(q.Left0).Concat(OneitemList(q.Right0))));

q.Copy(tempTree0.SetEmpty0);

}

else if ((q!=tempTree0.SetEmpty0) && (isbalance(q)==false)) {

flag=false;

X.Copy(X.Concat(OneitemList(q.Data0)));

S.Copy(S.Concat(OneitemList(q.Left0).Concat(OneitemList(q.Right0))));

q.Copy(tempTree0.SetEmpty0);

}

else if ((q.Equal(tempTree0.SetEmpty0)) &&!(S.Equal(tempList1.SetEmpty0))) {

q.Copy(S.Get(S.h));

S.Copy(S.Sublist(S.h+1,S.t));

}

}

else.

輸入10個無序的整數(shù)序列,并將其構(gòu)成二叉排序樹,對二叉排序樹進(jìn)行判斷是否為平衡二叉樹(見圖4).

圖4 構(gòu)建二叉排序樹

通過驗(yàn)證,自動生成的C++程序是正確的.“Apla到C++程序自動生成系統(tǒng)”將預(yù)定義的組合數(shù)據(jù)類型(集合、列表、二叉樹、圖、關(guān)系數(shù)據(jù)和其他預(yù)定義的數(shù)據(jù)類型)以ADT的形式進(jìn)行封裝,并且可以用作標(biāo)準(zhǔn)數(shù)據(jù)類型,這極大地提高算法和程序的開發(fā)效率.

6 結(jié)束語

本文通過對二叉樹類問題進(jìn)行分劃,尋找遞推關(guān)系,對求解序列的遞推關(guān)系為隊列這類問題,給出推導(dǎo)和形式化證明策略.探索二叉樹隊列關(guān)系問題非遞歸算法的循環(huán)不變式之間的共性和特性,發(fā)現(xiàn)很多二叉樹隊列關(guān)系問題都是可以基于層次遍歷二叉樹和求二叉樹深度這2個算法的功能加以實(shí)現(xiàn),由此,可將二叉樹隊列關(guān)系問題分為3類派生問題.本文對派生問題代表進(jìn)行推導(dǎo),得出遞推關(guān)系表達(dá)式和循環(huán)不變式,由此導(dǎo)出非遞歸Apla算法,再用Dijkstra-Gries標(biāo)準(zhǔn)程序證明法證明算法的正確性,最后使用“Apla到C++程序自動生成系統(tǒng)”自動生成C++可執(zhí)行程序,實(shí)現(xiàn)了從抽象規(guī)約到具體的可執(zhí)行程序的完整求精過程.相比國內(nèi)外現(xiàn)有研究,本文具有如下特點(diǎn):

1)提出了二叉樹隊列關(guān)系問題非遞歸算法推導(dǎo)及形式化證明策略.主要對3種輸出結(jié)果問題對應(yīng)地提出了3種開發(fā)循環(huán)不變式策略,并根據(jù)循環(huán)不變式之間的共性和特性,構(gòu)造一個二叉樹隊列關(guān)系問題通用循環(huán)不變式模板,使求解二叉樹隊列關(guān)系問題更具有針對性.

2)成功地推導(dǎo)和形式化證明了一系列二叉樹隊列關(guān)系問題非遞歸算法.在推導(dǎo)過程中,基于層次遍歷二叉樹和求二叉樹深度這2個算法的功能,將推導(dǎo)二叉樹隊列關(guān)系問題分為3類派生問題.這便于派生問題更準(zhǔn)確、更便捷地推導(dǎo)和形式化證明.

3)使用開發(fā)的“Apla到C++程序自動生成系統(tǒng)”,對原算法程序規(guī)約進(jìn)行了一系列的求精變換步驟.每一步都減少了一定的抽象程度或增加了一定的程序可執(zhí)行性,并最終得到相應(yīng)的C++可執(zhí)行程序.該程序?qū)崿F(xiàn)了從抽象規(guī)約到具體的可執(zhí)行程序的完整求精過程,這極大地提高了算法和程序的開發(fā)效率和可靠性.

本文的研究提升了開發(fā)共性算法程序的高效性和有效性,對尋找各種二叉樹隊列關(guān)系問題非遞歸算法的循環(huán)不變式指明了新的方向,對非線性數(shù)據(jù)結(jié)構(gòu)算法程序的推導(dǎo)及形式化證明具有指導(dǎo)意義.