区间上非线性程序的终止性判定
, PP. 3116-3123
Keywords: 程序验证,终止性分析,非线性程序,不动点,周期轨
Abstract:
分析了如下类型程序的终止性:whilex∈ωdo{x:=f(x)}end.其中,x是程序变量,ω是一个区间,f是一个连续函数.这类程序被称为区间上非线性程序.证明了上面程序不终止的必要条件是函数在区间内部或边界上有不动点.如果不动点不在区间的边界,则上述结果是充要条件.仅仅在区间边界上有不动点的情况下,对函数略加限制,也建立了相应结果.特别地,对逐段多项式连续函数程序的终止性给出了完备判定算法.
Full-Text