线性程序的Ranking函数自动合成

摘要：

针对判定一个程序终止性的经典方法Ranking函数法,运用半代数系统的概念,把程序终止性问题转换为求半代数系统的Ranking函数.然后运用符号计算工具DISCOV-ERER和Farkas引理,求出函数参数存在的充分必要条件,并根据符号计算理论的方法自动合成Ranking函数.通过计算代数理论的证明和试验的验证,并与其他方法做了比较,这种方法是高效合理的.

关键词：DISCOVERER、Farkas’lemma、Ranking函数、半代数系统、程序终止性、程序验证

所属期刊栏目：41

分类号：TP301(计算技术、计算机技术)

资助基金：国家科委973资助项目2004CB318003;中国科学院知识创新重要方向项目KJCX2-YW-S02;国家自然科学基金资助项目107712Q5;国家自然科学基金资助项目90718041

在线出版日期：2017-01-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：176-181