论文部分内容阅读
计算机代数方法和工具，如Grobner基计算、QEPCAD、DISCOVERER等已经应用到不变量生成，寻找秩函数，可达集计算等程序验证领域。本文结合用DISCOVERER寻找秩函数及浮点误差分析方法，提出了分析带循环程序误差的方法。我们的方法利用秩函数估计出了程序最多可能的循环步数，从而可以将带循环的程序展开，看作不带循环的程序来分析。我们还研究了线性程序终止性问题。讨论了在一些特殊情况下，如何改进[36]中提出的算法。我们发现，在这些情况下，计算复杂度可以从指数降低到多项式甚至是线性的。实际应用中这些特殊情况常常发生，因此对这些特殊情况进行的算法改进很有实际意义。