左正康,梁贊楊,蘇 崴,黃 箐,王 淵,王昌晶

(1.江西師范大學(xué)計算機信息工程學(xué)院,江西 南昌330022;2.江西師范大學(xué)軟件學(xué)院,江西 南昌330022)

1 引言

形式化方法作為一種基于數(shù)學(xué)語言和精確邏輯語義的方法被廣泛應(yīng)用于提高軟件的可靠性和正確性[1,2]，在軟件開發(fā)的各個階段發(fā)揮著不同的作用。形式化方法的研究方向可以分為形式化推導(dǎo)和形式化驗證[3]。形式化推導(dǎo)是在程序正確性證明理論下所進行的程序開發(fā)，通過程序規(guī)約構(gòu)造具體程序[4]。形式化驗證指的是針對一個已有程序，采用證明的方式判斷該程序是否滿足其程序規(guī)約[5]。序列作為一種高效且常用的數(shù)據(jù)結(jié)構(gòu)，在程序開發(fā)中被用于解決很多場景的實際問題，序列算法始終是人們研究的重要內(nèi)容[6]。然而，通過自然語言來描述算法問題與算法設(shè)計過程，其正確性難以保證。實踐證明，只有用數(shù)學(xué)方法對算法程序進行形式化推導(dǎo)或形式化證明，算法程序的正確性才能從邏輯上得到保證[7]。對于很多序列類問題，運用折半劃分的思想可以使問題更為簡單，進而開發(fā)出精妙且高效的算法。針對序列折半劃分問題開發(fā)一個形式化推導(dǎo)方法來保證算法的正確性是一項很有意義的工作?，F(xiàn)有的形式化推導(dǎo)方法將程序的開發(fā)與程序的證明交替進行，這一過程繁瑣且大多都只能推導(dǎo)得到抽象程序，而如何將抽象程序準(zhǔn)確地轉(zhuǎn)換為可執(zhí)行程序又成為一個難點。

為解決上述問題，本文提出了針對序列折半劃分問題的形式化推導(dǎo)方法，并以2種序列折半劃分問題為實例驗證了該方法的可行性。因非遞歸算法的效率遠高于其遞歸算法[8]的，故本文采用基于分劃遞推技術(shù)[9]的形式化推導(dǎo)方法。該方法先形式化描述問題的程序規(guī)約，通過分析問題的數(shù)學(xué)特性，對問題進行分劃。再通過程序規(guī)約變換技術(shù)對程序規(guī)約進行一系列數(shù)學(xué)變換，進而獲得算法程序的遞推關(guān)系和循環(huán)不變式。最終得出問題的Apla(Abstract programming language)程序并轉(zhuǎn)化為可執(zhí)行程序。該推導(dǎo)方法包含了從程序規(guī)約到可執(zhí)行程序的整個開發(fā)階段，推導(dǎo)過程以一階謂詞邏輯為基礎(chǔ)，應(yīng)用規(guī)約變換技術(shù)嚴(yán)格保證了規(guī)約的前后一致性。

本文提出的推導(dǎo)方法有以下優(yōu)點：(1)基于分劃遞推的核心思想，應(yīng)用規(guī)約變換技術(shù)對問題進行形式化推導(dǎo)，過程簡潔明了；(2)在構(gòu)造算法過程中，循環(huán)不變式可由遞推關(guān)系自然地構(gòu)造得到，循環(huán)不變式構(gòu)造相對容易；(3)實現(xiàn)了從程序規(guī)約到具體可執(zhí)行程序的完整程序求精過程。使用該方法推導(dǎo)程序可以將重點放在設(shè)計算法上，更多地考慮算法內(nèi)部的邏輯，使推導(dǎo)與求精同步進行。

本文第2節(jié)對相關(guān)工作進行介紹和比較。第3節(jié)對序列折半劃分問題形式化推導(dǎo)方法進行了詳細說明。第4節(jié)介紹了轉(zhuǎn)換平臺：Apla到C++程序自動生成系統(tǒng)。第5節(jié)將第3節(jié)中提出的方法應(yīng)用于“有序序列搜索特殊下標(biāo)”和“循環(huán)序列搜索最小元素下標(biāo)”這2個實例，進行推導(dǎo)得出遞推關(guān)系式和循環(huán)不變式，由此再推導(dǎo)出對應(yīng)問題的非遞歸Apla算法并通過“Apla到C++程序自動生成系統(tǒng)”自動生成C++可執(zhí)行程序。第6節(jié)對全文進行總結(jié)。

