计算机应用

作者：袁月, 李轶

单位：1. 中国人民大学 信息学院, 北京 100010;2. 自动推理与认知重庆市重点实验室(中国科学院 重庆绿色智能技术研究院), 重庆 401120

关键词：循环程序终止性,多项式循环程序,多项式秩函数,多阶段秩函数,Dixon结式,逐次差分代换

基金：国家自然科学基金资助项目（61472429，61572024，61103110）。

秩函数探测是循环程序终止性分析的重要方法，目前，已有很多研究者致力于为线性循环程序探测对应的线性秩函数，然而，针对具有多项式循环条件和多项式赋值的多项式型的循环，现有的秩函数探测方法还有所不足，解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题，基于扩展Dixon结式（KSY方法）和逐次差分代换（SDS）方法，提出一种为多项式循环程序探测多项式型秩函数的方法。首先，将待探测的秩函数模板看作带参数系数的多项式，将秩函数的探测转换为寻找满足条件的参数系数的问题；然后，进一步将问题转换为判定相应的方程组是否有解的问题，至此，利用KSY方法中的扩展的Dixon结式，将问题更进一步简化为带参系数多项式（即结式）严格为正的判定问题；最后，利用SDS方法，找到一个充分条件，使得得到的结式严格为正，此时，可以获取满足条件的参数系数的取值，从而找到一个满足条件的秩函数，通过实验验证该秩函数探测方法的有效性。实验结果表明，利用该方法，可以有效地为多项式循环程序找到多项式秩函数，包括深度为d的多阶段多项式秩函数，与已有方法相比，该方法能够更高效地找到多项式秩函数，对于基于柱形代数分解（CAD）方法的探测方法因时间复杂度问题无法而应对的一些循环，利用所提方法能够在几秒内为这些循环找到秩函数。

来源：2019年第7期

《计算机应用》期刊编辑部

查看计算机应用杂志2019年第7期