几类While循环终止性分析的理论、方法及其应用

正确性是程序的最重要的属性之一。包含终止性分析的程序验证被称为完全的正确性验证。众所周知，循环终止性问题的描述和研究由来已久，对其终止性的判定和证明依然无法完全解决。因此，对具普遍意义的基本循环程序模型进行终止性分析将具有十分重要的意义。近年来，计算机代数领域建立的深刻理论及工具已逐渐在计算机视觉，自动控制等领域得到广泛应用。最近，诸如DISCOVERER和BOTTEMA等实代数工具已逐渐被应用于程序变元为实变量的嵌入式软件的分析及验证中。目前，我们已在线性及非线性循环程序终止性分析问题上展开了工作，并取得了初步成果。以计算机代数为理论基础，结合符号-数值混合计算方法，本项目拟在几类非线性循环程序的终止性分析，线性循环终止性的离线判定等方面做深入研究，并借助所建立的理论和已有的实代数工具，对出现于嵌入式软件中的几类循环程序进行终止性分析。

本项目应用计算机代数和实代数中的深刻理论及成熟工具，采取符号与数值计算相结合的方法对广泛存在于实际应用中的几类线性和非线性循环程序的终止性进行分析和验证。. 我们主要从两个方面来进行循环程序的终止性分析。其一，从可判定的角度进行终止性分析。尽管程序终止性问题早在上世纪30年代就被Tiwari证明是不可判定的，但人们仍然热衷于去探寻可判定的子类。其二，采用合成Ranking函数的方式进行终止性分析。基于Ranking函数合成的验证方法并不是完备的。这是因为，虽然，Ranking函数的存在印证了循环程序是可终止的，但Ranking函数不存在却并不能说明循环程序是不可终止的。因此，Ranking函数的存在仅仅是循环程序可终止的充分而非必要的条件。尽管如此，基于Ranking函数的终止性验证方法仍是当今进行终止性分析的主流方法。. 首先，从可判定角度，我们对一类线性while循环程序的终止性问题进行了分析。这类循环在2004年首次被斯坦福教授Tiwari提出，并证明了它在实数域上的终止性是可判定的。但是，我们发现，在多数情形下，如果此类循环程序是不可终止的，那么，Tiwari的方法所给出的点是一个N-不可终止点，即这样的点需要再迭代N次后才能成为一个不可终止点。而在他的文章中也并没有给出N的计算方法。因此，基于这个发现，我们提出了一种方法去计算N的值。其次，基于赋值矩阵Jordan块的特殊结构，我们将这类线性循环程序的终止性问题归于为两类特殊线性程序的终止性问题。而后者的终止性更易被判定。更为重要的是，如果该类循环程序是不可终止的，那么，我们的新算法能构造至少一个不可终止点。本项目中，除了对上述的线性循环程序的终止性进行分析外，我们也研究了部分非线性循环程序的终止性。一般地，非线性循环程序的终止性因为其更为复杂的迭代动力行为，从而导致其终止性方面的研究甚少。通过分析无穷迭代序列在某些条件下所呈现出的良好性质，我们证明了三类非线性循环程序在实数域上的终止性是可判定的，并证明了其是不可终止的充要条件是迭代函数在循环条件所形成的区域中有不动点。. 其次，借助工具DISCOVERER和CDS理论，我们也建立了基于Ranking函数合成的终止性验证方法。新方法中，我们引进一些松弛变量，从而使得最终的半代数系统更容易让现有的工具去自动求解。