譚 旺，李 軼

（1.中國(guó)科學(xué)院重慶綠色智能技術(shù)研究院，重慶 400714；2.中國(guó)科學(xué)院大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，北京 101408）

0 引言

循環(huán)程序終止性的分析與驗(yàn)證已成為程序驗(yàn)證領(lǐng)域的一個(gè)熱點(diǎn)問題，并且引起了國(guó)內(nèi)外許多學(xué)者的關(guān)注［1-3］。循環(huán)程序的終止性是一個(gè)不可判定的問題［4-6］，它的解決方案可以廣泛地提高軟件的可靠性以及程序員的工作效率。目前有幾種優(yōu)秀的工具應(yīng)用于不同計(jì)算模型的自動(dòng)終止性驗(yàn)證分析［7-8］。證明給定循環(huán)程序是否是可終止的有著許多的研究方法，比如特征值法［9］、秩函數(shù)法［10-17］、界函數(shù)法［18-22］、抽象解釋［23-25］以及不變式［26-27］等。

秩函數(shù)法作為終止性分析的主流方法已經(jīng)得到了廣泛的研究。當(dāng)前求解秩函數(shù)的方法大多局限于線性秩函數(shù)［10-13］或者多項(xiàng)式秩函數(shù)［14-17］的求解。本文主要考慮給定循環(huán)的界函數(shù)計(jì)算問題，在循環(huán)程序體內(nèi)設(shè)置一個(gè)循環(huán)計(jì)數(shù)器變量c，然后計(jì)算循環(huán)計(jì)數(shù)器變量的上界，不難看出，循環(huán)計(jì)數(shù)器變量的上界實(shí)際上就是某給定初始值的循環(huán)迭代次數(shù)的一個(gè)上界。如果對(duì)于任意滿足循環(huán)條件的初始值，其對(duì)應(yīng)的循環(huán)計(jì)數(shù)器變量均存在上界，那么該循環(huán)程序一定是可終止的。具體地，本文首先設(shè)定一個(gè)界函數(shù)模板并且將界函數(shù)的求解問題轉(zhuǎn)化為線性二分類問題，然后利用支持向量機(jī)（Support Vector Machine，SVM）［28］探測(cè)分類超平面獲得模板系數(shù)從而得到候選的界函數(shù)，最后將候選界函數(shù)進(jìn)行優(yōu)化并采用符號(hào)驗(yàn)證工具Redlog 對(duì)其進(jìn)行驗(yàn)證。與基于秩函數(shù)的循環(huán)程序終止性驗(yàn)證問題相比，盡管計(jì)算循環(huán)程序計(jì)數(shù)器變量十分困難，即界函數(shù)方法是一個(gè)更為復(fù)雜的問題［29］，但是，本文的實(shí)驗(yàn)結(jié)果表明，對(duì)于某些不能通過計(jì)算線性秩函數(shù)或線性多階段秩函數(shù)來證明其終止性的循環(huán)，通過本文方法卻可以找到其線性界函數(shù)，從而證明這些循環(huán)的終止性。

1 預(yù)備知識(shí)

本文主要考慮如下形式循環(huán)，即：

其中：a=(a1，a2，…，ak)T∈Rk是一個(gè)k維向量，不等式≤0 是程序的循環(huán)條件，而=fi(a)中的表示ai在經(jīng)過一次循環(huán)迭代后的值，并且=fi(a)是循環(huán)的賦值表達(dá)式，其中fi(a)是連續(xù)函數(shù)。

令a′=以及f(a)=(f1(a)，f2(a)，…，fk(a))T，因此，可得a′=f(a)。

例1 考慮以下來自文獻(xiàn)［12］的循環(huán)：

在這個(gè)循環(huán)中，循環(huán)條件是4a1+a2≥1，循環(huán)區(qū)域?yàn)棣?{a∈R2：4a1+a2≥1}；賦值語句是=-2a1+4a2以及=4a1。

1.1 界函數(shù)

如果一個(gè)循環(huán)程序在滿足循環(huán)條件內(nèi)的所有初始值上均是可終止的，那么該循環(huán)程序便是可終止程序。對(duì)于可終止循環(huán)程序，滿足循環(huán)條件的初始點(diǎn)在有限次迭代之后必然跳出Ω。給定一個(gè)可終止循環(huán)P，令C(a)：Ω→N 為初始值輸入點(diǎn)a在循環(huán)P中的有窮次迭代次數(shù)。為方便，本文稱C(a)為Ω（或程序P）的迭代次數(shù)函數(shù)。對(duì)?a∈Ω，有C(a)≥1。

