循环程序的界函数合成

doi:10.11772/j.issn.1001-9081.2021020221

《计算机应用》唯一官方网站 ›› 2022, Vol. 42 ›› Issue (2): 565-573.DOI: 10.11772/j.issn.1001-9081.2021020221

• 计算机软件技术 • 上一篇

循环程序的界函数合成

谭旺¹^,², 李轶¹()

^1.中国科学院重庆绿色智能技术研究院, 重庆 400714
^2.中国科学院大学计算机科学与技术学院, 北京 101408

收稿日期:2021-02-05 修回日期:2021-04-12 接受日期:2021-04-13 发布日期:2021-05-10 出版日期:2022-02-10
通讯作者: 李轶
作者简介:谭旺（1995—），男，重庆人，硕士研究生，主要研究方向：循环程序终止性验证、机器学习；
李轶（1980—），男，重庆人，副研究员，博士，CCF会员，主要研究方向：程序验证、计算机代数。
基金资助:
国家自然科学基金资助项目(11771421);中国科学院“西部之光”;国家重点研发计划项目(2020YFA07123000);重庆市自然科学基金资助项目(cstc2019jcyj-msxmX0638)

Synthesis of loop bound functions for loop programs

Wang TAN¹^,², Yi LI¹()

^1.Chongqing Institute of Green and Intelligent Technology，Chinese Academy of Sciences，Chongqing 400714，China
^2.School of Computer Science and Technology，University of Chinese Academy of Sciences，Beijing 101408，China

Received:2021-02-05 Revised:2021-04-12 Accepted:2021-04-13 Online:2021-05-10 Published:2022-02-10
Contact: Yi LI
About author:TAN Wang， born in 1995， M. S. candidate. His research interests include， termination verification for loop programs， machine learning.
LI Yi， born in 1980， Ph. D.， research associate. His research interests include program verification， computer algebra.
Supported by:
National Natural Science Foundation of China(11771421);Chinese Academy of Sciences “Light of the West”, National Key Research and Development Program of China(2020YFA07123000);Natural Science Foundation of Chongqing(cstc2019jcyj-msxmX0638)

摘要/Abstract

摘要：

作为循环程序终止性分析的主流方法，当前的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数，现有秩函数方法就无法证明其终止性的问题，提出一个新的方法来合成给定循环程序对应的界函数。对于给定的循环程序，倘若能找到其界函数，则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题，并在选定界函数模板后，根据模板建立映射关系以构建训练集；然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解得到模板系数，从而得到候选的界函数；最后利用现有的符号验证工具Redlog对该候选界函数进行验证。实验结果表明，相较于现有的秩函数方法，所提方法不仅能够应用于更多的循环程序，而且所得界函数在形式上相较于秩函数更加简化。具体表现为，对于某些没有线性秩函数的循环，该方法可以得到其对应的线性界函数；同时，对于某些只有多阶段线性秩函数的循环，该方法可以求解得到全局的线性界函数。

关键词: 程序验证, 循环程序终止性, 支持向量机, 界函数, 秩函数

Abstract:

As the mainstream methods of loop program termination analysis，most existing ranking function methods are limited to the solution of linear or polynomial ranking functions. Concerning that the existing ranking function methods cannot prove the termination if there are no corresponding linear or polynomial ranking functions for the loop programs， a new method was proposed to synthesize the loop bound function for the given loop program. The existence of loop bound function of a given loop program implies the termination of this loop function. Firstly， the problem of solving the loop bound functions was transformed into a linear binary classification problem. Once the function’s template was selected， the mapping relationship was established according to the template to construct the training set. After that， the obtained training set was used to obtain the classification hyperplane through Support Vector Machine （SVM） to find the template coefficients， thereby obtaining the candidate loop bound function. Finally， the existing symbol verification tool Redlog was used to verify this candidate loop bound function. Experimental results show that compared with the existing ranking function methods， the proposed method not only can be applied to more loop programs， but also has the obtained loop bound functions more simplified in form than the ranking functions. Specifically， for some loops without linear ranking functions， the corresponding linear loop bound functions can be solved by the proposed method； at the same time， for some loops with only multiphase linear ranking functions， the global linear loop bound functions can be solved by the proposed method.

