袁月 李軼

摘 要：秩函數(shù)探測(cè)是循環(huán)程序終止性分析的重要方法，目前，已有很多研究者致力于為線性循環(huán)程序探測(cè)對(duì)應(yīng)的線性秩函數(shù)，然而，針對(duì)具有多項(xiàng)式循環(huán)條件和多項(xiàng)式賦值的多項(xiàng)式型的循環(huán)，現(xiàn)有的秩函數(shù)探測(cè)方法還有所不足，解決方案大多是不完備的、或者具有較高的時(shí)間復(fù)雜度。針對(duì)現(xiàn)有工作對(duì)于多項(xiàng)式秩函數(shù)探測(cè)方法不足的問題，基于擴(kuò)展Dixon結(jié)式（KSY方法）和逐次差分代換（SDS）方法，提出一種為多項(xiàng)式循環(huán)程序探測(cè)多項(xiàng)式型秩函數(shù)的方法。首先，將待探測(cè)的秩函數(shù)模板看作帶參數(shù)系數(shù)的多項(xiàng)式，將秩函數(shù)的探測(cè)轉(zhuǎn)換為尋找滿足條件的參數(shù)系數(shù)的問題;然后，進(jìn)一步將問題轉(zhuǎn)換為判定相應(yīng)的方程組是否有解的問題，至此，利用KSY方法中的擴(kuò)展的Dixon結(jié)式，將問題更進(jìn)一步簡(jiǎn)化為帶參系數(shù)多項(xiàng)式（即結(jié)式）嚴(yán)格為正的判定問題;最后，利用SDS方法，找到一個(gè)充分條件，使得得到的結(jié)式嚴(yán)格為正，此時(shí)，可以獲取滿足條件的參數(shù)系數(shù)的取值，從而找到一個(gè)滿足條件的秩函數(shù)，通過實(shí)驗(yàn)驗(yàn)證該秩函數(shù)探測(cè)方法的有效性。實(shí)驗(yàn)結(jié)果表明，利用該方法，可以有效地為多項(xiàng)式循環(huán)程序找到多項(xiàng)式秩函數(shù)，包括深度為d的多階段多項(xiàng)式秩函數(shù)，與已有方法相比，該方法能夠更高效地找到多項(xiàng)式秩函數(shù)，對(duì)于基于柱形代數(shù)分解（CAD）方法的探測(cè)方法因時(shí)間復(fù)雜度問題無法而應(yīng)對(duì)的一些循環(huán)，利用所提方法能夠在幾秒內(nèi)為這些循環(huán)找到秩函數(shù)。

關(guān)鍵詞：循環(huán)程序終止性;多項(xiàng)式循環(huán)程序;多項(xiàng)式秩函數(shù);多階段秩函數(shù);Dixon結(jié)式;逐次差分代換

Abstract： Ranking function detection is one of the most important methods to analyze the termination of loop program. Some tools have been developed to detect linear ranking functions corresponding to linear loop programs. However， for polynomial loops with polynomial loop conditions and polynomial assignments， existing methods for detecting their ranking functions are mostly incomplete or with high time complexity. To deal with these weaknesses of existing work， a method was proposed for detecting polynomial ranking functions for polynomial loop programs， which was based on extended Dixon resultants （the KSY （Kapur-Saxena-Yang） method） and Successive Difference Substitution （SDS） method. Firstly， the ranking functions to be detected were seen as polynomials with parametric coefficients. Then the detection of ranking functions was transformed to the problem of finding parametric coefficients satisfying the conditions. Secondly， this problem was further transformed to the problem of determining whether the corresponding equations have solutions or not. Based on extended Dixon resultants in KSY method， the problem was reduced to the decision problem whether the polynomials with symbolic coefficients （resultants） were strictly positive or not. Thirdly， a sufficient condition making the resultants obtained strictly positive were? found by SDS method. In this way， the coefficients satisfying the conditions were able to be obtained and thus a ranking function satisfying the conditions was found. The effectiveness of the method was proved by experiments. The experimental results show that polynomial ranking functions including d-depth multi-stage polynomial ranking functions are able to be detected for polynomial loop programs. This method is more efficient to find polynomial ranking functions compared with the existing methods. For loops whose ranking functions cannot be detected by the method based on Cylindrical Algebraic Decomposition （CAD） due to high time complexity， their ranking functions are able be found within a few seconds with the proposed method.

Key words： termination of loop program; polynomial loop program; polynomial ranking function; multi-stage ranking function; Dixon resultant; Successive Difference Substitution （SDS）