一般地，要精確計(jì)算C(a)是困難的。為此引入界函數(shù)的概念來逼近C(a)。函數(shù)的定義如下：

定義1給定循環(huán)程序P。令C(a)為程序P上的迭代次數(shù)函數(shù)。如果存在函數(shù)τ(a)，使得?a∈Ω，有τ(a)≥C(a)，則稱τ(a)為程序P的界函數(shù)。

從定義可以看出，對(duì)一個(gè)循環(huán)程序，若能夠求解出其對(duì)應(yīng)的界函數(shù)，那么初始值的迭代次數(shù)均會(huì)有一上界（即：該初始值必在有窮次迭代后跳出Ω）。因此，如果任意初始值a∈Ω均能夠在有窮次迭代后跳出Ω，那么該循環(huán)程序就是終止的。

1.2 支持向量機(jī)

支持向量機(jī)［30］是一種對(duì)數(shù)據(jù)進(jìn)行二元分類的廣義線性分類器，提出后便得到了廣泛的關(guān)注和持續(xù)的發(fā)展。此外，由于支持向量機(jī)方法已經(jīng)逐步理論化并成為統(tǒng)計(jì)學(xué)習(xí)理論的一部分［31］，并且是建立在結(jié)構(gòu)風(fēng)險(xiǎn)最小原理基礎(chǔ)上的，因此，其堅(jiān)實(shí)的理論基礎(chǔ)以及良好的特性使得現(xiàn)在很多領(lǐng)域都對(duì)其有著廣泛的應(yīng)用，例如：模式識(shí)別、概率密度估計(jì)和回歸估計(jì)等。本文將界函數(shù)計(jì)算問題歸結(jié)為線性二分類問題，從而可以利用支持向量機(jī)探測(cè)候選界函數(shù)。

假設(shè)給定訓(xùn)練樣本集D={(x1，y1)，(x2，y2)，…，(xk，yk)}，其中yi∈{-1，+1}。樣本空間的劃分問題即是否能夠找到一個(gè)超平面wTx+b=0 使得這兩類點(diǎn)分離，其中：w為法向量，決定了超平面的方向，而b則是位移項(xiàng)。支持向量機(jī)算法的作用便是能夠找到向量w以及實(shí)數(shù)b使得(xi，yi)∈D滿足［32］：

特別地，支持向量機(jī)能夠找到向量w使得：

1.3 不變式

程序不變式指的是程序變量之間滿足的并且不隨程序狀態(tài)遷移發(fā)生變化的關(guān)系。當(dāng)前，線性循環(huán)不變式以及多項(xiàng)式循環(huán)不變式的生成都取得了很大的進(jìn)展，構(gòu)造程序不變式已成為軟件自動(dòng)驗(yàn)證領(lǐng)域內(nèi)的重要研究?jī)?nèi)容。程序不變式的一般定義如下：

定義2給定帶初始值的循環(huán)程序P0：

如果存在表達(dá)式I(a)滿足下列兩個(gè)條件：

那么，I(a)稱為循環(huán)P0的循環(huán)不變式。其中：θ表示初始點(diǎn)集合；initial 條件表明循環(huán)的第一次迭代前，循環(huán)不變式為真；consecutive 條件表明如果在循環(huán)體內(nèi)某次迭代前為真，那么迭代后仍保持為真。

2 界函數(shù)的合成

本章描述了循環(huán)程序界函數(shù)的合成方法，主要包括了如何將合成界函數(shù)的問題轉(zhuǎn)換為分類問題，如何構(gòu)建訓(xùn)練集，如何獲得分類超平面來確定候選界函數(shù)，如何對(duì)候選界函數(shù)進(jìn)行優(yōu)化，以及如何構(gòu)建測(cè)試集。

2.1 問題轉(zhuǎn)換

本節(jié)將會(huì)介紹如何將界函數(shù)的求解問題轉(zhuǎn)化為分類問題。

令a=(a1，a2，…，ak)T∈Rk，其中k為Ω中點(diǎn)的維數(shù)。令τ(a)=wT·V(a)為循環(huán)程序P的界函數(shù)，其中wT為參數(shù)。τ(a)便是所設(shè)置的界函數(shù)模板，其中，V(a)由單項(xiàng)式或多項(xiàng)式所構(gòu)成。

根據(jù)迭代函數(shù)的定義，可得

又由界函數(shù)的定義，有

也即：對(duì)?a∈Ω，可得

故?a∈Ω，可得

