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