计算机科学 ›› 2018, Vol. 45 ›› Issue (6): 151-155.doi: 10.11896/j.issn.1002-137X.2018.06.026
李轶1,2, 蔡天训1,2, 吴文渊2
LI Yi1,2, CAI Tian-xun1,2, WU Wen-yuan2
摘要： 循环程序的终止性是确保循环程序完全正确的必要条件。如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Anx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。
中图分类号:
| [1]COLN M,SIPMA H.Synthesis of Linear Ranking Functions[C]//International Conf+Y63erence on Tools and Algorithms for the Construction and Analysis of Systems.Springer Berlin Heidelberg,2001:67-81. [2]COLÓN M,SIPMA H.Practical Methods for Proving Program Termination[C]//International Conference on Computer Aided Verification.Springer Berlin Heidelberg,2002:442-454. [3]PODELSKI A,RYBALCHENKO A.A Complete Method for the Synthesis of Linear Ranking Functions[C]//International Workshop on Verification,Model Checking,and Abstract Interpretation.Springer Berlin Heidelberg,2004:239-251. [4]CHEN Y H,XIA B C,YANG L,et al.Discovering Non-linear Ranking Functions by Solving Semialgebraic Systems[C]//International Colloquium on Theoretical Aspects of Computing,Springer Berlin Heidelberg,2007:34-49. [5]HEIZMANN M,HOENICKE J,LEIKE J.Linear Ranking for Linear Lasso Programs[C]//International Symposium on Automated Technology for Verification and Analysis.Springer,Cham,2013:365-380. [6]BAGNARA R,MESNARD F.Eventual Linear Ranking Functions[C]//Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming.Madrid,Spain,ACM,2013:229-238. [7]LI Y,ZHU G,FENG Y.The L-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops[C]//2016 10th International Symposium on Theoretical Aspects of Software Engineering.Shanghai,2016 :30-37. [8]LEIKE J,HEIZMANN M.Ranking Templates for Linear Loops[C]//Tools and Algorithms for the Construction and Analysis of Systems,Springer Berlin Heidelberg,2014:172-186. [9]BEN-AMRAM A M,GENAIM S.On the Linear Ranking Problem for Integer Linear-constraint Loops[C]//Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(POPL’13).Rome,Italy,ACM,2013:51-62. [10]TIWARI A.Termination of Linear Programs[C]//16th International Conference on Computer Aided Verification.Springer Berlin Heideiberg,2004:70-82. [11]BRAVERMAN M.Termination of integer linear programs[C]//Proceedings of the 18th International conference on Computer Aided Verification.Springer-Verlag,2006:372-385. [12]XIA B C,ZHANG Z H.Termination of linear programs with nonlinear constraints[J].Journal of Symbolic Computation,2010,45(11):1234-1249. [13]LI Y.Termination of Single-Path Polynomial Loop Programs[C]//International Colloquium on Theoretical Aspects of Computing.2016:33-50. [14]CHEN C B,MAZA M M.Quantifier Elimination by Cylindrical Algebraic Decomposition Based on Regular Chains[C]//Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation.ACM,2014:91-98. |
| [1] | 朱广,李轶,吴文渊. 计算最终线性秩函数的新方法 New Method for Computing Eventual Linear Ranking Functions 计算机科学, 2017, 44(1): 194-198. https://doi.org/10.11896/j.issn.1002-137X.2017.01.037 |
|
||
首页