綜上所述，界函數(shù)的計(jì)算問題可以被歸結(jié)為負(fù)類點(diǎn)u-與集合T的超平面劃分問題，而這是一個(gè)典型的二分類問題。由于T是無窮點(diǎn)集，為了便于利用SVM 去求解該超平面，需要首先從T中抽取有限個(gè)樣本點(diǎn)構(gòu)成T0，故負(fù)類點(diǎn)u-與集合T的超平面劃分問題便被轉(zhuǎn)化為u-與集合T0的超平面劃分問題。若u-與有限點(diǎn)集T0之間的超平面一旦被計(jì)算，就可以得到了一個(gè)“候選的界函數(shù)”，然后利用Redlog 工具去驗(yàn)證該候選界函數(shù)是否是真的界函數(shù)。

例2 考慮例1 所示循環(huán)。

本例中設(shè)置其界函數(shù)模板為：

τ(a1，a2)=w1·(a1+1)2+w2·(a2+1)2+w3

即：

由T的定義，

故可得兩類點(diǎn)集合為：

即：本文需要找到一個(gè)線性超平面L(u)：=wT·u=0 將u-與集合T嚴(yán)格分離。

2.2 超平面的求解

從2.1 節(jié)可知，本文將候選界函數(shù)的求解問題轉(zhuǎn)化為一個(gè)u-與T0之間的二分類問題，即找到u-與T0之間的超平面L(u)：=wT·u=0，從而獲得候選界函數(shù)的系數(shù)wT，進(jìn)而得到候選的界函數(shù)τ(a)=wT·V(a)。為此，本文首先需要構(gòu)造訓(xùn)練集，而構(gòu)造訓(xùn)練集的一般過程分為兩步：一是構(gòu)造正類點(diǎn)集合T0和負(fù)類點(diǎn)u-；二是對(duì)所獲得的樣本點(diǎn)打上標(biāo)簽。過程如下：

1）正類點(diǎn)集合T0和負(fù)類點(diǎn)u-。

首先需要在循環(huán)區(qū)域Ω中自定義采樣區(qū)間并采n個(gè)樣本點(diǎn)，即針對(duì)每一個(gè)變量自定義取值范圍，其中i∈{1，2，…，k}，而這里的以及n為可調(diào)參數(shù)；然后針對(duì)每一個(gè)采樣點(diǎn)，求解出其精確迭代次數(shù)，之后通過T=映射到U空間，本文將該映射關(guān)系令為H，這樣便獲得了正類點(diǎn)集合T0，其次，還需要找到一個(gè)負(fù)類點(diǎn)u-，滿足u-?T，而實(shí)驗(yàn)中只需要找到一個(gè)這樣的點(diǎn)作為負(fù)類點(diǎn)即可。這樣的點(diǎn)是容易選取的。

例3 考慮例1 中的循環(huán)（續(xù)例2）。

由于該循環(huán)的循環(huán)區(qū)域Ω為：4a1+a2≥1，因此需要在像空間U空間外找尋一個(gè)樣本點(diǎn)作為反例點(diǎn)u-。本例中選取反例點(diǎn)為（0，0，1）。由于該循環(huán)區(qū)域Ω為無界區(qū)域，因此為構(gòu)造樣本集T0需要在Ω中自定義一個(gè)有界的采樣區(qū)間進(jìn)行采樣，這里設(shè)定采樣區(qū)間為a1∈(-100，100) 以及a2∈（-100，100）。

2）打標(biāo)簽。

在得到樣本點(diǎn)之后，還需要對(duì)樣本點(diǎn)打上標(biāo)簽，正例點(diǎn)打上+1，負(fù)例點(diǎn)打上-1。

算法1 描述了求解樣本點(diǎn)真實(shí)迭代次數(shù)的過程，針對(duì)某一給定樣本點(diǎn)以及循環(huán)程序，求解出該樣本點(diǎn)在循環(huán)程序中的迭代次數(shù)。

算法2 描述了訓(xùn)練集的構(gòu)建過程。首先確定采樣個(gè)數(shù)，然后針對(duì)所采樣本點(diǎn)用上述的映射關(guān)系映射到U空間得到集合T0，之后選取一負(fù)類點(diǎn)u-使之滿足u-∈L-，最后分別對(duì)正類點(diǎn)以及負(fù)類點(diǎn)打上標(biāo)簽。

在得到訓(xùn)練集xtrain以及ytrain之后，便可以通過SVM 進(jìn)行訓(xùn)練。從上述構(gòu)造訓(xùn)練集的過程可以看出，無論所選取的界函數(shù)模板為何形式，都可以將樣本點(diǎn)映射到U空間，使得界函數(shù)的計(jì)算問題可以直接轉(zhuǎn)化為一個(gè)線性二分類問題。因此在利用SVM 的訓(xùn)練過程中均采用線性核函數(shù)，在用訓(xùn)練集進(jìn)行訓(xùn)練之后，所求得超平面如下：

