软件学报  2015, Vol. 26 Issue (2): 297-304   PDF    
多分支单变量循环程序的终止性分析
李轶1, 李传璨1,2, 吴文渊1    
1. 自动推理与认知重庆市重点实验室中国科学院 重庆绿色智能技术研究院, 重庆 401120;
2. 重庆邮电大学 计算机科学与技术学院, 重庆 400065
摘要:对多分支单变量循环程序的终止性问题进行了研究.证明了在适定的条件下,该类循环程序不可终止性的充分必要条件是迭代映射在循环条件形成的区域中有不动点.特别地,当这类循环程序是多项式循环程序时,在给定条件下,其在实数域上的终止性问题是可判定的.
关键词可信计算     多分支循环程序     终止性分析    
Termination Analysis of Multipath Loop Programs with One Variable
LI Yi1, LI Chuan-Can1,2, WU Wen-Yuan1    
1. Chongqing Key Laboratory of Automated Reasoning and Cognition Chongqing Institute of Green and Intelligent Technology, The Chinese Academy of Sciences, Chongqing 401120, China;
2. College of Computer Science and Technology, Chongqing University of Posts and Telecommunications, Chongqing 400065, China
Abstract: Termination of multipath loop programs with one variable is analyzed in this paper. It demonstrates that under proper conditions, this kind of loops is non-terminate if and only if there exist fixed points. Especially, if the class of programs are polynomial, then under proper conditions, the termination of the programs is decidable over the reals.
Key words: trusted computing     multipath loop program     termination analysis    

随着信息技术的迅猛发展,嵌入式系统在人类生活中发挥着越来越大的作用,而作为嵌入式系统灵魂的嵌入式软件在其中所占有的比重也越来越大.因此,嵌入式软件的可靠性将变得更加重要.诸如航空、航天、军事、交通、医疗等关键应用领域都对嵌入式系统的可靠性和安全性要求非常高,任何错误的发生都可能带来灾难性后果.这些系统被称为攸关安全系统.

嵌入式系统具有3个重要属性:可达性、终止性、不变式.可达性是指一个系统能否从一个给定状态到达另一个可接受状态,某些混成系统的可达性被证明是能用计算机代数工具来检验的;不变式则是系统变量在循环迭代时永远保持的特性;而终止性是研究系统中是否会发生死循环.不包括终止性分析的验证被称为程序的部分正确性证明[1],因此,程序的终止性分析是确保程序完全正确性的必要基础.

尽管程序的终止性问题早已被证明是不可判定的[2],但对其进行研究不仅具有理论意义,更具有实际意义.当前,国际上主要通过合成秩函数来进行循环终止性分析.当程序的秩函数被找到时,则表明程序是可终止的.利用多面体理论和整数规划等代数方法,国外科学家在线性秩函数的合成方面取得了大量成果[3, 4, 5, 6, 7].此外,我国科学家杨路、夏壁灿、詹乃军和周巢尘等人将秩函数和不变式的计算归约为半代数系统的求解,并运用实代数工具DISCOVERER提出了(非线性)多项式型不变式和秩函数生成的方法[1,8,9].不同于文献[10]中的方法,他们的方法能够精确判定循环程序是否有给定模板的秩函数或不变式.合成秩函数是验证循环程序终止性的一条重要途径,但是秩函数的存在是循环可终止的充分而非必要条件.即,可以构造一个循环程序,它是可终止的,但并没有秩函数.由此证明循环程序终止性的另一途径就是避开秩函数的合成.而采用数学方法严格证明某类或某些类循环程序的终止性是可判定的,并建立相对完备的判定算法.从可判定的角度进行终止性研究的结果甚少.2004年,Tiwari在文献[11]中首次证明了下列循环程序在实数域上的终止性是可判定的:

Q1 While BX>0 do

{X:=AX}

这里,A,BÎRnxn,XÎRn相似的结论被Braveman[12]推广到整数环上.此外,为避免Jordan标准型的浮点计算,文献[13]中提出了精确的符号计算方法对程序进行终止性判定.2010年,文献[14]对程序的终止性进行了分析,证明了当程序满足给定的NZM(non-zero minimum)条件时的终止性是可判定的:

Q2 While P(X)>0 do

{X:=AX}