0 引言

循環(huán)程序的終止性分析是程序驗(yàn)證中一個(gè)重要且具有挑戰(zhàn)性的研究領(lǐng)域。對(duì)于大多數(shù)軟件來說，保證循環(huán)程序是可終止的是十分重要的。目前，已有很多出色的研究工作[1-4]基于各種計(jì)算模型來自動(dòng)地進(jìn)行程序的終止性分析。秩函數(shù)法是證明循環(huán)程序終止性證明的主要方法，秩函數(shù)的存在是循環(huán)程序終止的一個(gè)充分條件。秩函數(shù)的探測(cè)在程序的正確性證明方面起著核心的作用，并且也被認(rèn)為是證明中最具挑戰(zhàn)性的一部分之一[5]。

秩函數(shù)將該循環(huán)的每個(gè)狀態(tài)映射為一個(gè)有界遞減集合中的元素，使得每當(dāng)循環(huán)完成一次迭代時(shí)，對(duì)應(yīng)的集合中的值減小。若能為一個(gè)給定的循環(huán)找到一個(gè)這種對(duì)應(yīng)的秩函數(shù)，則意味著該循環(huán)是可終止的。近來，秩函數(shù)的探測(cè)已成為一個(gè)熱門的研究方向。已有很多研究者致力于為線性循環(huán)程序探測(cè)線性秩函數(shù)，例如Colon等在2002年前后的一些早期工作[6-7]。在2004年，Podelski等[8]首次提出了一種完備有效地解決方案，基于Farkas引理[9]，為有理數(shù)域上的單分支線性循環(huán)探測(cè)線性秩函數(shù)。Ben-Amram等[10]最終在2014年，解決了針對(duì)整數(shù)域上的單分支線性循環(huán)程序的完備的線性秩函數(shù)探測(cè)方案的時(shí)間復(fù)雜度的問題。至此，從某種意義上說，如果對(duì)于一個(gè)單分支線性循環(huán)程序，存在一個(gè)對(duì)應(yīng)的線性秩函數(shù)，則一定能找到該秩函數(shù)。然而，對(duì)于一個(gè)（線性）循環(huán)程序，可能存在對(duì)應(yīng)的秩函數(shù)，卻不存在線性秩函數(shù)，并且，一般的循環(huán)程序終止性是不可判定的[11]，即使對(duì)于線性循環(huán)程序也是如此[12]。一些研究者[11，13]探測(cè)了終止性可判定的一些線性循環(huán)程序子類。Yang等[14]旨在尋找一些線性循環(huán)程序子類可終止的充分條件，使用計(jì)算機(jī)代數(shù)工具DISCOVERER來進(jìn)行輔助計(jì)算。此外，為了應(yīng)對(duì)更多的循環(huán)程序，最近一些研究者[10，15-20]構(gòu)造多個(gè)線性秩函數(shù)的組合（作為多階段秩函數(shù)）來應(yīng)對(duì)更加復(fù)雜的線性循環(huán)程序。

然而，具有線性秩函數(shù)的線性循環(huán)程序只是循環(huán)程序中的一小部分，為了捕捉更多的循環(huán)行為，一個(gè)研究方向是為具有多項(xiàng)式循環(huán)條件和多項(xiàng)式賦值語句的多項(xiàng)式型循環(huán)程序?qū)ふ叶囗?xiàng)式型的秩函數(shù)。Cousot[21]提出了一種針對(duì)半代數(shù)循環(huán)程序的多項(xiàng)式秩函數(shù)探測(cè)方法，他的方法基于的是拉格朗日松弛定理和半正定規(guī)劃（Semi-Definite Programming， SDP），但由于采用浮點(diǎn)計(jì)算，其得到秩函數(shù)并不一定是真正的秩函數(shù)，同時(shí)，拉格朗日乘子的引入也導(dǎo)致了該方法是不完備的;而Shen等[22]則在此方法的基礎(chǔ)上，利用有理恢復(fù)技術(shù)試圖找到更加精確的候選秩函數(shù)。Chen等[5]則是將探測(cè)多項(xiàng)式秩函數(shù)的問題轉(zhuǎn)化為了判斷半代數(shù)系統(tǒng)是否有解的問題，并基于Collins早年提出的量詞消去技術(shù)——柱形代數(shù)分解（Cylindrical Algebraic Decomposition， CAD），提出了一種完備的多項(xiàng)式秩函數(shù)探測(cè)方案，但由于CAD算法在糟糕情形下的復(fù)雜度是雙指數(shù)的，故限制了他們的方法只適用于較小規(guī)模的系統(tǒng)。

