基于迭代轨迹划分的单分支循环程序终止性分析.pdf

秩函数作为循环程序终止性分析的重要方法已得到广泛研究.文中着重研究了单分支循环的终止性.首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环.其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的.而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性.最后,将三段式秩函数的计算问题归结为S VM分类问题,并利用工具Z 或b o t t e m a对由S VM所得的候选秩函数进行验证.关键词:程序验证;秩函数;机器学习;程序终止性中图法分类号T P T e r m i n a t i o nA n a l y s i so fS i n g l eP a t hL o o pP r o g r a m sB a s e do nI t e r a t i v eT r a j e c t o r yD i v i s i o nWANGY a o,a n dL IY iC h o n g q i n gK e yL a b o r a t o r yo fA u t o m a t e dR e a s o n i n ga n dC o g n i t i o n,C I G I T,C A S,C h o n g q i n g ,C h i n aC h o n g q i n gS c h o o l,U n i v e r s i t yo fC h i n e s eA c a d e m yo fS c i e n c e s,C h o n g q i n g ,C h i n aA b s t r a c t T h er a n k i n g f u n c t i o nh a sb e e ne x t e n s i v e l ys t u d i e da sa n i m p o r t a n tm e t h o do fp r o g r a mt e r m i n a t i o na n a l y s i s I nt h i sp a p e r,w e f o c u so nt h e t e r m i n a t i o no f s i n g l e p a t hl o o p s F i r s t l y,t h ec o n c e p to f t w o w a yi t e r a t i v e l o o p s i sp r o p o s e d,a n dt h es i n g l e p a t h l o o p s a r ed i v i d e d i n t ob i d i r e c t i o n a l i t e r a t i v e l o o p s a n dn o n b i d i r e c t i o n a l i t e r a t i v e l o o p s S e c o n d l y,f o r t h eb i d i r e c t i o n a l i t e r a t i v el o o pp r o g r a m,ad i v i s i o nm e t h o da n dc o n c e p to f t r i v i a l r a n k i n g f u n c t i o na r ep r o p o s e d,a n d i t i sp r o v e dt h a t i f ab i d i r e c t i o n a l i t e r a t i v e l o o pe x i s t sa t r i v i a l r a n kf u n c t i o n,i t i s t e r m i n a t e d A s f o r t h en o n b i d i r e c t i o n a l i t e r a t i v e l o o p,w eu s e i n c r e m e n t a l f u n c t i o na st h ed i v i s i o nm e t h o d,i e,t h e o r i g i n a l p r o g r a ms p a c e i sd i v i d e d i n t o s m a l l e r s p a c e sb yu s i n g i n c r e m e n t a l f u n c t i o n,a n d t h e t e r m i n a t i o no f t h eo r i g i n a l p r o g r a mi sp r o v e db yc o m p u t i n gt h e r a n k i n gf u n c t i o no nt h es m a l l e r s p a c e F i n a l l y,t h ep r o b l e mo f c o m p u t i n gt h e t r i v i a l r a n k i n g f u n c t i o nc o m e sd o w n t o t h eS VMc l a s s i f i c a t i o np r o b l e m,a n dw ev e r i f i e s c a n d i d a t e r a n k i n g f u n c t i o n su s i n g t h et o o l sZ o rb o t t e m a K e y w o r d s P r o g r a mv e r i f i c a t i o n,R a n k i n gf u n c t i o n s,M a c h i n e l e a r n i n g,P r o g r a mt e r m i n a t i o n引言随着计算机相关技术的发展,人类目前正处于大数据和人工智能的时代,相关软件对社会的影响也越来越深入,计算机已经成为人们生活中必不可缺的东西.在人们越来越依赖计算机软件的同时,需要对软件内部程序的稳定性与正确性加以关注.众所周知,计算机程序是整个计算机服务体系的核心,因此,为了避免程序故障导致的重大事故,有必要研究程序运行的正确性与可靠性,保证程序的稳定运行.在程序理论的范畴中,程序的正确性指程序在一定的前提条件下,经过预先设定好的运算,生成符合某些性质的结果,同时要求程序最后必须终止.研究程序的终止性是保障程序正确性的必要条件.虽然循环程序的终止性问题已经被证明为不可判定问题,但是仍可以通过一定的算法判断循环程序的终止性.根据判断程序是否终止可以将其分成两类方法:通过寻找秩函数判断程序终止和通过寻找不动点或不变集来判断程序不终止.文献 的工作都是针对线性循环求解线性秩函数,其中P o d e l s k i等基于F a r k a s引理,根据循环条件和赋值语句构造约束关系来求解线性秩函数;B r a d l e y等首先提出了合成线性字典序秩函数的概念,基于这个概念,B e n Am r a m等提出了合成线性字典序秩函数的完备算法;自此,秩函数的形式被拓宽,B a g n a r a等提出了最终线性秩函数的概念,利 用划 分 思想 提 高 获 得 线 性 秩 函 数 的 可 能 性;L e i k e等 首次提出了多阶段秩函数和嵌套秩函数的定义;B e n Am r a m等 证明针对单分支线性约束程序,上述两个概念是等价的,并给出了合成嵌套秩函数的完备方法.文献 针对非线性秩函数,其中C o u s o t 使用参数抽象、拉格朗日松弛以及半正定规划进行约束求解,获得非线性秩函数;C h e n等 将多项式秩函数问题规约到半代数系统问题的求解中,并通过柱形代数分解的方法来获得非线性秩函数.但是这两种方法都存在一定的问题,C o u s o t的方法基于S D P进行求解,由于S D P内部采用浮点计算,因此最终得到的秩函数候补不是精确结果,且没有进行验证,C h e n等的方法基于传统柱形代数分解,在最糟糕的情况,时间复杂度甚至会达到双指数.近年来,机器学习方法被逐渐运用于程序验证领域,并且对以上方案进行了很好的改进.Y u a n等 将秩函数的两个满足条件转化为二分类问题,利用S VM算法寻找秩函数;S u n 基于机器学习算法,得到了多阶段秩函数的求解算法.但文献 的工作仅局限于全局秩函数,对拥有多阶段秩函数的循环不能很好地处理;而文献 的方法在进行多阶段秩函数的求解前,必须设定最大阶数,但是在理论上关于多阶段秩函数存在的阶数上界没有得到证明.本文主要考虑了单分支线性约束循环的终止性问题.B a g n a r a等在文献 中首次提出了增函数的概念,并利用增函数对原始程序空间进行划分得到更小的空间,进而在新的空间上计算秩函数.增函数划分为程序终止性分析提供了新的思路,即能否通过某种划分方法,将原始程序对应的程序空间划分为不同的m个子空间,然后通过证明m个子空间都有秩函数来证明原始程序是可终止的.受此启发,我们观察到一类被称为双向迭代循环的程序,其程序空间可以分为个子空间,并证明了如果这个子空间都存在秩函数,那么该程序是终止的.然后,通过S VM算法去探测这个子空间的秩函数.针对非双向迭代循环,我们引用了文献 中增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性.但与文献 利用f a r k a s引理计算秩函数的方法不同的是,本文将子空间上的秩函数计算归结为二分类问题,并利用S VM对其求解.不同于文献,本文方法可以处理非线性循环的秩函数计算问题,且对部分程序,本文方法可以得到形式更为简洁的秩函数.本文第章介绍程序终止性判断的相关概念;第章提出双向迭代循环以及三段式秩函数的定义,证明了若一个双向迭代循环存在三段式秩函数,则该双向循环程序终止,并给出了整个算法流程;第章展示本文方法与已有方法的实验对比;最后总结全文并展望未来.准备知识本章将主要介绍有关程序终止性判断的相关理论基础,这些内容将在后面的算法中起到重要作用.本文工作主要聚焦于以下形式的循环:w h i l ex,d ox F(x)xRn:P(x),Pk(x)其中,表示该循环的程序空间,并且是一个单连通集,Pi(x)是系数为实数的多项式,F(x)(f(x),fm(x),fi(x)是属于Rx 上的多项式.在下文中,为方便阐述,我们有时用程序空间来刻画所对应的循环程序.为了方便读者对于后续概念的理解,我们用下列循环贯穿全文进行阐述.E x a m p l e:w h i l e(xy),d ox x,y y 不变集定义(不变集)给定循环程序,集合Q被称为程序的不变集,如果xQ,有x Q.由不变集的定义可知,若循环程序存在不变集,那么不变集中的点将在此集合内进行无穷迭代,无法跳出该集合,表明该循环程序无法终止.秩函数秩函数法作为当前终止性分析的主流方法已得到广泛研究.给定一个循环程序,若能找到它的秩函数,则表明该循环是终止的.定义(秩函数)给定循环程序,函数f(x)被称为该程序的秩函数,如果它满足以下条件:x,f(x)c,c()x,f(x)f(x)c()x 为x迭代一次获得的状态点,上述秩函数的定义与传统秩函数定义是等价的.传统秩函数的定义如下:x,f(x)()x,f(x)f(x)c()为了方便实验,本文在秩函数的定义上采用定义中的式()、式(),而传统定义中的式()、式()可以等价改写为式()、式().这是因为,如果函数f(x)满足定义中的式()、式(),则 在 式()两 端 同 时 加 上 一 个 正 数c且 令f(x)f(x)c,(c),则 有f(x)c;同 时 不 难 看 出,f(x)f(x)f(x)c(f(x)c)f(x)f(x)c,显然f(x)满足式()、式().反之,若存在f(x)使得式()、式()成立,则令c c,那么式()、式()平凡成立.由式()、式()的性质可知,借助秩函数有界和递减的两个性质,将循环程序的状态映射到一个良基集中,程序每经过一次循环迭代,秩函数的值都会减少,直到抵达秩函数下界.由此可得,如果循环程序存在秩函数,那么它一定能够终止.增函数与最终线性秩函数下面介绍文献 中增函数的概念,该概念将被应用于下文对非双向迭代循环的终止性分析中.定义(增函数)给定循环程序,函数q(x)被称为上的增函数,如果对任意的x,有q(x)q(x),其中x 为x迭代一次获得的状态点.若增函数是线性的,那么它刻画了一个超平面.在增函数的划分下,循环空间中的状态点经过有限次迭代后都会进入划分超平面上方与循环空间相交的部分.接着,在该相交王垚,等:基于迭代轨迹划分的单分支循环程序终止性分析的部分中寻找线性秩函数.而在被划分得到的子空间寻找到的秩函数被称为最终线性秩函数.增函数的引入,将寻找原先整个循环空间上秩函数的问题转化为寻找循环空间子空间上秩函数的问题,增大了线性秩函数被找到的可能性.E x a m p l e:w h i l e(x),d ox xy,y y对于上述循环,其增函数为f(x,y)y,因为f(x,y)f(x,y)(y)(y).单分支循环程序终止性判定本章将主要研究单分支循环的终止性问题.增函数划分法的引入,将在整个循环空间寻找秩函数的问题转化为在其子空间寻找,这增大了秩函数被找到的可能性.受此启发,本文的一个基本思路是:能否通过某种不同的划分方法,将原先的循环空间划分为多个不相交的子空间,并通过证明每个子空间都存在秩函数,进而证明循环程序是终止的.为此我们根据循环空间中状态点的迭代路径特点,提出了一种新的循环程序类型,即双向迭代循环.这类循环的程序空间可被超平面分为个部分,更重要的是,寻找这个子空间中的秩函数即可判断整个循环程序的终止性.因此,这类循环终止性问题的判断符合提出的基本思路.此外,对于非双向迭代循环,本文仍然引用文献 中增函数的划分方法对程序空间进行划分.在寻找这两类循环被划分后所得的子空间中的秩函数时,我们证明其子空间中秩函数的计算问题都可以归结于二分类问题,故可利用S VM算法获得秩函数.基于迭代路径的划分 双向迭代循环循环空间中状态点的迭代由赋值语句决定,其迭代路径可能为沿着某一固定方向前进,也有可能在整个循环空间中进行没有规律的变化.在各种迭代路径中,我们发现,有一类循环的迭代路径会沿着某个超平面来回跃迁.下文中,我们称这类循环为双向迭代循环,并给出定义.定义(双向迭代循环)给定一个循环程序P:w h i l ex,d ox F(x),如果存在超平面g(x)aTxb,使得下列条件成立时,则P被称为双向迭代循环.xRn:g(x)xRn:g(x)()x(xg(x)x(xg(x)()由该定义可知,超平面g(x)将循环空间分为部分:,xRn:g(x).,非空,所以中的状态点迭代一次后跳入超平面中或超平面下方;同样,中的状态点迭代一次后跳入超平面中或超平面上方.下面的定理表明,对任给的双向迭代循环,若状态点x在中,那么该状态点迭代后得到的下一个状态点x 依旧在该超平面上,即g(x).定理给 定 一 个 循 环 程 序P:w h i l ex,d ox F(x).若P为 双 向 迭 代 循 环,那 么:x,则 有x F(x)xRn:g(x).证明:由循环P的定义可知,是单连通集,且,所以不为空.假设存在x使得g(F(x),即x迭代一次后所得的F(x)不落在g(x)上.那么由g(x),F(x)的连续性可知,必存在Oo(,x)邻域,使得情形A或B发生:情形AF(Oo(,x)xRn:g(x)情形BF(Oo(,x)xRn:g(x)为了不失一般性,假设情形A发生,则必存在yOo(,x),有g(F(y),也即y在迭代一次后仍然在g(x)中.这显然与循环程序P为“双向迭代循环”的定义相悖,因为根据定义,中的点y迭代一次后将跳入xRn:g(x).同理,对情形B也可以用如上方法证明.综上所述,若P为双向迭代循环,那么:xxRn:g(x),有x F(x)xRn:g(x).定理表明,若循环程序P为双向迭代循环,那么任意中的点x,迭代一次后获得的状态点始终在g(x)这个超平面上,即:xg(F(x).因此有以下情况出现:中的点x迭代一次后获得的新迭代点x,有可能落在或xRn:g(x)中.不难看出,若对x,都有x F(x),则为该循环的不变集.显然,若为不变集,则循环程序P是不终止的,这为双向迭代循环P是不终止的提供了充分的判准.接下来将介绍如何判断一个循环程序P是否是双向迭代循环,根据定义可知,这等价于寻找一个满足式()和式()的划分超平面g(x).因此,可以通过式()和式(),利用r e d l o g等工具去计算双向迭代循环的划分超平面.E x a m p l e:针对E x a m p l e,考虑该循环的划分超平面为g(x)a xb yc,用该式替换定义中的式()和式()中的g(x),通过r e d l o g命令求解,消掉式()和式()中的x和y,获得关于a,b,c的约束关系,发现当a,b,c时,满足a,b,c的约束关系,获得该循环的划分超平面为y.如果循环程序P是双向迭代循环,接下来将证明若,上存在秩函数f(x),f(x),f(x),那么循环程序P就是终止的,接下来给出三段式秩函数的概念.三段式秩函数定义(三段式秩函数)给定一个双向迭代循环P,我们称函数f(x)是P的三段式秩函数,如果它满足式()式():f(x)f(x)aTU(x),xf(x)aTU(x),xf(x)aTU(x),x()xf(x)c,cf(x)f(x)c,x F(x)()xf(x)c,cf(x)f(x)c,x F(x)()xf(x)c,cf(x)f(x)c,x F(x)()其中,Ui(x)(x:|d),xxxnn,|n,比如,当d,n,Ui(x)(xx,xx,xx,xx,xx,xx,xx,xx,xx).C o m p u t e rS c i e n c e计算机科学V o l ,N o ,S e p 由定义可 知,满 足 式()式()的 函 数f(x),f(x),f(x)分别为,上的秩函数.接下来证明,对于给定的双向迭代循环P,若上述定义的三段式秩函数存在,则该双向迭代循环P终止.定理给定一个双向迭代循环程序P,若P存在满足上述定义的三段式秩函数,那么P终止.证明:假设P不终止,那么上存在无穷迭代序列Sxi|i.由P是双向迭代循环可知,该无穷迭代序列存在种情形:情形S中的点在与上相互交替迭代,即xk且xk;或xk且xk;情形S中的点只出现在上,即S;情形S中的初始点x从或开始,即x(或x)经过有限次迭代后跳到上,由定理可知,之后其始终在中迭代.对于情形可以发现,虽然初始点x(或x),但有限次迭代后都会落入中.由于S是无穷迭代序列,舍去情形中未进入中的部分状态点,所得到的新的序列仍然是无穷迭代序列,因此情形可以归为情形.在接下来的证明中,我们只需要讨论情形和情形即可.下面分别证明当情形和情形发生时,P不终止的假设不成立.)考虑情形,假设S在与上相互交替,不失一般性,下文考虑xk且xk这种情况,那么会出现以下序列:():x,x,x,():x,x,x,由三段式秩函数的定义可知,f(x)和f(x)是与上的秩函数,所以有:f(xi)f(xi)cf(xi)f(xi)c继而有:f(x)f(x)f(x)f(x)f(x)f(x)又因 为S为 无 穷 迭 代 序 列,所 以 存 在xn,x n,使 得f(xn)c且f(x n)c,与f(x)的定义f(x)c且f(x)c相悖,因此情形不存在.)考虑情形,假设S只出现在上,f(x)是上的秩函数,那么对于序列S则有:f(xi)f(xi)c继而有:f(x)f(x)f(x)又因为S为无穷迭代序列,所以存在xn,使得f(xn)c与f(x)的定义f(x)c相悖,因此情形不存在.综上,若双向迭代循环存在三段式秩函数,那么该双向迭代循环一定终止.在判断双向迭代循环终止性时,我们先判断划分超平面与循环空间相交的部分,即是否为不变集.如果是不变集,那么双向迭代循环不终止;如果不是不变集,那么我们寻找该双向迭代循环是否具有三段式秩函数.计算秩函数对于双向迭代循环,我们利用满足定义的超平面进行划分,得到两个互不相交的子空间;对于非双向迭代循环,我们引用文献 中增函数的方法进行划分,得到子空间.无论使用哪种划分方法,划分后都会将原空间中秩函数的计算问题归结于子空间中秩函数的寻找问题.不失一般性,令划分后的子空间为i,该空间上的秩函数为fi(x):fi(x)aTiUi(x),xi()由于fi(x)是i上的秩函数,故有(x,xm),xixmFm(x)aTiUi(x)caTi(Ui(x)Ui(xm)c()令Gi,(x,xm)Ui(x)()Gi,(x,xm)Ui(x)Ui(xm)()中不同区域上的点按Gi,j,j,映射到象空间,从而得到中各区域在该映射下的象集:Gi,(i)u|uUi(x),xixmFm(x)()Gi,(i)u|uUi(x)Ui(xm),xixmFm(x)()继而可以得到:aTiGi,(i)caTiGi,(i)c()令SGi,(i)Gi,(i).综上所述,对于任意循环程序,其子空间i存在秩函数等价于存在aTi和正数c使式()成立.文献 将寻找嵌套秩函数的问题转化为寻找某个超平面的问题,该超平面能够将某个集合与原点严格分离.此证明思路可以被应用于证明定理.定理记号同上.给定一个循环程序P,令其划分后的子空间为i,若其子空间i上存在秩函数,当且仅当存在一个超平面L能够将集合S上的点和原点o严格分离.证明:)假设给定的循环程子空间i存在秩函数,即:fi(x)aTiUi(x),xi我们需要证明存在超平面L能够将集合S上的点和原点o严格分离.令waTi,构 造 超 平 面Lwuc,因 为o(,)T,并 且c,所 以L(o)wocc.对于uS,L(u)wucccc,因此超平面L能够将集合S上的点和原点o严格分离.)假设存在超平面Lwub能够将集合S上的点和原点o严格分离,接下来证明程序i上的确有秩函数,这等价于证明存在aTi使得秩函数成立.存在两种情况:()L(o)L(u),u)S()L(o)L(u),u)S王垚,等:基于迭代轨迹划分的单分支循环程序终止性分析本文只讨论情况(),类似的方法可应用于情况().L(o),可以推出wob,即b,b.又因为L(u),uS,即wub,wub,wbu,令w wb,可得,对于uS,w u.令c,那么对于uS,则有:aTibGi,(i)caTibGi,(i)c因此存在aTib和c使得式()成立,故该循环程序子空间i上的秩函数为:fi(x)aTibUi(x),xi综上,给定一个循环程序,其子空间i上存在秩函数,当且仅当存在一个超平面L能够将集合S上的点和原点o严格分离.验证由于通过S VM算法获得的秩函数为秩函数候补,因此还需进一步验证其是否在对应的空间上满足有界和下降这两个条件.本文实验使用工具b o t t e m a验证候选秩函数,其他工具如Z 也可以进行验证.为了使候选秩函数有更大的概率通过验证,我们利用迭代的思想缩小原先的验证空间,获得新的待验证区间,接着在此区域上对候选秩函数进行验证,具体思路如下.对于一个循环程序P,假设fk(x)为其划分后子空间k上的候选秩函数.利用缩小区域法验证fk(x)的思路如下:首先在k上验证fk(x)是否满足有界和下降两个条件,若满足,则fk(x)是k上的秩函数,若不满足,则令()kkF(),其中F()x:F(x),获得缩小后的子空间()k,()k为k的子集;接着在()k验证fk(x)是否为满足条件的秩函数,若满足,则fk(x)是()k上的秩函数,若不满足,则继续调用缩小区域算法进行验证,令()k()kF(),()k表示k经过两次缩小区域法获得的子空间,以此类推直到达到缩小次数上界.下面定理将证明,虽然fk(x)为其子空间k上的候选秩函数,但是只要fk(x)是k经过i次缩小区域法获得的某个子空间(i)k上的秩函数,则k中的点最终都会跳出k.定理(记号同上)令(i)k为对k调用i次算法获得的子空间.若fk(x)是(i)k上的秩函数,则k中的点最终都会跳出k.证明:由已知可得,(i)k(i)kFi(),为子空间(i)k调用一 次缩 小区 域算 法 获得,将(i)k分 为 两 部 分:(i)k和(i)k(i)k,令(i)k(i)k(i)k.因为fk(x)是(i)k上的秩函数,所以(i)k中的点经过有限次迭代将会跳出(i)k,那么就会有以下两种情况发生:(i)k中的点直接跳出k或者落入(i)k,(i)kk()k(i)k(其中kk()k,(i)k(i)k(i)k),根据缩小区域法的缩小规则可知,()k排除了k中迭代一次就会跳出的状态点,即k中的点迭代一次就会跳出,所以(i)k是迭代i次就会跳出的状态点的集合.由此可知,(i)k中的状态点经过有限次迭代后都会跳出循环空间,因此,(i)k中的点经过有限次迭代后都会跳出循环空间k.综上可得,若fk(x)是(i)k上的秩函数,k中的点最终都会跳出k.由定理可知,若k经过缩小区域法得到的子空间中存在秩函数,那么k中的点最终都会跳出k,因此我们接下来将证明整个程序P终止.定理(记号同上)如果k中的点最终都会跳出k,那么程序P终止.证明:下面将分别对非双向迭代循环和双向迭代循环进行讨论:对于非双向迭代循环,经过i次缩小区域算法后获得(i)k,该区域中 的 点 经 过 有 限 次 迭 代 跳 出k的 迭 代 路 径 如 图所示.图非双向迭代循环状态点迭代路径F i g N o nb i d i r e c t i o n a l l o o ps t a t ep o i n t i t e r a t i o np a t h路径(a)表示(i)k中的点跳入区域k,由于非双向迭代使用增函数划分,这表明中的点进入k不会再进入区域k,所以路径(a)不成立;那么仅剩路径(b),该路径表示,(i)k中的点跳出循环空间.因此,对于非双向循环,k中的点最终都会跳出循环空间.故非双向迭代循环程序终止.对于双向迭代循环,为了不失一般性,我们考虑经过i次缩小区域算法后,获得区域的(i).该区域中的点经过有限次迭代跳出的迭代路径如图所示.图双向迭代循环状态点迭代路径F i g B i d i r e c t i o n a l l o o ps t a t ep o i n t i t e r a t i o np a t h路径(c)表示(i)中的点跳入区域(j),而该区域中的点经过有限次迭代都会跳出循环空间;路径(d)表示(i)中的点跳入区域(j),对于这条路径,我们考虑定理的证明方法,可以证明不会存在交替于(i)与(j)间的无穷迭代序列,所以这条路径上的状态点最终也会跳出循环空间;路径(e)表示(i)中的点跳出循环空间.所以对于双向循环,中的点最终都会跳出循环空间.同理,中的点最终都会跳出循环空间,故双向迭代循环程序终止.综上,如果k中的点最终都会跳出k,那么程序P终止.C o m p u t e rS c i e n c e计算机科学V o l ,N o ,S e p 程序所需的子算法本节将对基于迭代轨迹划分方案中所需要的部分重要子算法进行介绍,以便读者理解方案的具体执行细节.判断循环程序是否存在不变集通过寻找输入集合的不变集来判断循环程序是否不终止,若存在不变集,则判定结果为存在不变集,否则为不存在不变集.对双向迭代循环的判定算法如算法所示,非双向迭代循环的判定算法如算法所示.算法R S TW()r e c u r r e n t s e to f t w o w a y l o o p输入:循环程序,迭代映射F,划分ft w输出:“t r u e”o r“f a l s e”i fx(Rn:ft w(x)x F(x)x (Rn:ft w)t h e n r e t u r nf a l s e;e l s e r e t u r nt r u e;e n d i f算法R S UTW()r e c u r r e n t s e to fu n t w o w a y l o o p输入:循环程序,迭代映射F,增函数fi n c输出:“t r u e”o r“f a l s e”i fx(x fi n c(x)x F(x)x (fi n c(x)t h e n r e t u r nf a l s e;e l s e r e t u r nt r u e;e n d i f 验证候选秩函数通过输入经过划分后获得的子空间,以及每个子空间上的候选秩函数,验证候选秩函数是否准确,若通过验证,则认为获得了准确的秩函数,否则调用缩小区域法对验证空间进行缩小,在新获得的验证区域上继续进行验证,若调用缩小区域算法的次数超过最大设定值,则认为候选秩函数未通过验证.对双向迭代循环的判定算法如算法所示,非双向迭代循环的判定算法如算法所示.算法C TW()c e r t i f i c a t e t w o w a y l o o p输入:被ft w划分后的到的,秩函数f,f,f(x)可调参数c(c),调用次数t,最大调用次数t输出:“t r u e”o r“f a l s e”i f t t r e t u r nf a l s e;i f(x(f(x)a n df(x)f(x)c)a n d(x(f(x)a n d f(x)f(x)c)a n d(x(f(x)a n df(x)f(x)c)t h e n r e t u r nf a l s e;e l s e t t;n a r r o wd o m a i n;C TW();e n d i f e n d i f算法C UTW()c e r t i f i c a t eu n t w o w a y l o o p输入:被fi n c划分后的到的,秩函数f,可调参数c(c),调用次数t,最大调用次数t输出:“t r u e”o r“f a l s e”i f t t t h e n r e t u r nf a l s e;e n d i fi f(x(f(x)a n d f(x)f(x)c)t h e n r e t u r nf a l s e;e l s e t t;n a r r o wd o m a i n;C TW();e n d i f 判断双向迭代循环是否终止判断双向迭代循环是否终止,首先通过寻找不变集来判断循环程序是否不终止,接着通过寻找秩函数来判断循环程序是否终止,具体步骤如算法所示.算法J TW()j u d g e t w o w a y l o o p输入:循环程序,迭代映射F输出:“t r u e”o r“f a l s e”寻找循环的划分ft w;i fR S TW()t h e n p r i n t“循环程序不终止”;r e t u r nt r u e;e l s e S VM();i fC TW()t h e n p r i n t“循环程序终止”;r e t u r nt r u e;e l s e r e t u r nf a l s e;e n d i f e n d i f 判断非双向迭代循环是否终止判断非双向迭代循环是否终止和判断双向迭代循环是否终止的思路大致相同,区别在于前者执行算法前需要提前设置最大划分次数,具体步骤如算法所示.算法J UTW()j u d g eu n t w o w a y l o o p输入:循环程序,迭代映射F,寻找次数p,最大寻找次数p输出:“t r u e”o r“f a l s e”w h i l e pp pp;寻找循环的划分fi n c;i fR S TW()t h e np r i n t“循环程序不终止”;r e t u r nt r u e;e l s e S VM();i fC UTW()t h e n p r i n t“循环程序终止”;r e t u r nt r u e;e l s e r e t u r nf a l s e;e n d i f e n d i f e n dw h i l e r e t u r nf a l s e 判断循环程序是否终止划分方案的完整执行流程如算法所示.首先寻找 输王垚,等:基于迭代轨迹划分的单分支循环程序终止性分析入循环程序的不动点,再分别进行 双向 迭代循环以及非双向迭代循环的判断,如果超过了非双向迭代判定算法中设置的最大划分次数跳出后,则认为基于迭代轨迹的划分方案无法对输入的循环程序进行处理,输出结果“循环程序未知”.算法R S TW()r e c u r r e n t s e to f t w o w a y l o o p输入:循环程序,迭代映射F输出:“循环程序终止”或者“循环程序不终止”或者“循环程序未知”i fF P()t h e n r e t u r n“循环程序不终止”;e l s e i f!J TW()t h e n i f!J UTW()t h e n p r i n t“循环程序未知”;r e t u r nt r u e;e l s e b r e a k;e n d i f e l s e b r e a k;e n d i f e n d i f 流程图整个算法的运行流程如图所示.图算法流程图F i g F l o wc h a r to f a l g o r i t h m实验结果将寻找秩 函 数 问 题 转 化 为S VM分 类 问 题,