其中,P(X)为(非线性)多项式.从可判定的角度,目前的研究多集中于单重循环程序的终止性分析,而针对带多分支语句的循环终止性分析结果甚少.2005年,Bradley等人[15]研究了一类多分支多项式循环程序的终止性问题.他们的方法极大地依赖于循环程序中表达式的有限差分树结构,并建立了不完备的判定方法.但大多数循环程序并没有有限差分树结构,因而限制了该方法的使用.

本文中,我们对一类带多个分支的单变量循环程序的终止性问题进行了分析.证明了当满足所给定的条件时,这类循环不可终止的充分必要条件为迭代映射在循环条件形成的区域中有不动点.倘若我们将这类循环中的表达式都限定为多项式表达式(这类循环称为多分支单变量多项式循环程序),那么在满足给定条件下,根据由Tarski提出的一阶多项式公式的真伪是可判定的这一结论可知,这类多分支单变量多项式循环程序在实数域上的终止性问题是可判定的.针对多分支单变量多项式循环程序,文中定理给定的条件非常容易借助实代数工具QEPCAD和DISCOVERER去验证.不同于Bradley等人的方法,本文呈现的方法并不需要循环程序具有有限差分树的结构.

1 主要结果

下文中,我们称由迭代函数F和循环条件形成的区域I所构成的循环程序P(F,I)在实数域¡是不可终止的,如果存在一点x0Ρ,使得.这里,Fi=FoFo…oF表示函数的复合.如果那样的x0不存在,则称循环

P(F,I)在实数域上可终止.

定理1. 令f:RaR为一维连续映射.I为一闭区间.循环程序

P1 While xÎIdo

{x:=f(x)}

是不可终止的充分必要条件为迭代映射f在闭区间I上有不动点.

证明:充分性.如果fI上有不动点,则程序P1显然不可终止.

必要性.若fI上没有不动点,则由函数的连续性可知:必存在正数c>0,使得对任意的xÎI,有f(x)-xc>0;或者,必存在正数c>0,使得对任意的xÎI,f(x)-x≤-c<0.下面我们将分两种情况证明程序P1必然终止.

(1) 存在正数c>0,使得对任意的xÎI,有f(x)-xc>0.任取一点x0ÎI,由x0将产生一无穷迭代序列:

下面将证明必存在一正整数k,使得迭代序列中的点fk(x0)ÏI.假设这样的k不存在,那么有

又因为存在正数c>0,使得对任意的xÎI,f(x)-xc>0,则有:

x0f(x0)-cf2(x0)-2c≤….

因此,在有限步后,迭代序列中的点将跳出区间I.假设不成立,这样的k必然存在,即,在情形(1)中,程序P1必然可终止.

(2) 存在正数c>0,使得对任意的xÎI,有f(x)-x≤-c<0.类似于情形(1)的分析,同理可证明:对任意的x0ÎI,必存在正整数k,使得fk(x0)ÏI.即,程序P1I上可终止.综上所述,fI上没有不动点时,程序P1可终止. 

记循环程序:

P2 While xÎI do { if xÎI1 then x:=f1(x) else if xÎI2 then x:=f2(x) … else if xÎIn-1 then x:=fn-1(x) else x:=fn(x) }

这里,fi:RaR为一维连续映射.令