Key words: program verification, loop program termination, Support Vector Machine (SVM), loop bound function, ranking function

中图分类号:

TP311

谭旺, 李轶. 循环程序的界函数合成[J]. 计算机应用, 2022, 42(2): 565-573.

Wang TAN, Yi LI. Synthesis of loop bound functions for loop programs[J]. Journal of Computer Applications, 2022, 42(2): 565-573.

图/表 6

图1 界函数合成框架

Fig. 1 Framework of synthesizing loop bound function

图2 基于SVM的循环程序界函数计算流程

Fig. 2 Flowchart of calculating loop bound function for loop program via SVM

表1 实验所涉及的循环

Tab. 1 Loops for experiments

编号	表达式
1	$w h i l e (a 1! = a 2) d o i f (a 1 > a 2) a 1' = a 1 - a 2; i f (a 2 > a 1) a 2' = a 2 - a 1$
2	$w h i l e (1 < a 1 < 10) d o a 1' = 2 a 1; a 2' = a 2 + 1$
3	$w h i l e (a 22 + 10 ≤ a 1 + 6 a 2, a 12 + 6 ≤ 4 a 1 + a 2) d o a 1' = a 1 + a 2; a 2' = a 2 - 1$
4	$w h i l e (a 1 + a 2 ≥ 1, a 1 ≤ 3, a 22 ≤ 1) d o a 1' = 5 a 1 - a 12; a 2' = a 22 + a 2$
5	$w h i l e (a 1 > a 22 - a 2) d o a 1' = a 1 + a 2 - 5; a 2' = - a 2$
6	$w h i l e (a 1 ≥ a 2, a 2 ≥ 0) d o a 1' = a 1 - 4 a 22 - 4 a 2 + 3; a 2' = a 2 - 2$
7	$w h i l e (a 1 ≥ 0, a 2 ≥ 0) d o a 1' = a 1 - a 2; a 2' = 2 a 2 + 1$
8	$w h i l e (a 1 ≥ 0, a 2 ≥ a 1) d o a 1' = 3 a 1 - a 2; a 2' = 4 a 1 + 2 a 2 + 3$
9	$w h i l e (a 1 ≥ 1, a 1 - a 2 ≥ 1) d o a 1' = a 1 - 2 a 2; a 2' = 2 a 1 + 4 a 2 + 2$
10	$w h i l e (4 a 1 + a 2 ≥ 1) d o a 1' = - 2 a 1 + 4 a 2; a 2' = 4 a 1$

表1 实验所涉及的循环

Tab. 1 Loops for experiments

编号	表达式
1	$w h i l e (a 1! = a 2) d o i f (a 1 > a 2) a 1' = a 1 - a 2; i f (a 2 > a 1) a 2' = a 2 - a 1$
2	$w h i l e (1 < a 1 < 10) d o a 1' = 2 a 1; a 2' = a 2 + 1$
3	$w h i l e (a 22 + 10 ≤ a 1 + 6 a 2, a 12 + 6 ≤ 4 a 1 + a 2) d o a 1' = a 1 + a 2; a 2' = a 2 - 1$
4	$w h i l e (a 1 + a 2 ≥ 1, a 1 ≤ 3, a 22 ≤ 1) d o a 1' = 5 a 1 - a 12; a 2' = a 22 + a 2$
5	$w h i l e (a 1 > a 22 - a 2) d o a 1' = a 1 + a 2 - 5; a 2' = - a 2$
6	$w h i l e (a 1 ≥ a 2, a 2 ≥ 0) d o a 1' = a 1 - 4 a 22 - 4 a 2 + 3; a 2' = a 2 - 2$
7	$w h i l e (a 1 ≥ 0, a 2 ≥ 0) d o a 1' = a 1 - a 2; a 2' = 2 a 2 + 1$
8	$w h i l e (a 1 ≥ 0, a 2 ≥ a 1) d o a 1' = 3 a 1 - a 2; a 2' = 4 a 1 + 2 a 2 + 3$
9	$w h i l e (a 1 ≥ 1, a 1 - a 2 ≥ 1) d o a 1' = a 1 - 2 a 2; a 2' = 2 a 1 + 4 a 2 + 2$
10	$w h i l e (4 a 1 + a 2 ≥ 1) d o a 1' = - 2 a 1 + 4 a 2; a 2' = 4 a 1$