且對(duì)?(u1，u2，…，ud)∈T0，有

若1-wd+1>0，則由式（9），對(duì)?(u1，u2，…，ud)∈T0，有

可得到一個(gè)新的超平面L(u)=WT·u，且對(duì)?u∈T0，有L(u)≥1，即T0在L(u)的正半部分。

當(dāng)1-wd+1<0 時(shí)，將重新構(gòu)建訓(xùn)練集進(jìn)行訓(xùn)練。

因此根據(jù)事先設(shè)定的模板，便可以得到候選界函數(shù)為：

例4 對(duì)于例1 中的循環(huán)程序（續(xù)接例3）。

將例3 所得到的訓(xùn)練集代入SVM 模型進(jìn)行訓(xùn)練之后，可以得到分類超平面系數(shù)為：

因此可以得到：

則候選界函數(shù)為：

τ(a1，a2)=5.868 054 17(a1+1)2+5.922 738 91(a2+1)2-4.982 226 63

2.3 候選界函數(shù)的優(yōu)化

通過上述對(duì)超平面的求解，可以得到界函數(shù)的模板系數(shù)，進(jìn)而得到候選的界函數(shù)。此外，根據(jù)界函數(shù)自身獨(dú)特的性質(zhì)，可以對(duì)候選界函數(shù)通過一些方法進(jìn)行優(yōu)化，使其有更大的可能通過后續(xù)的精確驗(yàn)證。

根據(jù)界函數(shù)的性質(zhì)，界函數(shù)滿足：?a∈Ω，τ(a)≥C(a)。因此，本文將候選的界函數(shù)進(jìn)行放大操作得到τ′(a)，使其滿足：

因此，如果能夠通過優(yōu)化得到τ′(a)，那么本文最終只需驗(yàn)證τ′(a)是否是真正的界函數(shù)，即驗(yàn)證τ′(a)≥C(a)。

本文將分為以下幾個(gè)情況對(duì)候選τ(a)進(jìn)行處理：

1）令出現(xiàn)在τ(a)中的程序變量集S={}，其中ij∈{1，2，…，k}。如果存在ij，使得在Ω上恒為正或者恒為負(fù)，那么就可以將這種情形下的τ(a)進(jìn)行優(yōu)化放大處理。

3）對(duì)于候選界函數(shù)中的常數(shù)項(xiàng)，可以始終對(duì)其進(jìn)行放大處理：一是當(dāng)所求的常數(shù)項(xiàng)范圍在（-1，1），可以直接將其放大至1；二是當(dāng)所求的常數(shù)項(xiàng)范圍為(-∞，-1)，將其上取整再取平方值。通過放大常數(shù)項(xiàng)系數(shù)，使得候選的界函數(shù)有更大的可能通過后續(xù)的驗(yàn)證。

例5 考慮例1 中的循環(huán)，續(xù)接例4。

由于其程序變量在Ω上有正有負(fù)，所以將該程序變量在模板中系數(shù)設(shè)為2，由設(shè)置的界函數(shù)模板易得，變量項(xiàng)(a1+1)2與(a2+1)2均為正項(xiàng)，因此其系數(shù)可以進(jìn)行放大處理（如：向上取整）。

根據(jù)例4 所得的超平面系數(shù)，可以得到候選界函數(shù)為，

τ(a1，a2)=5.868 054 17(a1+1)2+5.922 738 91(a2+1)2-4.982 226 63

于是將所得的候選界函數(shù)變量項(xiàng)前的系數(shù)進(jìn)行向上取整，可得：

τ′(a1，a2)=6(a1+1)2+6(a2+1)2-4.982 226 63

再對(duì)常數(shù)項(xiàng)進(jìn)行處理，可得最終的候選界函數(shù)為：

τ″(a1，a2)=6(a1+1)2+6(a2+1)2+25

2.4 測(cè)試集

在得到候選的界函數(shù)之后，還需要在精確驗(yàn)證前構(gòu)造一個(gè)測(cè)試集對(duì)其進(jìn)行初步的驗(yàn)證，當(dāng)所獲得的候選界函數(shù)沒能夠通過測(cè)試集時(shí)，可以將未通過的測(cè)試樣本點(diǎn)添加進(jìn)入訓(xùn)練集，然后再重新訓(xùn)練，或者可以通過調(diào)整負(fù)類點(diǎn)的值，再進(jìn)行訓(xùn)練。測(cè)試集構(gòu)造過程如下：本文將上述所得的候選界函數(shù)稱為candidate_BF，在循環(huán)條件圍成的區(qū)域Ω中隨機(jī)抽取采樣點(diǎn)若干次。然后針對(duì)每一個(gè)樣本點(diǎn)代入candidate_BF求解得到該樣本點(diǎn)的迭代次數(shù)上界c_cal。最后著代入C(a)求解其真實(shí)的迭代次數(shù)c_real，若出現(xiàn)c_cal