为一闭区间,且IiÇIj=Æ("i¹j).根据上述记号,程序P2可被重写为

P2 While xÎIdo

{x:=F(x)}

定理2. 记号同上.记分别为区间I,Ii的端点集合.令.如果满足以下条件,那么,程序

P2是不可终止的的充分必要条件为迭代映射F在闭区间I上有不动点:

(1) 存在正数d>0,使得对任意的xÎI都有:

(2) 存在¡上的连续函数T(x),使得下列分段函数:

(1)

在闭区间I上连续,且满足(3).

(3) 对任意的xÎI,有G(x)=0ÞF(x)-x=0(即,对任意的xÎIi,有Tofi(x)-T(x)=0Þfi(x)-x=0,i=1,2,…,n).

证明:充分性.若FI上有不动点,则程序P2不可终止.

必要性.若程序P2不可终止,必存在无穷迭代序列D={x0,F(x0),F2(x0),…}ÍI.令因为T连续,故数列T(D)有界,记其上、下确界分别为.分两种情形:

(A) 若T^ÎT(D),则必存在T(xt)=T^ÎT(D).令x^=xt.故存在x^ÎD,有: T(F(x^))≤T(x^).

(B) 若T^ÏT(D),则由确界性质可知:必存在子列收敛于T^,也即

因为数列有界,故必有收敛子列.即

.

因为由题设可知:存在正数d>0,使得对任意的xÎI都有

T的连续性可知:

且因为为收敛数列的子列,故有T(x)=T^.令

因为T^T(D)的上确界,故对任意的n,有ToFn(x0)≤T^=T(x^).因此有:

(2)

因为F上连续,故,

因此,对公式(2)两边取极限,有ToF(x^)≤T(x^).

综上所述,无论情形(A)或情形(B),均可得到一点使得ToF(x^)≤T(x^).

同理,对下确界,采用完全类似的分析可知,必存在一点,使得

又因为由题设中的条件(2)可知:函数G(x)=TF(x)-T(x)在I上连续,且ToF(x^)≤T(x^),,故必

存在使得根据题设中的条件(3)可知,必有故,FI上不动点.

注:因为迭代函数F在闭区间上是不连续的,而题设条件(2)中辅助函数T(x)的引入便于构造闭区间上的连续函数.要检验定理中的条件(2)是否成立,即检验函数G(x)是否为I上的连续函数,仅需验证G(x)在相邻两个区间端点的函数值是否相等.比如,假设两个相邻区间为Ij=(aj,bj),Ij+1=[aj+1,bj+1],bj=aj+1.G(x)要在I上连续,必须满足G(bj)=G(aj+1).辅助函数T(x)的构建是关键.在实际的计算中,我们无法事先知道辅助函数T的具体表达式.为了计算出T,我们需要先给出T的一个参系数模板(为了便于计算,文中我们选用了多项式模板).然后,通过工具DISCOVERER和QEPCAD,我们得到了参系数的取值范围f(a,b,…)(这里,a,b,…为模板中的参系数).f(a,b,…)是一个由多项式等式或不等式构成的半代数系统.如果这个系统f(a,b,…)非空,即,存在a,b,…的某个取值a*,b,…满足f(a,b,…),则满足题设的函数T被构造出来;否则,若f(a,b,…)为空,则我们需要修改T的模板再重新计算.因此,若系统f(a,b,…)非空,则T的选择是很多的,甚至是无穷多种选择.

定理2的结论可以推广到更加一般的情形.首先给出一些记号.

n个闭区间,为定义在闭区间上的函数.这里,fi,Fi分别型如程序P1,P2中的迭代映射.若则表明为闭区间上一个连续函数;若则表明为闭区间上一个逐段连续函数.

根据定义的不同类型的迭代函数,n个闭区间可被分为两类:

对任意的iÎL2,记且对任意的j,j¢=1,...,ki,有IijÇIij¢=Æ.同时,对任意的iÎL2,记分别为区间的端点集合.令xL,xR分别为闭区间中最小的左端点和最大的右端点,且令显然,同时,令

这里,

定理3. 记号同上.如果满足以下条件,那么,程序P3是不可终止的的充分必要条件为迭代映射

上有不动点:

(1) 存在正数d>0,使得对任意的都有:

(2) 存在¡上的连续函数T(x),使得下列分段函数:

(3)

在闭区间上连续,即,对任意的i,在区间上连续;且对任意两个相邻区间

在区间右端点的函数值等于在区间左端点的函数值.且满足:

(3) 任意的,有.即,对任意的有:

i=1,2,…,n.

(4) G(x)在上没有零点.

证明:这个证明非常类似于定理2的证明.若上有不动点,则程序P3显然不可终止.假设程序P3不可终止,类似于定理3中的证明,题设中的条件(1)、条件(2)保证了在中必然存在两点,使得:

因此,根据G上的连续性可知:必在上存在一点

根据题设中的条件(4)可知,再根据条件(3),即得

定理1~定理3将一类多分支单变量循环程序在实数域上的终止性问题等价地规约为判定其赋值函数在循环条件中的区间上是否有实的不动点的问题.这里,各定理中的赋值函数仅要求连续即可.因此,连续赋值函数表达式的复杂多样性导致不动点的计算变得困难.但是,倘若我们将赋值函数限定为多项式,则区间上不动点是否存在的判定问题等价于一个半代数系统有无实数解的判定问题.后者可以用一阶多项式公式来描述,进而根据Tarski的结论可知该问题是可判定的.同时,既然循环中所有表达式均为多项式的,那么定理中各题设条件的验证问题均可等价转换为半代数系统有无实解的问题.由上述分析可知,后者是可判定的.因此,由上述分析,我们有以下显然的结论:

定理4. 在满足定理1~定理3的题设条件下,型如P1,P2,P3的多分支单变量多项式循环程序在实数域上的终止性是可判定的.

下面,我们给出几个具体的多项式循环程序来阐述本文的方法.

2 实 例

例1:考虑下列循环的终止性:

While -3≤x≤1 do

{x:=11x6+41x5+2x4-7x3-21x2+15x-71}

迭代函数f在循环条件[-3,1]上没有不动点,由定理1可知,该循环必然终止.既然定理1中仅需要迭代函数为连续函数,那么定理1对下列循环仍然适用:

例2:考虑下列循环的终止性:

else x:=7x-3 }