為了解決時(shí)間復(fù)雜度以及精確性的問題，本文提出一種為多項(xiàng)式循環(huán)程序探測(cè)多項(xiàng)式秩函數(shù)的方法，利用楊路等的研究成果，即擴(kuò)展的Dixon結(jié)式（KSY（Kapur-Saxena-Yang）方法[23]）和逐次差分代換（Successive Difference Substitution， SDS）方法[24]，來進(jìn)行秩函數(shù)的探測(cè)。具體而言，本文將循環(huán)程序的終止性證明的問題轉(zhuǎn)換為不等式的證明問題，首先，將帶探測(cè)的秩函數(shù)模板看作帶參數(shù)系數(shù)的多項(xiàng)式，將秩函數(shù)的探測(cè)轉(zhuǎn)換為尋找滿足條件的參數(shù)系數(shù)的問題，此時(shí)，秩函數(shù)應(yīng)當(dāng)滿足的條件被轉(zhuǎn)化為一系列帶參系數(shù)多項(xiàng)式不等式之間應(yīng)當(dāng)滿足一定的蘊(yùn)含關(guān)系;然后，將蘊(yùn)含關(guān)系的判定問題轉(zhuǎn)換為判定相應(yīng)的方程組是否有解的問題，至此，利用KSY方法中的擴(kuò)展的Dixon結(jié)式，將問題進(jìn)一步簡(jiǎn)化為帶參系數(shù)多項(xiàng)式（即結(jié)式）嚴(yán)格為正的判定問題;最后，利用逐次差分代換（SDS）方法，找到一個(gè)充分條件，使得得到的結(jié)式嚴(yán)格為正。通過這種方式，可以獲取滿足條件的參數(shù)系數(shù)的取值，從而找到一個(gè)滿足條件的秩函數(shù)。

實(shí)驗(yàn)結(jié)果表明，利用本文提出的方法可以有效地為多項(xiàng)式循環(huán)程序找到多項(xiàng)式秩函數(shù)，與現(xiàn)有基于CAD技術(shù)的完備的探測(cè)方案相比更加高效。此外，利用該方法，還能為多項(xiàng)式循環(huán)程序探測(cè)深度為d的多階段秩函數(shù)，更具體而言，即嵌套秩函數(shù)（2017年由Ben-Amram等[16]提出的多階段秩函數(shù)的一個(gè)更加普適性的定義）。與基于SDP方法的多項(xiàng)式秩函數(shù)探測(cè)方案不同的是，該方法可以找到精確的秩函數(shù)，不需要對(duì)找到的秩函數(shù)進(jìn)行再一次的驗(yàn)證。

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

本章將介紹與KSY方法和SDS方法相關(guān)的背景知識(shí)。

1.1 Dixon結(jié)式和KSY方法

給定由k+1個(gè)含k個(gè)變?cè)亩囗?xiàng)式方程組S：

該多項(xiàng)式δ則被稱為Dixon多項(xiàng)式。將δ看作關(guān)于α的多項(xiàng)式，令s′為系數(shù)個(gè)數(shù)、關(guān)于x的多項(xiàng)式oi（x）為每個(gè)系數(shù)，進(jìn)一步得到以下方程組：

顯然，無論α取值如何，S的任意一個(gè)解xi都是δ的一個(gè)零點(diǎn)，因此，xi也是多項(xiàng)式oi（x）的所有系數(shù)的零點(diǎn)，也就是說xi是方程組S′的一個(gè)解。進(jìn)一步，S′可以寫成如下形式：

其中vi（i=1，2，…，s）是δ中關(guān)于變?cè)獂1，x2，…，xk的所有冪積，D是系數(shù)矩陣。D則被稱為Dixon矩陣，而D的行列式則被稱為Dixon結(jié)式。當(dāng)s′=s時(shí)，Dixon結(jié)式有零點(diǎn)是原方程組S有解的一個(gè)必要條件[25]。

然而，Dixon矩陣常常可能是奇異的，即其行列式總等于0，或者s′≠s無法計(jì)算Dixon結(jié)式，此時(shí)，不能提供與原方程組有解相關(guān)的有用信息，因此，為了解決這個(gè)問題，Yang等[23]提出了KSY方法，來計(jì)算擴(kuò)展的Dixon結(jié)式。