3 精確驗(yàn)證

本章將介紹如何對(duì)上述所得的候選界函數(shù)進(jìn)行進(jìn)一步的精確驗(yàn)證。得到候選界函數(shù)之后，并且該函數(shù)已經(jīng)通過測(cè)試集驗(yàn)證，但測(cè)試集僅是離散的樣本點(diǎn)，遠(yuǎn)遠(yuǎn)不能表征整個(gè)循環(huán)區(qū)域Ω，因此，還需要對(duì)其進(jìn)行進(jìn)一步的精確驗(yàn)證以保證所得到的候選界函數(shù)在整個(gè)Ω內(nèi)滿足界函數(shù)的性質(zhì)。本文采用的方法是：首先找出循環(huán)中的不變式，然后通過不變式以及工具Redlog 去驗(yàn)證所得到的函數(shù)是否滿足界函數(shù)的性質(zhì)。

3.1 不變式的構(gòu)建

構(gòu)建不變式，首先需要設(shè)定不變式的模板，本文不變式的模板與前述提及的界函數(shù)模板保持一致。假定不變式為I(a，c)：=MT·V(a)≥c，其中MT=(m1，m2，…，md)為參數(shù)，c為程序的計(jì)數(shù)變量用于計(jì)算迭代次數(shù)。根據(jù)不變式的性質(zhì)，可得：

能夠同時(shí)滿足A、B 兩式的表達(dá)式便是該循環(huán)的不變式，令A(yù) 式中MT以及a*需要滿足的范圍為M0，采用Redlog 工具對(duì)B 式進(jìn)行量詞消去（Quantifier Elimination，QE），消去(a，c)，可以得到不變式模板系數(shù)MT需要滿足的范圍M1。其中，a*為初始輸入，本文將其參數(shù)化。

3.2 候選界函數(shù)的驗(yàn)證

構(gòu)建不變式是為了利用不變式來驗(yàn)證候選界函數(shù)，如果該循環(huán)存在一個(gè)不變式能夠推出候選界函數(shù)為真，那么該候選界函數(shù)就為真正的界函數(shù)?；诖?，可得：

采用Redlog 工具對(duì)式（14）進(jìn)行量詞消去，消去(a，c)，可以得到式（14）中MT以及a*需要滿足范圍M2。

綜上：對(duì)兩次所得到的MT范圍求交，判斷是否存在一組MT，使其滿足A、B、C 三式。因此，可得：

同樣采用Redlog 工具對(duì)式（15）進(jìn)行量詞消去，消去MT，可以得到滿足式（15）中a*需要滿足的范圍M3。對(duì)滿足M3的初始值a*必存在一組MT使得該循環(huán)存在一個(gè)不變式I(a，c)：=MT·V(a)≥c，該不變式能夠蘊(yùn)含候選界函數(shù)。

因此最終還需要驗(yàn)證是否對(duì)于整個(gè)循環(huán)區(qū)域內(nèi)的初始點(diǎn)都存在一個(gè)不變式，使得該不變式能夠推出候選界函數(shù)為真，即驗(yàn)證是否循環(huán)區(qū)域Ω都在M3內(nèi)部。

依然采用Redlog 工具對(duì)式（16）進(jìn)行量詞消去，消去a*，若最終輸出結(jié)果為真，那么表示整個(gè)循環(huán)區(qū)域內(nèi)的點(diǎn)均能夠找到一個(gè)與之對(duì)應(yīng)的不變式，并且該不變式能夠蘊(yùn)含候選界函數(shù)。

綜上所述，利用Redlog 工具借助不變式驗(yàn)證候選界函數(shù)的算法如下：

本文在求解候選界函數(shù)時(shí)并不局限于函數(shù)的形式，超越函數(shù)、多項(xiàng)式函數(shù)均可，但是由于后期驗(yàn)證依賴于Redlog 工具，而由于Redlog 工具本身的局限性，導(dǎo)致它無法處理一些高次的多項(xiàng)式函數(shù)以及超越函數(shù)，因此對(duì)這類候選界函數(shù)Redlog 無法進(jìn)行驗(yàn)證，這也是本文循環(huán)程序界函數(shù)計(jì)算方法的局限所在。綜上所述，求解某給定循環(huán)其對(duì)應(yīng)的界函數(shù)的過程框架如圖1 所示。