2 相關(guān)工作

程序的形式化推導(dǎo)相較于形式化驗證，較多強調(diào)在演繹系統(tǒng)內(nèi)工作的能力，通過形式化描述的斷言來“發(fā)現(xiàn)”程序[10]。該方法從問題的精確規(guī)約出發(fā)，在程序正確性證明理論的指導(dǎo)下進行程序開發(fā)，使整個程序的開發(fā)及其正確性證明同時進行，邊求精，邊推導(dǎo)，程序開發(fā)過程完成的同時，它的正確性也得到了保證。

Dijkstra[11]提出的最弱前置謂詞方法提供了賦值語句、選擇語句和循環(huán)語句的形式化推導(dǎo)方法，通過給出問題的精確程序規(guī)約，并以此作為程序設(shè)計的出發(fā)點，然后在程序驗證系統(tǒng)的指導(dǎo)下求解出所需的程序。將程序開發(fā)及其正確性證明“手拉手”地解決。程序每個片段的證明總是先于該片段代碼得到，這種方法的重點在開發(fā)程序而不是設(shè)計算法，它將程序正確性證明的理論融合到開發(fā)過程中，邊開發(fā)邊保證程序的正確性，自動化程度低。另外，用程序演算方法不能直接形式化推導(dǎo)出程序語句，且對于復(fù)雜程序難以進行推導(dǎo)。

文獻[12,13]從程序規(guī)約出發(fā)給出了最大分段和等問題的計算推導(dǎo)步驟，突出顯示了程序派生會話中涉及的典型步驟。其推導(dǎo)步驟基于最弱前置謂詞方法，并將后置斷言拆分成多個規(guī)約，再組成循環(huán)不變式，最終推導(dǎo)出正確的程序。這種方法依賴于后置斷言拆分分解后的規(guī)約，在面對較復(fù)雜程序規(guī)約時，尋找子規(guī)約的難度較大，并且隨著子規(guī)約的增多，推導(dǎo)過程會愈加繁瑣。

Kourie等[14]設(shè)計了一種基于構(gòu)建正確性的程序開發(fā)風(fēng)格，這種開發(fā)風(fēng)格結(jié)合了Dijkstra[11]的GCL(Guarded Command Language)語言和Morgan的精化演算規(guī)則，從問題的形式化規(guī)約開始，逐步將規(guī)約精化為代碼。其推導(dǎo)過程的難點在于這些算法的推導(dǎo)基于循環(huán)不變式，其循環(huán)不變式在推導(dǎo)開始時通過推測得來。然而，循環(huán)不變式的開發(fā)是循環(huán)程序的難點，復(fù)雜程序的循環(huán)不變式往往較難獲得[15]。

在文獻[16]中，作者使用PAR(Partition-And-Recur)方法[9,17]從形式規(guī)約出發(fā)，使用量詞的性質(zhì)等作為規(guī)則構(gòu)造出一組問題求解的遞推關(guān)系，從而推導(dǎo)出一組查找算法程序。其推導(dǎo)過程揭露了線性查找和折半查找的思想，在保證程序正確性的同時，提高了相關(guān)算法程序的設(shè)計效率。文獻闡述了常見的搜索算法的分劃方式，但是并沒有形成一套針對查找類問題的形式化推導(dǎo)方法。

綜上所述，對算法的形式化推導(dǎo)的研究是一項很有意義的工作，以上針對形式化推導(dǎo)方法的研究都取得了相應(yīng)成果，為該領(lǐng)域研究提供了重要參考。

3 序列折半劃分問題的形式化推導(dǎo)方法