表2 实验参数以及所得模板系数

Tab. 2 Experimental parameters and template coefficients

编号	界函数模板	负类点	模板系数
1	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（2，2，2）
2	$w 1 ⋅ a 1 + w 2$	（10，1）	（10，0）
3	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（1，1，1）
4	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3.34，3.32，1）
5	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，0.5，1）	（2，2，1）
6	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3，5，4）
7	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（2，2，4）
8	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，3，9）
9	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，2，16）
10	$w 1 ⋅ (a 1 + 1) 2 + w 2 ⋅ (a 2 + 1) 2 + w 3$	（0，0，1）	（6，6，25）

表2 实验参数以及所得模板系数

Tab. 2 Experimental parameters and template coefficients

编号	界函数模板	负类点	模板系数
1	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（2，2，2）
2	$w 1 ⋅ a 1 + w 2$	（10，1）	（10，0）
3	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（1，1，1）
4	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3.34，3.32，1）
5	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，0.5，1）	（2，2，1）
6	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（0，0，1）	（3，5，4）
7	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（2，2，4）
8	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，3，9）
9	$w 1 ⋅ a 1 + w 2 ⋅ a 2 + w 3$	（-1，-1，1）	（3，2，16）
10	$w 1 ⋅ (a 1 + 1) 2 + w 2 ⋅ (a 2 + 1) 2 + w 3$	（0，0，1）	（6，6，25）

表3 不同方法的可行性对比

Tab. 3 Feasibility comparison of different methods

编号	基于QE 秩函数合成	基于SVM 秩函数合成	多阶段线性秩函数合成	本文方法
1	成功	成功	失败	成功
2	成功	成功	成功	成功
3	失败	成功	失败	成功
4	失败	成功	失败	成功
5	失败	成功	失败	成功
6	失败	成功	失败	成功
7	失败	失败	成功	成功
8	失败	失败	成功	成功
9	失败	失败	成功	成功
10	失败	失败	失败	成功

表4 实验所得函数形式结果对比

Tab. 4 Comparison of experimental results in functional forms

编号	基于QE 秩函数合成	基于SVM 秩函数合成	多阶段线性秩函数合成	本文方法
1	线性	线性	无法合成	线性
2	线性	线性	线性	线性
3	无法合成	线性	无法合成	线性
4	无法合成	线性	无法合成	线性
5	无法合成	非线性	无法合成	线性
6	无法合成	非线性	无法合成	线性
7	无法合成	无法合成	多阶段线性	线性
8	无法合成	无法合成	多阶段线性	线性
9	无法合成	无法合成	多阶段线性	线性
10	无法合成	无法合成	无法合成	非线性

参考文献 32

