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

摘要

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