圖1 界函數(shù)合成框架Fig.1 Framework of synthesizing loop bound function

其中在通過SVM 獲取候選超平面時(shí)，由于本文將界函數(shù)的計(jì)算問題轉(zhuǎn)化為線性二分類問題，因此在SVM 訓(xùn)練時(shí)均采用線性核函數(shù)。此外，并非所有的循環(huán)經(jīng)過一次訓(xùn)練就可以直接通過測(cè)試集，因此當(dāng)?shù)谝淮斡?xùn)練后的候選界函數(shù)并未通過測(cè)試集時(shí)，將測(cè)試集中未通過的點(diǎn)重新加入訓(xùn)練集進(jìn)行訓(xùn)練，然后自行設(shè)定訓(xùn)練次數(shù)，重復(fù)上述過程。整個(gè)實(shí)驗(yàn)流程如圖2 所示。

圖2 基于SVM的循環(huán)程序界函數(shù)計(jì)算流程Fig.2 Flowchart of calculating loop bound function for loop program via SVM

綜上所述，算法5 描述了對(duì)于給定循環(huán)程序，其界函數(shù)計(jì)算過程如下：首先設(shè)定界函數(shù)的模板從而得到映射關(guān)系，然后調(diào)用算法2 構(gòu)建訓(xùn)練集，得到訓(xùn)練集利用SVM 進(jìn)行訓(xùn)練得到分類超平面進(jìn)而得到候選的界函數(shù)，再對(duì)該候選界函數(shù)進(jìn)行優(yōu)化得到新的候選界函數(shù)，之后通過算法3 利用測(cè)試集對(duì)該候選界函數(shù)進(jìn)行初步驗(yàn)證，最后利用算法4 對(duì)通過測(cè)試集驗(yàn)證的候選界函數(shù)利用Redlog 工具進(jìn)行精確驗(yàn)證，如果驗(yàn)證通過，那么該候選界函數(shù)便是該循環(huán)程序的真正的界函數(shù)。

4 實(shí)驗(yàn)與結(jié)果分析

本文求解候選界函數(shù)是通過Python 利用Scikit-learn［28］包進(jìn)行實(shí)現(xiàn)，并且所有的實(shí)驗(yàn)均基于2.9 GHz Intel Core i5-9400f CPU 和8 GB 2 666 MHz DDR4 RAM 的PC 上進(jìn)行的。

4.1 實(shí)驗(yàn)結(jié)果

所有循環(huán)均取自于兩種方式：一是現(xiàn)有其他文獻(xiàn)工作中的循環(huán)；二是在現(xiàn)有文獻(xiàn)工作中的循環(huán)基礎(chǔ)上進(jìn)行了修改。表1 列出了本次實(shí)驗(yàn)所涉及的循環(huán)，其中循環(huán)1～2 來自于界函數(shù)相關(guān)文獻(xiàn)［21-22］中所提及的循環(huán)，循環(huán)3～6 來自于秩函數(shù)相關(guān)文獻(xiàn)［17］中的循環(huán)，循環(huán)7～9 則是對(duì)秩函數(shù)相關(guān)文獻(xiàn)中循環(huán)基礎(chǔ)上作出了修改，循環(huán)10 則是取自于文獻(xiàn)［12］。

表1 實(shí)驗(yàn)所涉及的循環(huán)Tab.1 Loops for experiments

從表2 可以看出：不同的循環(huán)有著各自不同的模板，并且不同的循環(huán)其所選取的負(fù)類點(diǎn)的值也各不相同。此外，還可以看出，針對(duì)從界函數(shù)文獻(xiàn)中提取的循環(huán)1～2，本文方法能夠獲得該循環(huán)所對(duì)應(yīng)的界函數(shù)；針對(duì)從秩函數(shù)文獻(xiàn)中獲得的循環(huán)3～6，本文方法能夠?qū)@些循環(huán)求解其對(duì)應(yīng)的界函數(shù)；針對(duì)循環(huán)7～9，當(dāng)前求解秩函數(shù)方法不能獲取其線性秩函數(shù)，只能夠求解其多階段線性秩函數(shù)，但是本文方法卻能夠獲得其全局的線性界函數(shù)；針對(duì)循環(huán)10，對(duì)比方法不能得到其線性秩函數(shù)以及多階段線性秩函數(shù)，本文方法也能獲得其對(duì)應(yīng)的界函數(shù)。

表2 實(shí)驗(yàn)參數(shù)以及所得模板系數(shù)Tab.2 Experimental parameters and template coefficients

