序列折半劃分問題的形式化推導*

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

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

1 引言

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

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

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

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

2 相關工作

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

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

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

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

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

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

3 序列折半劃分問題的形式化推導方法

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

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

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

3.1 構造程序規(guī)約

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

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

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

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:搜索結果。

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

3.2 分劃原問題

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

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

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

(1)修改分劃范圍。

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

(2)分劃停止。

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

3.3 尋找遞推關系

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

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

Algorithm:〈算法名稱〉

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

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

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

Termination:〈遞推終止條件〉

Recur:〈遞推關系式F〉

End

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

∧1≤j≤k≤n+1

(5)

3.5 將Radl算法轉換為Apla程序

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

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

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

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

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

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

5 2個折半劃分搜索實例的推導與生成

5.1 有序序列搜索特殊下標

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

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

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

Q:(?k,1≤k

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

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

分劃原問題：設原問題為s(a,1,n),代表在[1,n]中搜索。利用折半劃分思想，搜索特殊下標過程從數(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運算得到。

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

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

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

③若(j+k)/2≤a[(j+k)/2]，則將k設為(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

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

s(a,j,k)=

(8)

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

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

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

算法1實例1.Radl

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

輸出：特殊下標值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算法轉換為Apla程序。

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

算法2實例1.Apla

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

輸出：特殊下標值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所示的轉換結果。圖3中，左側代碼對應算法的Apla程序，右側代碼為驗證后自動生成的C++程序。

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

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

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

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

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

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

Q:(?i,1

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

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

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

(10)

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

(11)

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

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

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

③ 若a[(j+k)/2]>a[k]，代表該范圍元素順序發(fā)生跳變，此時將j設為(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

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

s(a,j,k)=

(12)

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

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

算法3實例2.Radl

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

輸出：特殊下標值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算法轉換為Apla程序。

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

算法4實例2.Apla

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

輸出：最小元素下標值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所示的轉換結果。圖6為自動生成的C++程序代碼正確運行的結果。

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

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

6 結束語

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

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

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

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