基于迭代轨迹划分的单分支循环程序终止性分析  

Termination Analysis of Single Path Loop Programs Based on Iterative Trajectory Division

作　　者：王垚 李轶[1] WANG Yao;LI Yi(Chongqing Key Laboratory of Automated Reasoning and Cognition,CIGIT,CAS,Chongqing 400714,China;Chongqing School,University of Chinese Academy of Sciences,Chongqing 400714,China)

机构地区：[1]中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室,重庆400714 [2]中国科学院大学重庆学院,重庆400714

出　　处：《计算机科学》2023年第9期108-116,共9页Computer Science

基　　金：国家自然科学基金(61572024,11771421,61103110);重庆市自然科学基金(cstc2019jcyj-msxmX0638);重庆市院士专项(cstc2018jcyjyszxX0002,cstc2019yszx-jcyjX0003);国家重点研发计划(2020YFA07123000);中国科学院“西部之光”。

摘　　要：秩函数作为循环程序终止性分析的重要方法已得到广泛研究。文中着重研究了单分支循环的终止性。首先提出了双向迭代循环概念,将单分支循环分为双向迭代循环和非双向迭代循环。其次,针对双向迭代循环程序,建立了一种划分思路,提出了三段式秩函数的概念,并证明了若该双向迭代循环存在三段式秩函数,则其是终止的。而对非双向迭代循环,引用增函数的划分思路,即利用增函数将原程序空间划分为更小的空间,并通过计算更小空间上的秩函数来证明原程序的终止性。最后,将三段式秩函数的计算问题归结为SVM分类问题,并利用工具Z3或bottema对由SVM所得的候选秩函数进行验证。The ranking function has been extensively studied as an important method of program termination analysis.In this paper,we focus on the termination of single-path loops.Firstly,the concept of two-way iterative loops is proposed,and the single-path loops are divided into bidirectional iterative loops and non-bidirectional iterative loops.Secondly,for the bidirectional iterative loop program,a division method and concept of trivial ranking function are proposed,and it is proved that if a bidirectional iterative loop exists a trivial rank function,it is terminated.As for the non-bidirectional iterative loop,we use incremental function as the division method,i.e.,the original program space is divided into smaller spaces by using incremental function,and the termination of the original program is proved by computing the ranking function on the smaller space.Finally,the problem of computing the trivial ranking function comes down to the SVM classification problem,and we verifies candidate ran-king functions using the tools Z3 or bottema.

关 键 词：程序验证 秩函数 机器学习 程序终止性 

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