令F={p1（x），p2（x），…，pk+1（x）}，給定對(duì)x的約束C，有如下形式x≠0。設(shè)Dixon矩陣的第i列為ui，它所對(duì)應(yīng)的單項(xiàng)式為monom（ui），令nvcol（C）為所有的滿足C monom（ui）≠0的列，而D1為所有通過刪除Dixon矩陣中屬于nvcol（C）的一列而得到s′×（s-1）的子矩陣集合。設(shè)a1，a2，…，am為m個(gè)參數(shù)，Q為有理數(shù)域的代數(shù)閉域，Φ：{a1，a2，…，am} → Q為一個(gè)映射，也就是把參數(shù)的值代入，獲取Q上的一個(gè)值，令Φ（F），Φ（D）和Φ（D1）為把參數(shù)值分別代入到F、D和D1而得到的結(jié)果，再令R={Y|Y是D的一個(gè)r×r的非奇異子矩陣}。

定理1 如果X∈D1.rank（X）此處的X，是矢量、向量或矩陣嗎？另外，rank前面（D1后面）的符號(hào)，是點(diǎn)還是逗號(hào)，請(qǐng)明確?；貜?fù)：rank前面（D1后面）的符號(hào)，是點(diǎn)，也就是s.t.;

根據(jù)定理1，可以得到如下的算法：先檢查是否有X∈D1.rank（X）

1.2 SDS方法

差分代換（Difference Substitution， DS）方法常被用于對(duì)稱形式的不等式的證明中，Yang[24]定義了一個(gè)更加一般的DS的概念，用于證明對(duì)稱以及非對(duì)稱形式的不等式，并且提出逐次差分替換法（即SDS方法），此后，很多研究者[26-29]對(duì)該方法進(jìn)行了進(jìn)一步的擴(kuò)展研究。利用SDS方法，可以證明多元多項(xiàng)式在正實(shí)數(shù)域上是半正定的。

一般地，給定一個(gè)n元多項(xiàng)式P，其變量x1，x2，…，xn有n！種排序結(jié)果，對(duì)諸如x1≥x2≥…≥xn的每個(gè)排序，對(duì)應(yīng)著一個(gè)替代變換：

其中，ti≥0。通過代換之后，P可以轉(zhuǎn)化為一個(gè)關(guān)于t1，t2，…，tn的多項(xiàng)式，而所有n！個(gè)代換得到的多項(xiàng)式組成的集合稱為DS。進(jìn)一步，如果該集合中的每個(gè)元素的所有系數(shù)均為非負(fù)的，則無論x1，x2，…，xn取何種非負(fù)值都有P≥0，也就是說P在正實(shí)數(shù)域上是半正定的，而如果該集合中存在一個(gè)元素有系數(shù)為負(fù)，則繼續(xù)對(duì)該多項(xiàng)式的DS用同樣的方式進(jìn)行檢查。以上這個(gè)過程被稱為逐次差分代換法（SDS方法）。

更進(jìn)一步，利用SDS方法，可以得到多項(xiàng)式P嚴(yán)格為正的一個(gè)充分條件，即如果DS中的每個(gè)元素的所有系數(shù)非負(fù)且常數(shù)項(xiàng)嚴(yán)格為正，則P在正實(shí)數(shù)域上是嚴(yán)格正定的。

2 不等式蘊(yùn)含關(guān)系的證明問題及其解決方法

本章將解決的是帶參數(shù)系數(shù)的多元多項(xiàng)式不等式蘊(yùn)含關(guān)系的證明問題，該問題定義如下。

定義1 P1。設(shè)p（x）為一個(gè)帶參數(shù)系數(shù)η1，η2，…，ηm的多項(xiàng)式，其中，x=（x1，x2，…，xn）T為一個(gè)含n元變量的向量。P1問題為：找到一組η1，η2，…，ηm的實(shí)數(shù)賦值，使得對(duì)任意的x∈Rn有：

證明 當(dāng)k=n時(shí)，SY為一個(gè)關(guān)于n個(gè)變?cè)獂的由n+1個(gè)多項(xiàng)式等式組成的方程組，又有如果H（η，ξ）≠0則SY無解，進(jìn)一步，也就是說SY無解，更進(jìn)一步，也就意味著P1問題中的關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。證畢。

注1 本文將多項(xiàng)式H（η，ξ）稱為式（1）在k=n的情況下的擴(kuò)展Dixon結(jié)式。在這種情況下，為解決P1問題，只需找到一個(gè)η使得H（η，ξ）在ξ∈Rk+1+上嚴(yán)格正定即可。考慮1.2節(jié)中介紹的SDS方法，其中，需要確保DS中每一個(gè)替換后的多項(xiàng)式的系數(shù)非負(fù)，而對(duì)于H（η，ξ）而言，如果每個(gè)替換后的多項(xiàng)式的所有系數(shù)非負(fù)且常數(shù)項(xiàng)嚴(yán)格為正，那么則可確保H（η，ξ）在ξ∈Rk+1+上嚴(yán)格正定，也就是說，此時(shí)可以找到一組P1問題中所要尋找的η1，η2，…，ηm的賦值。