4.2 實(shí)驗(yàn)對(duì)比

對(duì)于上述10 個(gè)循環(huán)將本文方法與當(dāng)前循環(huán)程序終止性驗(yàn)證的主流方法秩函數(shù)法作出對(duì)比以及與界函數(shù)相關(guān)方法作出比較。

4.2.1 與秩函數(shù)法的對(duì)比

秩函數(shù)是程序終止性驗(yàn)證的主流方法，因此首先選取了三種當(dāng)前合成秩函數(shù)的方法與本文方法在可行性以及合成秩函數(shù)或者界函數(shù)形式這兩個(gè)方面作出對(duì)比。表3 描述了針對(duì)表1 的循環(huán)程序，基于量詞消去秩函數(shù)合成、基于SVM秩函數(shù)合成以及多階段秩函數(shù)合成方法與本文方法的實(shí)驗(yàn)結(jié)果。

從表3 的實(shí)驗(yàn)結(jié)果可以看出：

表3 不同方法的可行性對(duì)比Tab.3 Feasibility comparison of different methods

1）基于QE 的方法由于其運(yùn)算復(fù)雜度高，因此一般用于處理線性循環(huán)，無法處理多階的循環(huán)程序，而本文方法可以處理多階的循環(huán)程序。

2）基于SVM 的秩函數(shù)合成方法其本身需要設(shè)定秩函數(shù)模板，再求解模板系數(shù)的值，因此對(duì)于一些存在多階段秩函數(shù)的循環(huán)程序便無法合成，而本文界函數(shù)方法可以合成全局的界函數(shù)。

3）基于線性規(guī)劃的多階段線性秩函數(shù)合成，它本身只能針對(duì)單路徑線性約束循環(huán)程序，對(duì)于一些二次或高次的循環(huán)程序便不能合成對(duì)應(yīng)的秩函數(shù)。

綜上所述，針對(duì)表1 所述的循環(huán)程序，在可行性上，本文方法能夠處理更多的循環(huán)。接下來將上述三種秩函數(shù)所能得到的秩函數(shù)形式與本文方法所能得到的界函數(shù)形式進(jìn)行對(duì)比，表4 羅列了針對(duì)表1 的循環(huán)，秩函數(shù)方法所能合成的秩函數(shù)形式以及本文方法所能得到的界函數(shù)形式。

表4 實(shí)驗(yàn)所得函數(shù)形式結(jié)果對(duì)比Tab.4 Comparison of experimental results in functional forms

從表4 可以看出，與三種秩函數(shù)的合成方法所求解得到的秩函數(shù)形式相比，本文方法求解得到的界函數(shù)在形式上更加簡(jiǎn)潔并且所得到的界函數(shù)均為全局界函數(shù)。

1）針對(duì)循環(huán)5～6，基于SVM 的方法雖然能夠得到秩函數(shù)，但是秩函數(shù)形式是非線性的，而本文方法卻能夠求解得到其所對(duì)應(yīng)的線性界函數(shù)，相較于非線性模板，線性模板在模板的選取上更加簡(jiǎn)潔直接。

2）針對(duì)循環(huán)7～9，此類循環(huán)沒有線性秩函數(shù)，僅僅存在多階段線性秩函數(shù)。本次實(shí)驗(yàn)多階段秩函數(shù)的求解過程采用了irankfinder 工具進(jìn)行實(shí)驗(yàn)，并將本文方法與文獻(xiàn)［12］中的求解多階段線性秩函數(shù)合成法進(jìn)行對(duì)比，從表4 結(jié)果可以看出，文獻(xiàn)［12］方法無法求解得到該循環(huán)所對(duì)應(yīng)的全局線性秩函數(shù)，僅僅能夠獲得多階段的線性秩函數(shù)，但是本文方法卻可以得到全局的線性界函數(shù)。

3）針對(duì)循環(huán)10，該循環(huán)利用秩函數(shù)求解方法，無法獲取其線性秩函數(shù)以及多階段線性秩函數(shù)，但是本文方法卻能夠求解其非線性的界函數(shù)。此外，實(shí)驗(yàn)中設(shè)置了簡(jiǎn)單的模板嘗試求解循環(huán)12 的2 次秩函數(shù)，但通過計(jì)算發(fā)現(xiàn)沒有相應(yīng)的秩函數(shù)（倘若設(shè)置復(fù)雜的2 次模板，則超出了工具的計(jì)算能力）。