1	COUSOT P， COUSOT R. An abstract interpretation framework for termination ［C］// Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2012： 245-258. 10.1145/2103656.2103687
2	LEE S C， JONES N D， BEN-AMRAM A M. The size-change principle for program termination ［C］// Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2001： 81-92. 10.1145/360204.360210
3	LEIKE J， HEIZMANN M. Geometric nontermination arguments ［C］// Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems， LNCS10806. Cham： Springer， 2018： 266-283.
4	BRAVERMAN M. Termination of integer linear programs ［C］// Proceedings of the 2006 International Conference on Computer Aided Verification， LNCS4144. Berlin： Springer， 2006： 372-385.
5	TIWARI A. Termination of linear programs ［C］// Proceedings of the 2004 International Conference on Computer Aided Verification， LNCS3114. Berlin： Springer， 2004： 70-82.
6	TURING A M. On computable numbers， with an application to the Entscheidungsproblem［J］. Proceedings of the London Mathematical Society， 1937， s2-41（1）： 230-265. 10.1112/plms/s2-42.1.230
7	CHEN Y F， HEIZMANN M， LENGÁL O， et al. Advanced automata-based algorithms for program termination checking ［C］// Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York： ACM， 2018： 135-150. 10.1145/3192366.3192405
8	FEDYUKOVICH G， ZHANG Y L， GUPTA A. Syntax-guided termination analysis ［C］// Proceedings of the 2018 International Conference on Computer Aided Verification， LNCS10981. Cham： Springer， 2018： 124-143.
9	LI Y. Witness to non-termination of linear programs［J］. Theoretical Computer Science， 2017， 681： 75-100. 10.1016/j.tcs.2017.03.036
10	BAGNARA R， MESNARD F. Eventual linear ranking functions ［C］// Proceedings of the 15th International Symposium on Principles and Practice of Declarative Programming. New York： ACM， 2013： 229-238. 10.1145/2505879.2505884
11	BEN-AMRAM A M， GENAIM S. Ranking functions for linear-constraint loops［J］. Journal of the ACM， 2014， 61（4）： No.26. 10.1145/2629488
12	BEN-AMRAM A M， GENAIM S. On multiphase-linear ranking functions ［C］// Proceedings of the 2017 International Conference on Computer Aided Verification， LNCS10427. Cham： Springer， 2017： 601-620.
13	LEIKE J， HEIZMANN M. Ranking templates for linear loops ［C］// Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems， LNCS8413. Berlin： Springer， 2014： 172-186. 10.2168/lmcs-11(1:16)2015
14	LI Y， ZHU G， FENG Y. The l-depth eventual linear ranking functions for single-path linear constraint loops ［C］// Proceedings of the 10th International Symposium on Theoretical Aspects of Software Engineering. Piscataway： IEEE， 2016： 30-37. 10.1109/tase.2016.8
15	CHEN Y H， XIA B C， YANG L， et al. Discovering non-linear ranking functions by solving semi-algebraic systems ［C］// Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing， LNCS4711. Berlin： Springer， 2007： 34-49.
16	SHEN L Y， WU M， YANG Z F， et al. Generating exact nonlinear ranking functions by symbolic-numeric hybrid method［J］. Journal of Systems Science and Complexity， 2013， 26（2）： 291-301. 10.1007/s11424-013-1004-1
17	YUAN Y， LI Y. Ranking function detection via SVM： a more general method［J］. IEEE Access， 2019， 7： 9971-9979. 10.1109/access.2018.2890692
18	KOVÁCS L. Automated invariant generation by algebraic techniques for imperative program verification in Theorema［D］. Linz： Johannes Kepler University Linz， 2007： 43-75.
19	GULWANI S， JAIN S， KOSKINEN E. Control-flow refinement and progress invariants for bound analysis ［C］// Proceedings of the 30th ACM SIGPLAN Conference on Programming Languages Design and Implementation. New York： ACM， 2009： 375-385. 10.1145/1542476.1542518
20	GULWANI S， MEHRA K K， CHILIMBI T. SPEED： precise and efficient static estimation of program computational complexity ［C］// Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2009： 127-139. 10.1145/1594834.1480898
21	NORI A V， SHARMA R. Termination proofs from tests ［C］// Proceedings of the 9th Joint Meeting on Foundations of Software Engineering. New York： ACM， 2013： 246-256. 10.1145/2491411.2491413
22	邢建英.程序验证关键技术研究［D］.长沙：国防科学技术大学， 2011： 63-75.
	XING J Y. Study on program verification［D］. Changsha： National University of Defense Technology， 2011： 63-75.
23	BERDINE J， CHAWDHARY A， COOK B， et al. Variance analyses from invariance analyses ［C］// Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York： ACM， 2007： 211-224. 10.1145/1190216.1190249
24	CHAWDHARY A， COOK B， GULWANI S， et al. Ranking abstractions ［C］// Proceedings of the 2008 International Conference on European Symposium on Programming. Cham： Springer， 2008： 148-162. 10.1007/978-3-540-78739-6_13
25	TSITOVICH A， SHARYGINA N， WINTERSTEIGER C M， et al. Loop summarization and termination analysis ［C］// Proceedings of the 2011 International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Cham： Springer， 2011： 81-95. 10.1007/978-3-642-19835-9_9
26	KROENING D， SHARYGINA N， TSITOVICH A， et al. Termination analysis with compositional transition invariants ［C］// Proceedings of the 2010 International Conference on Computer Aided Verification， LNCS6174. Berlin： Springer， 2010： 89-103.
27	PODELSKI A， RYBALCHENKO A. Transition invariants ［C］// Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science. Piscataway： IEEE， 2004： 32-41. 10.1109/lics.2004.1319598
28	PEDREGOSA F， VAROQUAUX G， GRAMFORT A， et al. Scikit-learn： machine learning in Python［J］. Journal of Machine Learning Research， 2011， 12： 2825-2830. 10.3389/fninf.2014.00014
29	GULWANI S. SPEED： symbolic complexity bound analysis ［C］// Proceedings of the 2009 International Conference on Computer Aided Verification， LNCS5643. Berlin： Springer， 2009： 51-62.
30	VAPNIK V N， CHERVONENKIS A Y. A note on one class of perceptrons［J］. Automation and Remote Control， 1964， 25（1）： 103-109.
31	VAPNIK V N. Statistical learning theory［J］. Encyclopedia of the Sciences of Learning， 1998， 41（4）： 3185-3185.
32	周志华.机器学习［M］.北京：清华大学出版社， 2016： 121-124. 10.21436/inbom.12382432
	ZHOU Z H. Machine Learning［M］. Beijing： Tsinghua University Press， 2016： 121-124. 10.21436/inbom.12382432