引理2 k

那么，關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。

證明 有如果H（η，，ξ）≠0則SY無解，進(jìn)一步，也就是說SY無解，更進(jìn)一步，也就意味著P1問題中的關(guān)于變量x∈Rn蘊(yùn)含式（1）成立。證畢。

至此，只需找到一個(gè)η使得HS中的每個(gè)多項(xiàng)式Hi在β∈Rn+1+上嚴(yán)格正定即可。利用與注1類似的方法，可以找到一個(gè)η使得HS中的每個(gè)多項(xiàng)式Hi在β∈Rn+1+上嚴(yán)格正定，進(jìn)一步，也就是說，此時(shí)，H（η，，ξ）在ξ∈Rk+1+，∈Rn-k上嚴(yán)格正定，更進(jìn)一步，至此可以找到一組P1問題中所要尋找的η1，η2，…，ηm的賦值。

3 多項(xiàng)式秩函數(shù)探測(cè)問題

本章將介紹如何利用第2章的結(jié)果來為單路徑多項(xiàng)式循環(huán)程序探測(cè)多項(xiàng)式秩函數(shù)。首先，將給出所針對(duì)的循環(huán)程序的定義;然后，將介紹為一類循環(huán)程序探測(cè)秩函數(shù)（即深度為1的嵌套秩函數(shù)）的方法;最后將介紹為更加一般的循環(huán)程序探測(cè)深度為d的嵌套秩函數(shù)的方法。

引理3 給定一個(gè)形如式（5）的循環(huán)程序P，P在實(shí)數(shù)域上不可終止的充分必要條件是其所對(duì)應(yīng)的形如式（6）的循環(huán)程序P在實(shí)數(shù)域上不可終止。

證明 分為以下兩種情況考慮。

1）k≤b。在這種情況下，有n=b，也就是說P即為P，此時(shí)，顯然，P不可終止的充要條件為P不可終止。

2）k>b。在這種情況下，有n=k>b。

本節(jié)將針對(duì)形如式（6）的循環(huán)P的一種簡(jiǎn)單的情況，即k=n的情況，為這類循環(huán)探測(cè)秩函數(shù)。r（x）為一個(gè)Rq → R的函數(shù)，r（x）被稱為P的秩函數(shù)，如果以下條件被滿足：

設(shè)r（x）為一個(gè)關(guān)于x的多項(xiàng)式，顯然，（x）=r（x）-r（M（x））-1也為一個(gè)關(guān)于x的多項(xiàng)式，令η=（η1，η2，…，ηq+1）T∈Rq+1為r（x）的參數(shù)系數(shù)組成的向量，η′為（x）的參數(shù)系數(shù)向量，顯然有η′=Bη，其中B是一個(gè)確定的矩陣，由循環(huán)中的賦值M和r（x）確定。

其中，η′=Bη，H1和H2分別是蘊(yùn)含式（7）和（8）的擴(kuò)展Dixon結(jié)式，則P有對(duì)應(yīng)的秩函數(shù)。

證明 已知在蘊(yùn)含式（7）和（8）中，G（x）≥0是由k個(gè)多項(xiàng)式不等式組成的合取式，并且x為一個(gè)含k個(gè)變量的向量，因此，根據(jù)引理1，如果存在η使得：對(duì)任意的ξ1∈Rk+1+有H1（η，ξ1）≠0并且對(duì)任意的ξ2∈Rk+1+有H2（η′，ξ2）≠0，那么式（7）對(duì)任意的x∈Rk恒成立并且對(duì)式（8）對(duì)任意的x∈Rk恒成立，此時(shí)，根據(jù)秩函數(shù)的有界和遞減的條件可知，P有對(duì)應(yīng)的秩函數(shù)r（x），該秩函數(shù)的系數(shù)由η確定。證畢。

至此，再利用類似于注1中的方法，即基于SDS方法，可以找到一個(gè)η，使得H1（η，ξ1）和H2（Bη，ξ2）對(duì)任意的ξ1∈Rk+1+和任意的ξ2∈Rk+1+均嚴(yán)格為正，此時(shí)即可找到滿足條件的秩函數(shù)。

