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

Automatic Synthesis of Linear Program Ranking Functions

作　　者：李骏[1] 李轶[1] 冯勇[1,2] 秦小林[1] 

机构地区：[1]中国科学院成都计算机应用研究所,四川成都610041 [2]电子科技大学计算机推理与可信计算实验室,四川成都610054

出　　处：《四川大学学报（工程科学版）》2009年第5期176-181,共6页Journal of Sichuan University (Engineering Science Edition)

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

摘　　要：针对判定一个程序终止性的经典方法Ranking函数法,运用半代数系统的概念,把程序终止性问题转换为求半代数系统的Ranking函数。然后运用符号计算工具DISCOV-ERER和Farkas引理,求出函数参数存在的充分必要条件,并根据符号计算理论的方法自动合成Ranking函数。通过计算代数理论的证明和试验的验证,并与其他方法做了比较,这种方法是高效合理的。To determine the classical ranking functions of program verification,a new approach was proposed based on the theory of semi-algebraic systems.It automatically converted the problem of program verification to solve the ranking function of semi-algebraic systems.The sufficient and necessary conditions of parameters in ranking functions could be obtained using symbolic computation tool,DISCOVERER and Farkas' Lemma,and then the novel ranking function was automatically synthesized by symbolic computations.The c...

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

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]