序列折半劃分問(wèn)題的形式化推導(dǎo)*

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

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

1 引言

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

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

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

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

2 相關(guān)工作

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Spec1≡(?k,1≤k

(1)

其中，n為序列的長(zhǎng)度。

定義2(循環(huán)序列) 如果在序列a[1],a[2],…,a[n]中存在某個(gè)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)序列的形式化定義,可以得出針對(duì)有序序列或循環(huán)序列這一類劃分問(wèn)題的形式化規(guī)約的一般形式：

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

R:搜索結(jié)果。

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

3.2 分劃原問(wèn)題

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

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

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

(1)修改分劃范圍。

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

(2)分劃停止。

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

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

根據(jù)3.2節(jié)中分劃過(guò)程的狀態(tài)，可以得到問(wèn)題的遞推關(guān)系F:s(a,1,n)=F(C,s(a,j,k))，其中，s(a,j,k)是s(a,1,n)的子問(wèn)題，s(a,j,k)和約束條件C通過(guò)遞推關(guān)系F可以得到原問(wèn)題s(a,1,n)的解。由此可以得到該類問(wè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è)計(jì)語(yǔ)言，它的主要功能是描述問(wèn)題的規(guī)約、規(guī)范變換規(guī)則和算法[18]。Radl算法是使用Radl語(yǔ)言描述的算法,Radl語(yǔ)言由算法規(guī)范語(yǔ)言和算法描述語(yǔ)言2部分組成。Radl被用作Apla語(yǔ)言的前端語(yǔ)言，使用傳統(tǒng)的數(shù)學(xué)習(xí)慣，且具有引用透明性，便于算法的形式推導(dǎo)和證明。

Radl語(yǔ)言的一般形式如下所示：

Algorithm:〈算法名稱〉

|[運(yùn)算變量初始化定義]|

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

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

Termination:〈遞推終止條件〉

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

End

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

∧1≤j≤k≤n+1

(5)

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

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

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

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

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

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

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

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

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

實(shí)例1問(wèn)題描述：給定有序序列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)分劃原問(wèn)題并尋找遞推關(guān)系。

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

(6)

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

(7)

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

尋找遞推關(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，在此問(wèn)題中，若a[m]

①若j=k，搜索區(qū)間變?yōu)楣潭c(diǎn)，直接判斷點(diǎn)k是否為特殊下標(biāo)。若點(diǎn)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ù)可能情況對(duì)形式化規(guī)約進(jìn)行變換：

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))

{化簡(jiǎn)}

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

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

s(a,j,k)=

(8)

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

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

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

算法1實(shí)例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實(shí)例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)實(shí)例C++算法的自動(dòng)生成。

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

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

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

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

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

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

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

Q:(?i,1

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

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

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

(10)

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

(11)

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

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

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

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

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

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))

{化簡(jiǎn)}

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

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

s(a,j,k)=

(12)

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

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

算法3實(shí)例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實(shí)例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)實(shí)例C++算法的自動(dòng)生成。

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

Figure 5 Automatically generating loop sequence search minimum element subscript program圖5 自動(dòng)生成循環(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é)束語(yǔ)

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

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

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

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