3.3 深度為d的嵌套秩函數(shù)

多階段秩函數(shù)的概念可以進(jìn)一步擴(kuò)展為一個(gè)更一般的概念（可以應(yīng)對(duì)更多的循環(huán)程序），即嵌套秩函數(shù)[16]。接下來，將介紹為形如式（6）的循環(huán)探測(cè)深度為d的嵌套秩函數(shù)的方法。

顯然，在3.2節(jié)中定義的秩函數(shù)為一個(gè)深度為1的嵌套秩函數(shù)。

4 算法和實(shí)驗(yàn)

深度為d的嵌套秩函數(shù)的探測(cè)算法如下算法1和算法2所示。在算法1中，SY指的是第3章中的式（2），Hi指的是定理3中的擴(kuò)展的Dixon結(jié)式。

算法1 DETC。帶參數(shù)系數(shù)的多元多項(xiàng)式不等式蘊(yùn)含關(guān)系的探測(cè)。

輸入：含d個(gè)關(guān)于n元變量的多項(xiàng)式的蘊(yùn)含式的合取式I（在每個(gè)蘊(yùn)含式中，前件為已知的k個(gè)多項(xiàng)式的合取式，后件為一個(gè)帶參系數(shù)的多項(xiàng)式）。

輸出：返回滿足條件的參數(shù)系數(shù)的一組賦值。

過程：

1）為每個(gè)蘊(yùn)含式中加入（k+1）個(gè)松弛變量，將I轉(zhuǎn)化為形如SY的d個(gè)多項(xiàng)式方程組。

2）獲取每個(gè)方程組的擴(kuò)展Dixon結(jié)式Hi（i=1，2，…，d）。

3）如果存在一組參系數(shù)賦值使得H1，H2，…，Hd均嚴(yán)格為正，則返回該賦值;否則，返回空。

算法2 探測(cè)深度為d的嵌套秩函數(shù)。

輸入：循環(huán)程序P（含n個(gè)變量，循環(huán)條件中有k個(gè)不等式，且k不大于n），秩函數(shù)模板r。

輸出：如果存在深度為d的嵌套秩函數(shù)則返回True。

過程：

1）根據(jù)秩函數(shù)需滿足的條件，將P和r轉(zhuǎn)化為含d+1個(gè)蘊(yùn)含式的合取式I;

討論 兩個(gè)算法的時(shí)間復(fù)雜度主要集中在算法1中的擴(kuò)展Dixon結(jié)式的計(jì)算以及SDS方法的計(jì)算。首先是關(guān)于Dixon結(jié)式計(jì)算的復(fù)雜度，其中主要包括構(gòu)造Dixon矩陣的復(fù)雜度（O（m21n！3∏ni=2m3i）[30]和計(jì)算Dixon結(jié)式的復(fù)雜度（即計(jì)算Dixon矩陣的行列式，O（n3n log n log log n））[31-32]。其次，關(guān)于SDS方法的計(jì)算復(fù)雜度，因?yàn)槠溥^程是一個(gè)不可終止的過程，所以只能在給定差分代換次數(shù)上界的前提下來討論其復(fù)雜度，給定一個(gè)n元多項(xiàng)式，對(duì)其進(jìn)行1次差分代換，將產(chǎn)生n！個(gè)多項(xiàng)式，若對(duì)其進(jìn)行m次差分代換，將產(chǎn)生（n?。﹎個(gè)多項(xiàng)式。這就需要對(duì)（n?。﹎個(gè)多項(xiàng)式進(jìn)行分別處理（即從每個(gè)多項(xiàng)式中抽取出所有系數(shù)構(gòu)成線性不等式系統(tǒng)，然后用線性規(guī)劃工具進(jìn)行求解，這個(gè)求解過程是多項(xiàng)式時(shí)間復(fù)雜度的），所以，復(fù)雜度較高。盡管如此，實(shí)驗(yàn)表明，對(duì)某些程序?qū)嵗?，與現(xiàn)有工具（如基于CAD的秩函數(shù)探測(cè)方法[5]）比較，本文方法能有效計(jì)算它們的秩函數(shù)。