[1]	祁祥洲, 邢红杰. 基于中心核对齐的多核单类支持向量机[J]. 《计算机应用》唯一官方网站, 2022, 42(2): 349-356.
[2]	贾洪飞, 刘茜, 王瑜, 肖洪兵, 邢素霞. 3DPCANet在阿尔茨海默症功能磁共振成像图像分类中的应用[J]. 《计算机应用》唯一官方网站, 2022, 42(1): 310-315.
[3]	贾鹤鸣, 姜子超, 李瑶, 孙康健. 基于改进斑点鬣狗优化算法的同步优化特征选择[J]. 计算机应用, 2021, 41(5): 1290-1298.
[4]	袁芊芊, 邓洪敏, 王晓航. 基于超像素快速模糊C均值聚类与支持向量机的柑橘病虫害区域分割[J]. 计算机应用, 2021, 41(2): 563-570.
[5]	曹鸿亮, 张莹, 武斌, 李繁菀, 那绪博. 基于迁移成分分析和支持向量机的肝移植并发症预测方法[J]. 《计算机应用》唯一官方网站, 2021, 41(12): 3608-3613.
[6]	李凯, 李洁. 基于pinball损失的结构模糊多分类支持向量机算法[J]. 《计算机应用》唯一官方网站, 2021, 41(11): 3104-3112.
[7]	陆荣秀, 陈明明, 杨辉, 朱建勇. 基于溶液图像时序特征的元素组分含量动态监测系统[J]. 计算机应用, 2021, 41(10): 3075-3081.
[8]	童林, 官铮. 改进鲸鱼优化支持向量机的交通流量模糊粒化预测[J]. 计算机应用, 2021, 41(10): 2919-2927.
[9]	张健铭, 施元昊, 徐正蓺, 魏建明. 基于误差预测的自适应UWB/PDR融合定位算法[J]. 计算机应用, 2020, 40(6): 1755-1762.
[10]	王杨, 赵红东. 基于改进粒子群优化的支持向量机与情景感知的人体活动识别[J]. 计算机应用, 2020, 40(3): 665-671.
[11]	黄功, 赵永平, 谢云龙. 基于局部密度的加权一类支持向量机算法及其在涡轴发动机故障检测中的应用[J]. 计算机应用, 2020, 40(3): 917-924.
[12]	赵一, 段兴, 谢仕义, 梁春林. 面向特定目标自识别的交通图像语义检索方法[J]. 《计算机应用》唯一官方网站, 2020, 40(2): 553-560.
[13]	李卉, 杨志霞. 基于Rescaled Hinge损失函数的多子支持向量机[J]. 计算机应用, 2020, 40(11): 3139-3145.
[14]	牛晓可, 黄伊鑫, 徐华兴, 蒋震阳. 基于听皮层神经元感受野的强噪声环境下说话人识别[J]. 计算机应用, 2020, 40(10): 3034-3040.
[15]	白东颖, 易亚星, 王庆超, 余志勇. 面向概念漂移问题的渐进多核学习方法[J]. 计算机应用, 2019, 39(9): 2494-2498.

循环程序的界函数合成

Synthesis of loop bound functions for loop programs

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 6

参考文献 32

相关文章 15

编辑推荐

Metrics