线性C循环代码的终止性分析及其工具开发

发布时间：2020-07-11 09:58

【摘要】：循环程序的终止性分析是程序验证的重要组成部分。确保循环程序的终止是循环程序完全正确的必要条件。目前,用来证明程序终止性的主流方法是通过合成秩函数的方法来证明。秩函数是一个关于循环变量的函数,其值域是一个良基集,它的函数值随着循环体的执行持续减小。本文给出了如何通过合成复杂秩函数的方法来证明循环程序的终止性,并介绍了循环程序终止性自动验证工具TermChecker。目前合成秩函数的主要方法是通过设定秩函数模板,然后求解模板参数来完成的。传统定义的秩函数要求循环的每次迭代都使得函数值都减小,这种较强的约束往往使得模板参数无解,这严重限制了通过合成秩函数来证明循环程序的终止。因此,在本文中,首先将传统秩函数的概念进行了推广,提出了k阶秩函数的概念,并通过合成k阶秩函数来证明单分支线性赋值循环程序的终止性。传统的秩函数只是k阶秩函数的一种特殊情况。针对多分支循环程序的终止性的证明,传统的方法是通过合成字典序秩函数或者全局秩函数来证明的。但是,多分支循环程序存在字典序秩函数或者全局秩函数只是对应多分支循环程序终止的充分条件,而非必要条件。因此,为了进一步扩大秩函数的适用范围,本文提出了一个多分支线性赋值循环程序终止的充分标准。该标准通过合成多分支线性赋值循环程序的局部秩函数来证明对应循环程序的终止性。实验结果表明针对某些终止的多分支线性赋值循环程序,不能通过合成字典序秩函数或者全局秩函数来证明它的终止,但是可以通过合成局部秩函数来证明。为了实现循环程序终止性的自动验证,开发了工具TermChecker。该工具可以实现C语言编写的循环程序片段的终止性自动分析工作。软件首先对输入的循环程序进行词法分析、语法分析,然后提取出循环信息并将其传给服务器端。服务器端的循环程序终止性分析算法使用符号计算软件Maple编写,该算法供服务器端的C程序调用对循环信息进行分析,然后将分析结果返回给客户端。最后客户端显示分析结果。
【学位授予单位】：重庆邮电大学
【学位级别】：硕士
【学位授予年份】：2018
【分类号】：TP312.1;TP311.53
【图文】：

加载,符号计算,量词

在符号计算领域发展多年，有许多高效的函数可以供调用，这将极大的方便我们的计算推导过程。Mathematica 本来兼具符号计算和数值计算，但是其符号计算的能力和函数库的丰富程度还有所欠缺，因此我们不选用该计算软件。RegularChains 是Maple 的一个包，可以在 Maple 下加载调用。其中包含了许多子包和函数，可用于求解多项式等式、不等式和符号不等式系统。其中的命令 QuantifierElimination 可用于量词消去。本章我们利用 RegularChains 中的函数进行秩函数的合成计算。下面，通过一个实例来介绍 RegularChains 的使用。对于如下所示的量词公式 x , y ( x 1 x 9 y x 0 y 0 ax by c 0)表示对于任意的 x,y, 当x 1 x 9 y x 0 y 0时，可以推出 ax by c 0，其中 a，b，c 是参数。为方便讨论，我们令 f ax by c，接下来，我们通过 RegularChains 来演示如何求出一组合适的 a，b，c 来满足上述的量词公式。

加载,循环程序,硕士学位论文,分支线

重庆邮电大学硕士学位论文第 2 章单分支线性赋值循环程序的终止性分析如图 2.1 所示，首先需要指定 RegularChains 的路径参数 libname，这是因为目前 Maple 中自带的 RegularChains 包中还没有将最新的量词消去函数QuantifierElimination 包含进去，因此本文中计算所需的 RegularChains 包需要到http://www.regularchains.org/downloads.html 去下载最新版本，然后将其放在 E 盘下面，通过 libname 参数来指定加载。然后我们依次加载 RegularChains 和SemiAlgebraicSetTools.

实例图,实例,存在量词,约束条件

图 2.2 使用 QuantifierElimination 命令进行量词消去首先输入量词公式 x , y ( x 1 x 9 y x 0 y 0 ax by c 0)并命名为 p1，然后使用 QuantifierElimination 命令消去 x,y 得到 a，b，c 的约束条件，并将该约束条件命名为 t1.接下来需要判断是否存在 a，b，c 满足约束 t1，将该存在量词公式命名为 p2，再一次调用 QuantifierElimination 进行判断，得到 true 即表明约束t1 是有解的。

【参考文献】