實(shí)驗(yàn)環(huán)境為：一臺(tái)處理器為Intel Core i5-6300HQ 2.3GHz、內(nèi)存為16GB、操作系統(tǒng)為64位的Windows操作系統(tǒng)的計(jì)算機(jī)，利用的是Maple 18軟件。實(shí)驗(yàn)中將本文所提出的秩函數(shù)探測(cè)方法與基于CAD的秩函數(shù)探測(cè)方法[5]（利用Maple中的量消去工具RegularChains）進(jìn)行了比較，表1是實(shí)驗(yàn)結(jié)果，其中循環(huán)程序10～13來自文獻(xiàn)[16，20]。實(shí)驗(yàn)結(jié)果表明，利用本文提出的方法能夠更加高效地探測(cè)到秩函數(shù)（僅需用幾秒鐘的時(shí)間）。特別地，對(duì)于表1中的循環(huán)程序11，利用本文的方法也無法計(jì)算其秩函數(shù)，這是因?yàn)楸疚姆椒ㄕ业降氖侵群瘮?shù)存在的一個(gè)充分條件，而不是充要條件。下面將給出一些例子來具體說明秩函數(shù)探測(cè)的過程。

5 結(jié)語

本文基于楊路等的研究成果，即KSY方法和SDS方法，提出了一種為多項(xiàng)式循環(huán)程序探測(cè)多項(xiàng)式秩函數(shù)的方法，給定秩函數(shù)模板，尋找滿足條件的秩函數(shù)模板中的參數(shù)，從而確定滿足條件的秩函數(shù)。實(shí)驗(yàn)結(jié)果表明，對(duì)于一些多項(xiàng)式循環(huán)程序，可以有效地為其找到多項(xiàng)式秩函數(shù)（即深度為1的多階段秩函數(shù)）和深度為d的多階段秩函數(shù)。此外，與現(xiàn)有的基于SDP方法的解決方案不同，利用本文提出的方法，可以發(fā)現(xiàn)精確的秩函數(shù)，無需進(jìn)行再次驗(yàn)證。本文方法能在較短時(shí)間內(nèi)為多項(xiàng)式循環(huán)找到對(duì)應(yīng)的多項(xiàng)式秩函數(shù)。在后續(xù)的工作中，本研究將針對(duì)多項(xiàng)式秩函數(shù)的探測(cè)問題進(jìn)行進(jìn)一步探索，以應(yīng)對(duì)更多的多項(xiàng)式循環(huán)程序。

參考文獻(xiàn) （References）

[1] LEIKE J， HEIZMANN M. Geometric nontermination arguments [C]// TACAS 2018： Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2018： 172-186.

[2] FEDYUKOVICH G， ZHANG Y L， GUPTA A. Syntax-guided termination analysis[C]// CAV 2018： Proceedings of the 2018 International Conference on Computer Aided Verification. Berlin： Springer， 2018： 124-143.

[3] CHEN Y F， HEIZMANN M， LENGAL O， et al. Advanced automata-based algorithms for program termination checking[C]// PLDI 2018： Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation. New York： ACM， 2018： 135-150.

[4] LI Y. Witness to non-termination of linear programs[J]. Theoretical Computer Science， 2017， 681： 75-100.

[5] CHEN Y H， XIA B C， YANG L， et al. Discovering non-linear ranking functions by solving semi-algebraic systems[C]// ICTAC 2007： Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing. Berlin： Springer， 2007： 34-49.

[6] COLON M， SPIMA H. Synthesis of linear ranking functions[C]// TACAS 2001： Proceedings of the 2001 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2001： 67-81.

[7] COLON M， SPIMA H. Practical methods for proving program termination[C]// CAV 2002： Proceedings of the 2002 International Conference on Computer Aided Verification. Berlin： Springer， 2002： 442-454.

[8] PODELSKI A， RYBALCHENKO A. A complete method for the synthesis of linear ranking functions[C]// VMCAI 2004： Proceedings of the 2004 International Conference on Verification， Model Checking and Abstract Interpretation. Berlin： Springer， 2004： 239-251.

[9] SCHRIJVER A. Theory of Linear and Integer Programming [M]. New York： John Wiley and Sons， Inc.， 1986： 87-90.

[10] BEN-AMRAM A M， GENAIM S. Ranking functions for linear-constraint loops[J]. Journal of the ACM， 2014， 61（4）： Article No. 26.

[11] TURING A M. On computable numbers， with an application to the entscheidungs problem[J]. Proceedings of the London Mathematical Society， 1937， 42（2）： 230-265.

[12] BRAVEMAN M. Termination of integer linear programs[C]// CAV 2006： Proceedings of the 2006 International Conference on Computer Aided Verification. Berlin： Springer， 2006： 372-385.

[13] TIWARI A. Termination of linear programs[C]// CAV 2004： Proceedings of the 2004 International Conference on Computer Aided Verification. Berlin： Springer， 2004： 70-82.