綜上所述，針對(duì)表1 所述的循環(huán)程序，與當(dāng)前的三種秩函數(shù)的合成方法相比較，本文界函數(shù)方法不僅能夠處理更多的循環(huán)，并且還有著以下的特點(diǎn)：一是對(duì)某些循環(huán)，秩函數(shù)法僅能夠獲取非線性的秩函數(shù)，但是本文界函數(shù)法能夠獲取線性的界函數(shù)，相較于非線性結(jié)構(gòu)，線性結(jié)構(gòu)更為簡(jiǎn)潔；二是對(duì)某些循環(huán)，秩函數(shù)法僅僅能夠求解多階段的線性秩函數(shù)，但是本文界函數(shù)法能夠得到全局的界函數(shù)；三是對(duì)某些循環(huán)，秩函數(shù)方法無法求解得到其對(duì)應(yīng)的線性秩函數(shù)或者多階段線性秩函數(shù)，但是本文方法能夠獲得其非線性的界函數(shù)。

4.2.2 與界函數(shù)法的對(duì)比

相較于現(xiàn)有界函數(shù)求解方法，本文提出了一個(gè)新的界函數(shù)求解思路，即將界函數(shù)的求解問題轉(zhuǎn)化為線性的二分類問題，然后利用SVM 得到分類超平面進(jìn)而求解得到模板系數(shù)。因此本文方法求解候選界函數(shù)的過程并不局限于循環(huán)程序的形式，循環(huán)程序可以是多項(xiàng)式或者非多項(xiàng)式。此外，對(duì)于候選界函數(shù)的證明過程，本文給出了一個(gè)更加具有完備性的驗(yàn)證過程：

1）文獻(xiàn)［18-19，22］中的方法所針對(duì)的循環(huán)并非將初始值全部作為參數(shù)，而是給定具體的初始值或者給定部分初始值；本文方法所針對(duì)的循環(huán)程序是將初始值作為參數(shù)的循環(huán)。

2）文獻(xiàn)［21］方法在驗(yàn)證候選界函數(shù)時(shí)也需要獲取不變式，該方法首先將不變式的求解轉(zhuǎn)化為二次規(guī)劃優(yōu)化問題，再利用現(xiàn)有求解器獲取候選的不變式，最后驗(yàn)證該候選不變式是否為真正的不變式；而本文方法則是利用符號(hào)計(jì)算，在不變式參數(shù)全空間對(duì)滿足條件的不變式進(jìn)行查找，因此相較于文獻(xiàn)［21］方法，本文方法更加完備。例如：針對(duì)循環(huán)1，文獻(xiàn)［21］方法需要首先求解得到候選的不變式為a1+a2-≥c，然后再驗(yàn)證該不變式是否為真正的不變式，而與之不同的是本文方法采用符號(hào)計(jì)算在不變式參數(shù)全空間去尋找滿足條件的不變式，因此并不需要求解得到具體的不變式，僅需考慮其存在性。

5 結(jié)語

本文將界函數(shù)的求解問題轉(zhuǎn)化為線性二分類問題，提出了一個(gè)新的方法去尋找循環(huán)程序的界函數(shù)。首先，設(shè)定一個(gè)界函數(shù)模板，然后利用SVM 查找分類超平面獲取模板系數(shù)從而得到候選的界函數(shù)，最后通過現(xiàn)有符號(hào)驗(yàn)證工具Redlog結(jié)合不變式精確驗(yàn)證其是否是一個(gè)正確的界函數(shù)。從實(shí)驗(yàn)結(jié)果可以看出，相較于當(dāng)前的秩函數(shù)相關(guān)方法，針對(duì)循環(huán)5～6，秩函數(shù)方法只能夠找到其非線性的秩函數(shù)，但本文方法能夠得到其對(duì)應(yīng)的線性界函數(shù)；針對(duì)循環(huán)7～9，該循環(huán)沒有對(duì)應(yīng)的線性秩函數(shù)，只有多階段線性秩函數(shù)，但是本文方法能夠得到其對(duì)應(yīng)的全局線性界函數(shù)；針對(duì)循環(huán)10，當(dāng)前秩函數(shù)方法不能得到其對(duì)應(yīng)的線性秩函數(shù)以及多階段線性秩函數(shù)，而本文方法能夠得到其對(duì)應(yīng)2 次界函數(shù)。但是，后期的驗(yàn)證過程仍然依賴于Redlog 工具，因此對(duì)于一些循環(huán)利用本文方法即使能夠獲得其候選的界函數(shù)，但是由于Redlog 工具計(jì)算能力的局限性，不能對(duì)其進(jìn)行驗(yàn)證。此外，如何更加有效率地選取界函數(shù)模板以及訓(xùn)練集中的負(fù)類點(diǎn)也是在未來工作中需要進(jìn)一步深入研究的問題。