折半劃分的前提要求為待劃分序列必須有序。為將折半劃分思想更加有效地應(yīng)用到序列劃分問題中，本文將序列進一步細分為“有序序列”和“循環(huán)序列”2種類型。針對這2種序列提出了序列折半劃分問題的形式化推導(dǎo)方法。該方法結(jié)合程序求精思想，將推理與形式化方法相結(jié)合，從抽象程度高的程序規(guī)約出發(fā)，經(jīng)過一系列的規(guī)約變換步驟，逐步降低規(guī)約的抽象程度，最終得到正確的Apla程序。整個過程可以概括為5個步驟，如圖1所示。

Figure 1 Flow chart of formal derivation method forsequence dimidiate partition problem圖1 序列折半劃分問題的形式化推導(dǎo)方法流程圖

圖1中，步驟1通過Spec1或Spec2和相應(yīng)的初始條件構(gòu)成問題規(guī)約；步驟2根據(jù)問題本身的特點以及序列中間元素的值對問題的可能情況進行分劃；步驟3對分劃的結(jié)果進行規(guī)約變換與化簡，形成問題的遞推關(guān)系式；步驟4將遞推關(guān)系式與初始條件結(jié)合得到問題的Radl(Recurrence-based algorithm design language)算法與循環(huán)不變式；步驟5將Radl算法等價轉(zhuǎn)換為Apla程序。接下來對這5個步驟進行詳細介紹。

3.1 構(gòu)造程序規(guī)約

構(gòu)造程序規(guī)約明確序列折半劃分問題的目標(biāo)，程序規(guī)約由前置斷言(Q)和后置斷言(R)構(gòu)成，用于精確地描述算法要完成的工作。

針對折半劃分問題先給出有序序列和循環(huán)序列的形式化定義。

定義1(有序序列) 有序序列指的是序列長度有限，在序列元素a[1],a[2],…,a[n]中，序列元素由小到大依次遞增，且不存在重復(fù)元素的序列。有序序列使用形式化定義可以描述為:

Spec1≡(?k,1≤k

(1)

其中，n為序列的長度。

定義2(循環(huán)序列) 如果在序列a[1],a[2],…,a[n]中存在某個i使得a[i]是序列中的最小元素，且序列a[i],a[i+1],…,a[n],a[1],…,a[n-1]是遞增的，則稱序列a[1],a[2],…,a[n]是循環(huán)序列。循環(huán)序列可以看作為2段有序序列的頭尾相連，并且第2段中元素的最大值a[n]小于第1段中元素的最小值a[1]，循環(huán)序列使用形式化定義可以描述為：

Spec2≡(?i,1

(?p,q,1≤p

a[p]

a[q+1]∧a[n]

(2)

基于上述有序序列和循環(huán)序列的形式化定義,可以得出針對有序序列或循環(huán)序列這一類劃分問題的形式化規(guī)約的一般形式：

Q:(Spec1|Spec2)∧初始條件

R:搜索結(jié)果。

根據(jù)該類問題規(guī)約的一般形式并結(jié)合待解決問題可以精確地刻畫出問題的程序規(guī)約。

3.2 分劃原問題

根據(jù)3.1節(jié)中的程序規(guī)約一般形式得出問題的程序規(guī)約后，將原問題進行分劃，分劃的核心思想為每一個子問題的解都可以由更小的子問題得出。基于這一思想，根據(jù)給定序列的特點，假設(shè)原問題為s(a,1,n),其中，1和n為序列的下標(biāo)，代表原問題在范圍a[1]～a[n]中尋找問題的解，通過序列中間位置下標(biāo)(1+n)/2將序列分為前、后2個子序列，根據(jù)具體問題與中間位置的值a[(1+n)/2]將原問題逐步分解為2個結(jié)構(gòu)相同且規(guī)模更小的子問題s(a,1,(1+n)/2)和s(a,(1+n)/2+1,n)。

若子問題總是可以被解決并且可以輸出查找結(jié)果，則可以通過分劃遞推法進行設(shè)計，通過分析子問題的特征，構(gòu)造求解規(guī)約并對規(guī)約進行變換,得到問題遞推關(guān)系。該過程能夠逐步正確推導(dǎo)出原問題的解。

針對序列類問題，分析給定序列的數(shù)學(xué)性質(zhì)以及具體問題，可以對原問題進行分劃，根據(jù)分劃過程中可能出現(xiàn)的情況，分劃過程的狀態(tài)可以分為“修改分劃范圍”和“分劃停止”2種：

(1)修改分劃范圍。

問題的初始范圍[1,n]即原序列的長度。在執(zhí)行過程中需要對范圍進行更改，通過修改下標(biāo)值的范圍形成子問題。

(2)分劃停止。

當(dāng)成功搜索到目標(biāo)值或子問題區(qū)間為一個點無法進一步分劃時，分劃停止，輸出結(jié)果。

3.3 尋找遞推關(guān)系

根據(jù)3.2節(jié)中分劃過程的狀態(tài)，可以得到問題的遞推關(guān)系F:s(a,1,n)=F(C,s(a,j,k))，其中，s(a,j,k)是s(a,1,n)的子問題，s(a,j,k)和約束條件C通過遞推關(guān)系F可以得到原問題s(a,1,n)的解。由此可以得到該類問題的通用遞推關(guān)系，如式(3)所示：

(3)

約束條件C1,C2,…,Cn滿足:

(?i,j,1≤i,j≤n∧i≠j:Ci∧Cj=False)∧

C1∨C2∨…∨Cn=True

(4)

3.4 得到Radl算法和循環(huán)不變式

Radl是一種基于遞推關(guān)系的算法設(shè)計語言，它的主要功能是描述問題的規(guī)約、規(guī)范變換規(guī)則和算法[18]。Radl算法是使用Radl語言描述的算法,Radl語言由算法規(guī)范語言和算法描述語言2部分組成。Radl被用作Apla語言的前端語言，使用傳統(tǒng)的數(shù)學(xué)習(xí)慣，且具有引用透明性，便于算法的形式推導(dǎo)和證明。

Radl語言的一般形式如下所示：

Algorithm:〈算法名稱〉

|[運算變量初始化定義]|

{Q∧R}〈算法規(guī)約〉

Begin:〈遞推控制變量〉;〈變量初始化賦值〉

Termination:〈遞推終止條件〉

Recur:〈遞推關(guān)系式F〉

End

在得到遞推關(guān)系之后，將遞推關(guān)系中出現(xiàn)的函數(shù)和變量的初始化條件刻畫出來，再把所有的遞推關(guān)系、遞推關(guān)系要滿足的初始化條件和求解問題的描述規(guī)約合并成一個Radl算法。根據(jù)遞推終止條件和遞推關(guān)系式，分析循環(huán)前后的信息，找出循環(huán)相關(guān)變量的變化規(guī)律，最后運用條件選擇斷言式可以快速得到循環(huán)不變式，其通用形式如式(5)所示：

∧1≤j≤k≤n+1

(5)

3.5 將Radl算法轉(zhuǎn)換為Apla程序

Apla是為實現(xiàn)算法程序形式化開發(fā)的一種抽象程序設(shè)計語言[19,20]，具有功能抽象、數(shù)據(jù)抽象和簡單易用等特點。Apla程序可讀性強，易于進行程序開發(fā)與形式化證明，且可以轉(zhuǎn)換成各種可執(zhí)行語言程序。

Radl語言是抽象程序設(shè)計語言Apla的前端語言，并且Radl和Apla中的標(biāo)識符、關(guān)鍵字和符號的表達方式完全一致。本文通過剖析Radl算法特性，揭示用遞推關(guān)系組表示的Radl算法與抽象順序程序Apla間的本質(zhì)關(guān)系，將Radl算法中無序的遞推語句轉(zhuǎn)化為順序程序?；赗adl語法產(chǎn)生式的Apla程序生成規(guī)則和Apla程序自動生成系統(tǒng),可以將Radl算法正確地轉(zhuǎn)換為可讀性好并且易于理解和驗證的Apla程序[18]。

4 工具：Apla到C++程序自動生成系統(tǒng)

因Apla語言不能直接編譯運行得到相應(yīng)的結(jié)果，為Apla語言編寫一個編譯器難度較大，而且難以在不同機器間移植，編譯器的正確性也難以得到保證。本文開發(fā)了一個自動程序轉(zhuǎn)換系統(tǒng)，將抽象Apla算法程序轉(zhuǎn)換成一個可執(zhí)行程序，這樣就可以通過編譯得到運行結(jié)果，由于將編譯成機器代碼的工作交給了第三方編譯器去完成，因而實現(xiàn)了算法程序的機器無關(guān)性，轉(zhuǎn)換系統(tǒng)的可靠性也易于保證。

該系統(tǒng)集詞法分析、語法分析、語義一致性分析、轉(zhuǎn)換、編譯和運行為一體，并為用戶提供了一個應(yīng)用界面，方便用戶將Apla程序轉(zhuǎn)換為正確的C++程序[21]，從而實現(xiàn)了從抽象到具體的程序求精過程。Apla到C++自動生成系統(tǒng)的總體結(jié)構(gòu)如圖2所示。

Figure 2 Overall structure of Apla to C++program automatic generation system 圖2 Apla到C++程序自動生成統(tǒng)總體結(jié)構(gòu)

5 2個折半劃分搜索實例的推導(dǎo)與生成

5.1 有序序列搜索特殊下標(biāo)

實例1問題描述：給定有序序列a[1],a[2],…,a[n]，試確定是否存在元素等于其下標(biāo)值，即a[i]=i。若存在則將i設(shè)為其下標(biāo)值，否則將i設(shè)為-1。

(1)構(gòu)造程序規(guī)約。

根據(jù)3.1節(jié)中的形式化規(guī)約一般形式，將初始條件設(shè)為i=0可構(gòu)造出如下規(guī)約：

Q:(?k,1≤k

R:i=-1∨((?k,1≤k≤n,a[k]=k)→i=k)

(2)分劃原問題并尋找遞推關(guān)系。

分劃原問題：設(shè)原問題為s(a,1,n),代表在[1,n]中搜索。利用折半劃分思想，搜索特殊下標(biāo)過程從數(shù)組的中間元素開始，對原問題進行如下分劃:

(6)

分別使用j和k來表示搜索空間的左邊界和右邊界，其中1≤j≤k≤n，可以得出該問題的一般形式,如式(7)所示：

(7)

式(7)將s(a,j,k)分劃成2個子問題，表示s(a,j,k)的解可以通過s(a,j,(j+k)/2)和s(a,(j+k)/2+1,k)的F運算得到。

尋找遞推關(guān)系：s(a,j,k)代表在[j,k]中搜索滿足條件a[i]=i的i，分劃的關(guān)鍵在于比較a[(j+k)/2]與(j+k)/2的大小。根據(jù)中間元素下標(biāo)判斷特殊下標(biāo)i的位置，設(shè)中間元素下標(biāo)為m，在此問題中，若a[m]

①若j=k，搜索區(qū)間變?yōu)楣潭c，直接判斷點k是否為特殊下標(biāo)。若點k是特殊下標(biāo)，則將i設(shè)為k，否則將i設(shè)為-1。

②若(j+k)/2>a[(j+k)/2]，則將j設(shè)為(j+k)/2+1。

③若(j+k)/2≤a[(j+k)/2]，則將k設(shè)為(j+k)/2。

根據(jù)可能情況對形式化規(guī)約進行變換：

s(a,j,k)≡s(a,j,(j+k)/2)∨

s(a,(j+k)/2+1,k)∨k∨-1

{范圍分裂}

s(a,j,k)≡(j=k∧(a[k]=k∧s(a,j,k))=k∨(a[k]≠k∧s(a,j,k)=-1))∨((j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k))∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{分配律}

s(a,j,k)≡(s(a,j,k)=-1)∨(s(a,j,k)=x∧(?x,j≤x≤k:a[x]=x))∨(j=k∧a[k]=k∧s(a,j,k)=k)∨(j=k∧a[k]≠k∧s(a,j,k)=-1)∨((j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k))∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{化簡}

s(a,j,k)≡s(a,j,(j+k)/2)∨s(a,(j+k)/2+1,k)∨k∨-1

化簡后可得到遞推關(guān)系，如式(8)所示:

s(a,j,k)=

(8)

Figure 3 Automatically generating ordered sequence search special subscript program圖3 自動生成有序序列搜索特殊下標(biāo)程序

(3)構(gòu)造Radl算法和循環(huán)不變式。

根據(jù)式(8)和初始值，構(gòu)造Radl算法，如算法1所示：

算法1實例1.Radl

輸入：有序序列a[1],a[2],…,a[n]。

輸出：特殊下標(biāo)值i。

1. |[i,j,k:integer;a:array[1..n,integer];]|;

2. {Q∧R};

3.Begin：i,j,k=0,1,n;

4.Termination：j>k;

5.Recur：Formula (8);

6.End

根據(jù)式(8)和循環(huán)終止條件，并約束j和k的變化范圍，將(j+k)/2用變量m表示，可以得出該程序的循環(huán)不變式,如式(9)所示：

ρ:a[m]≥m→s(a,j,k)=s(a,j,m)∨

a[m]

s(a,m+1,k)∧1≤j≤k+1≤n+1

(9)

(4)將Radl算法轉(zhuǎn)換為Apla程序。

根據(jù)算法1和式(9)可得出如下Apla算法:

算法2實例1.Apla

輸入：有序序列a[1],a[2],…,a[n]。

輸出：特殊下標(biāo)值i。

1.j:=1;k:=n;m:=(1+n)/2;i:=0;

2.do(j≤k)→m:=(j+k) div 2;

3.if(j=k)→if(a[j]=j)→i:=k;

4.[]→i:=-1;fi;j:=j+1;fi;

5.if(a[m]

6.if(a[m] ≥m)→k:=m;fi;

7.od;

(5)實例C++算法的自動生成。

將算法2輸入到Apla到C++程序自動生成系統(tǒng)中，可以得到圖3所示的轉(zhuǎn)換結(jié)果。圖3中，左側(cè)代碼對應(yīng)算法的Apla程序，右側(cè)代碼為驗證后自動生成的C++程序。

可以發(fā)現(xiàn)，相較于自動生成的C++程序，抽象算法程序Apla可以通過非常簡短的語句來精確描述算法功能。對生成的2段C++代碼隨機輸入測試數(shù)據(jù)，運行結(jié)果如圖4所示。

Figure 4 Execution result of ordered sequence search special subscript program 圖4 有序序列搜索特殊下標(biāo)程序執(zhí)行結(jié)果

經(jīng)過驗證，程序能夠執(zhí)行。由于Apla到C++系統(tǒng)可以確保Apla代碼轉(zhuǎn)換到C++代碼過程的語義等價性，因此可以確定生成的C++程序是完全正確的，從而免于驗證繁瑣的C++程序，大幅提高了軟件開發(fā)效率并保證了軟件的可靠性和正確性。

5.2 循環(huán)序列搜索最小元素下標(biāo)

實例2問題描述：對于一個已知的循環(huán)序列，找出其中最小元素的位置i。

(1)構(gòu)造程序規(guī)約。

Q:(?i,1

R:?k,1≤k≤n:a[k]≥a[i]

(2)分劃原問題并尋找遞推關(guān)系。

分劃原問題：將原問題設(shè)為s(a,1,n)，代表在[1,n]中尋找最小元素的位置i，為實現(xiàn)該算法，對原問題進行如下分劃：

(10)

分別使用j和k來表示搜索空間的左邊界和右邊界可得出該問題的一般形式，如式(11)所示：

(11)

尋找遞推關(guān)系：針對此問題，可以比較范圍邊界值a[j]和a[k]，其中ja[k]，則i就一定落在區(qū)間(j,k]中，因為在這個區(qū)間內(nèi)，元素的順序發(fā)生了跳變。通過這種分劃方法，能在O(logn)次比較后找到i。分劃的關(guān)鍵在于比較a[(j+k)/2]與a[k]的大小，故有3種可能情況：

① 若j=k，代表找到最小元素下標(biāo)，搜索區(qū)間變?yōu)楣潭c，此時將i設(shè)為k;

② 若a[(j+k)/2]

③ 若a[(j+k)/2]>a[k]，代表該范圍元素順序發(fā)生跳變，此時將j設(shè)為(j+k)/2+1。

根據(jù)可能情況對形式化規(guī)約進行變換：

s(a,j,k)≡

(s(a,j,k)=i∧(mini:1≤i≤n:a[i]))

{范圍分裂}

s(a,j,k)≡(j=k∧s(a,j,k)=k)∨(a[k]>a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))∨(a[k]

{分配律}

s(a,j,k)≡(s(a,j,k=-1)∨(s(a,j,k)=x∧(?x,j≤x≤k:a[x]=x))∨(j=k∧a[k]=k∧s(a,j,k)=k)∨(j=k∧a[k]≠k∧s(a,j,k)=-1)∨(j+k)/2>a[(j+k)/2]∧s(a,j,k)=s(a,(j+k)/2+1,k)∨((j+k)/2≤a[(j+k)/2]∧s(a,j,k)=s(a,j,(j+k)/2))

{化簡}

s(a,j,k)≡s(a,j,(j+k)/2)∨s(a,(j+k)/2+1,k)∨k

化簡后可得到遞推關(guān)系，如式(12)所示:

s(a,j,k)=

(12)

(3)構(gòu)造Radl算法和循環(huán)不變式。

根據(jù)遞推關(guān)系式(12)及初始值，可得解此問題的Radl算法，如算法3所示：

算法3實例2.Radl

輸入：循環(huán)序列a[1],a[2],…,a[n]。

輸出：特殊下標(biāo)值i。

1.|[i,j,k:integer;a:array[1..n,integer];]|;

2.{Q∧R};

3.Begin：i,j,k=0,1,n;

4.Termination：j>k;

5.Recur:Formula (12);

6.End

根據(jù)式(12)和循環(huán)終止條件，并約束j和k的變化范圍，將(j+k)/2用變量m代替，可以得出該程序的循環(huán)不變式，如式(13)所示：

ρ：a[k]>a[m]→s(a,j,k)=

s(a,j,m)∨a[k]

s(a,m+1,k)∧1≤j≤k+1≤n+1

(13)

(4)將Radl算法轉(zhuǎn)換為Apla程序。

根據(jù)算法3和式(13)，可得出如下Apla算法：

算法4實例2.Apla

輸入：循環(huán)序列a[1],a[2],…,a[n]。

輸出：最小元素下標(biāo)值i。

1.j:=1;k:=n;m:=(1+n)/2;i:=0;

2.do(j≤k)→m:=(j+k) div 2;

3.if(j=k)→i:=k;j:=j+1;fi;

4.if(a[m]

5.[]→j:=m+1;fi;

6.od;

(5)實例C++算法的自動生成。

將算法4輸入到Apla到C++程序自動生成系統(tǒng)中，可以得到圖5所示的轉(zhuǎn)換結(jié)果。圖6為自動生成的C++程序代碼正確運行的結(jié)果。

Figure 5 Automatically generating loop sequence search minimum element subscript program圖5 自動生成循環(huán)序列搜索最小元素下標(biāo)程序

Figure 6 Execution result of loop sequence search minimum element subscript program 圖6 循環(huán)序列搜索最小元素下標(biāo)程序執(zhí)行結(jié)果

6 結(jié)束語

本文以序列折半劃分問題為研究對象，運用分劃遞推的核心思想，探討該類問題的共性，提出了序列折半劃分問題的形式化推導(dǎo)方法。通過“有序序列搜索特殊下標(biāo)”和“循環(huán)序列搜索最小值下標(biāo)”2個實例驗證了本文方法的可行性。與現(xiàn)有研究相比，本文方法具有以下特點：

(1)運用規(guī)約變換技術(shù)對問題規(guī)約進行變換并嚴(yán)格保證一致性，免于繁瑣的證明，使得推導(dǎo)過程更加簡潔。

(2)該方法包括了完整的程序求精過程，實現(xiàn)了從程序規(guī)約到C++程序的完整轉(zhuǎn)換過程。

(3)相較于以往的靠靈感和經(jīng)驗開發(fā)算法程序，本文把算法設(shè)計過程轉(zhuǎn)變?yōu)橐?guī)范化的算法程序生成過程，這一過程確保了程序的可靠性與正確性。