[14] YANG L， ZHAN N J， XIA B C， et al. Program verification by using DISCOVERER[C]// VSTTE 2005： Proceedings of the 2005 Working Conference on Verified Software： Theories， Tools， and Experiments. Berlin： Springer， 2008： 528-538.

[15] BAGNARA R， MESNARD F. Eventual linear ranking functions[C]// PPDP 2013： Proceedings of the 2013 International Symposium on Principles and Practice of Declarative Programming. New York： ACM， 2013： 229-238.

[16] BEN-AMRAM A M， GENAIM S. On multiphase-linear ranking functions[C]// CAV 2017： Proceedings of the 2017 International Conference on Computer Aided Verification. Berlin： Springer， 2017： 601-620.

[17] BRADLEY A R， MANNA Z， SIPMA H B. Linear ranking with reachability[C]// CAV 2005： Proceedings of the 2005 International Conference on Computer Aided Verification. Berlin： Springer， 2005： 491-504.

[18] BRADLEY A R， MANNA Z， SIPMA H B. The polyranking principle[C]// ICALP 2005： Proceedings of the 2005 International Conference on Automata， Languages and Programming. Berlin： Springer， 2005： 1349-1361.

[19] LEIKE J， HEIZMANN M. Ranking templates for linear loops[C]// TACAS 2014： Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin： Springer， 2014： 172-186.

[20] LI Y， ZHU G， FENG Y. The L-depth eventual linear ranking functions for single-path linear constraint loops[C]// TASE 2016： Proceedings of the 2016 International Symposium on Theoretical Aspects of Software Engineering. Piscataway， NJ： IEEE， 2016： 30-37.

[21] COUSOT P. Proving program invariance and termination by parametric abstraction， Lagrangian relaxation and semidefinite programming[C]// VMCAI 2005： Proceedings of the 2005 International Conference on Verification， Model Checking and Abstract Interpretation. Berlin： Springer， 2005： 1-24.

[22] SHEN L Y， WU M， YANG Z F， et al. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method[J]. Journal of Systems Science and Complexity， 2013， 26（2）： 291-301.

[23] KAPUR D， SAXENA T， YANG L. Algebraic and geometric reasoning using Dixon resultants[C]// ISSAC 1994： Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation. New York： ACM， 1994： 99-107.

[24] YANG L. Solving harder problems with lesser mathematics[C]// ATCM 2005： Proceedings of the 2005 Asian Technology Conference in Mathematics. Radford， VA： Mathematics and Technology， 2005： 37-46.

[25] DIXON A L. The eliminant of three quantics in two independent variables[J]. Proceedings of the London Mathematical Society， 1909， s2-7（49）： 49-69.

[26] 楊路，姚勇.差分代換矩陣與多項(xiàng)式的非負(fù)性判定[J].系統(tǒng)科學(xué)與數(shù)學(xué)，2009，29（9）：1169-1177.（YANG L， YAO Y. Difference substitution matrices and decision on nonnegativity of polynomials [J]. Journal of Systems Science and Mathematical Sciences， 2009， 29（9）：1169-1177.）

[27] HOU X R， SHAO J W. Bounds on the number of steps of WDS required for checking the positivity of integral forms[J]. Applied Mathematics and Computation， 2011， 217（24）： 9978-9984.

[28] 韓京俊.基于差分代換的正半定型判定完備方法[J].北京大學(xué)學(xué)報(bào)（自然科學(xué)版），2013，49（4）：545-551.（HAN J J. A complete method based on successive difference substitution method for deciding positive semi-definiteness of polynomials[J]. Acta Scientiarum Naturalium Universitatis Pekinensis， 2013， 49（4）： 545-551.）

[29] 楊路.差分代換與不等式機(jī)器證明[J].廣州大學(xué)學(xué)報(bào)（自然科學(xué)版），2006，5（2）：1-7.（YANG L. Difference substitution and automated inequality proving[J]. Journal of Guangzhou University （Natural Science edition）， 2006， 5（2）： 1-7.）

[30] QIN X， WU D， TANG L， et al. Complexity of constructing Dixon resultant matrix[J]. International Journal of Computer Mathematics， 2016， 94（10）： 1-16.

[31] LI Y. An effective hybrid algorithm for computing symbolic determinants[J]. Applied Mathematics and Computation， 2009， 215（7）： 2495-2501.

[32] KALTOFEN E. On computing determinants of matrices without divisions [C]// ISSAC 1992： Proceedings of the 1992 International Symposium on Symbolic and Algebraic Computation. New York： ACM， 1992： 342-349.