While -3≤x≤5 do

{ if -5≤x<0 then x:=-4x+2

else if 0≤x≤1 then x:=2x3+2

else if 1<x<3 then x:=x2+3x

不难验证,相邻两端段函数在间断点处的函数值均相等,故迭代函数在区间[-5,5]连续.迭代函数在循环条件[-5,5]上没有不动点,由定理1可知,该循环必然终止.

While x2≤4 do

{

if 0<x≤2 then x:=-x2-1

else x:=2x2+x+1

}

例3:考虑下列循环的终止性:

f1=-x2-1,f2=2x2+x+1.显然,-1=f1(0)¹f2(0)=1.故迭代函数在x=0处不连续,因此定理1对该循环不再适用.我们将利用定理2对该循环的终止性进行判定.根据定理2的题设,需要首先验证3个条件是否满足.记循环条件围成的闭区间为I=[-2, 2],两分支条件确定的区间分别为I1=(0,2),I2=[-2, 0].那么由定义可得:

首先验证定理2中的条件(1)是否满足,这等价于判定下列量词公式是否成立:

$d"x((xÎIÙd>0)Þ(F(x)≥dÚF(x)≤-d)).

通过工具QEPCAD可以判定上述公式成立.由此可知:对任意的xÎI,F(x)都不会位于间断点x=0的某一d邻域内.即,定理2中条件(1)得到满足.

其次,为验证该循环是否满足定理2中条件(2)、条件(3),构造¡上的连续函数T(x).令T(x)=ax2+bx,a,bΡ为

参数.根据定理2中的公式(1),可构造函数G(x).为保证G(x)在区间I内连续,只需使得G(x)在I内唯一间断点x=0处连续,即,需要满足:

Tf1(0)-T(0)=Tf2(0)-T(0)  (4)

根据公式(4),可得参数约束b=0.即,当且仅当b=0时,公式(4)成立.同时,为验证定理2中的条件(3)是否被满足,等价于验证下列系统无解:

x2-4≤0ÙG(x)=0ÙF(x)-x¹0 (5)

利用实代数工具DISCOVERER中的命令求解公式(5),即,

· tofind([Tf1(x)-T(x)],[2-x],[x],[f1(x)-x],[x],[a,b],0);

· tofind([Tf2(x)-T(x)],[x+2,-x],[×],[f2(x)-x],[x],[a,b],0).

得到如下参数a,b的约束:

(3a-b)(3a-4b)>0Ù(a+2b)(5a+b)>0 (6)

结合前面得到的约束b=0,求解所有参数约束可得到a=1,b=0.故定理2题设中的连续函数T(x)存在.

综上所述,定理2中的3个条件都满足,根据定理2,该循环不可终止的充要条件是迭代函数FI上有不动点.经过计算,迭代函数FI上没有不动点,故该循环可终止.

例4:考虑下列循环的终止性:

While -2≤x≤-1Ú1≤x≤2 do

{

if -2≤x≤-1 then x:=-2x2-4x+1

else

}

该循环条件由两个闭区间构成,故定理1、定理2均不适用.

根据定理3中的记号,令,记:

下面验证定理3中的条件是否被满足.

首先,既然L2=Æ,那么定理3中的条件(1)自然成立.

其次,构造连续函数T(x)=ax2+bx,并由此构建型如公式(3)的连续函数G(x).

,显然有

因此,G(x)要在上连续,必须满足由此得到参数约束:

b=-10a (7)

当公式(7)成立时,定理3中的条件(2)得到满足.为了满足定理3中的条件(3),等价于下列系统无实数解:

-2≤x≤-1ÙTf1(x)-T(x)=0Ùf1(x)-x¹0 (8)

1≤x≤2ÙTf2(x)-T(x)=0Ùf2(x)-x¹0  (9)

调用tofind命令,可以得到参数约束:

(a-b)(2a+b)<0Ù(44a+5b)(21a+5b)>0 (10)

最后,要满足定理3中的条件(4),等价于下列系统无实数解:

-1<x≤0ÙTf1(x)-T(x)=0 (11)

0<x<1ÙTf2(x)-T(x)=0 (12)

调用tofind命令,可以得到参数约束:

(a+b)(17a+8b)>0Ù(44a+5b)(104a+11b)>0 (13)

根据参数约束(7)、参数约束(10)和参数约束(13),可得到a=1,b=-10.因此,存在连续函数T(x)=x2-10x,满足定理3的所有条件.故根据定理3,仅需计算其不动点是否在循环条件中来判定该循环的终止性.通过计算得知,

上没有不动点,故该循环可终止.

3 结 论

尽管循环程序的终止性问题被证明是不可判定的,但寻找可判定的程序子类并建立相应的判定算法具有重要的实际意义.本文对一类单变量多分支while循环程序的终止性问题进行了研究,证明了在给定条件下,这类循环程序不可终止的充要条件是迭代函数在循环条件形成的区域中有不动点.特别地,当这类循环程序为多项式循环程序时,证明了在适定条件下,该类多项式循环程序在实数域上的终止性问题是可判定的.本文方法的特点是:针对这类多分支单变量多项式循环程序,各个定理中的条件易于判定,即,容易通过实代数工具去验证定理中的条件是否成立;其次,判定不动点是否落入到循环条件形成的区域中的问题也可以转换为半代数系统求解,后者同样容易通过实代数工具进行判定.

致谢 感谢上海高可信计算重点实验室对本文工作的支持.

参考文献
[1] Yang L, Zhou CC, Zhan NJ, Xia BC. Recent advances in program verification through computer algebra. Frontiers of Computer Science in China, 2012,4(1):1-16 .
[2] Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011,54(5):88-98 .
[3] Ben-Amram AM, Genaim S. On the linear ranking problem for integer linear-constraint loops. In: Proc. of the 40th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM, 2013. 51-62 .
[4] Colón MA, Sipma HB. Practical methods for proving program termination. In: Brinksma E, Larsen KG, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2002. 227-240 .
[5] Colón MA, Sipma HB. Synthesis of linear ranking functions. In: Margaria T, Wang Y, eds. Proc. of the 7th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. London: Springer-Verlag, 2001. 67-81 .
[6] Bagnara R, Mesnard F, Pescetti A, Zaffanella E. A new look at the automatic synthesis of linear ranking functions. Information and Computation, 2012,215:47-67 .
[7] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In: Steffen B, Levi G, eds. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2004. 239-251 .
[8] Chen YH, Xia BC, Yang L, Zhan NS, Zhou CC. Discovering non-linear ranking functions by solving semi-algebraic systems. In: Jones CB, Liu ZM, Woodcock J, eds. Proc. of the Theoretical Aspects of Computing (ICTAC 2007). Berlin, Heidelberg: Springer- Verlag, 2007. 34-49 .
[9] Yang L, Zhan NJ, Xia BC, Zhou CC. Program verification by using DISCOVERER. In: Meyer B, Woodcock J, eds. Proc. of the Verified Software: Theories, Tools, Experiments. Berlin, Heidelberg: Springer-Verlag, 2008. 528-538 .
[10] Cousot P. Proving program invariance and termination by parametric abstraction Langrangian relaxation and semidefinite programming. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2005. 1-24 .
[11] Tiwari A. Termination of linear programs. In: Alur R, Peled DA, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2004. 70-82 .
[12] Braverman M. Termination of integer linear programs. In: Ball T, Jones RB, eds. Proc. of the Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2006. 372-385 .
[13] Xia BC, Yang L, Zhan NJ, Zhang ZH. Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing, 2009,23(2):171-190 .
[14] Xia BC, Zhang ZH. Termination of linear programs with nonlinear constraints. Journal of Symbolic Computation, 2010,45(11): 1234-1249 .
[15] Bradley A, Manna Z, Sipma H. Termination of polynomial programs. In: Cousot R, ed. Proc. of the Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2005. 113-129 .