| 摘要: |
| 计算程序中循环的程序复杂度符号化上界可以验证程序的停机性.基于差分方程和最优化问题求解技术,给出了一种计算P*-solvable 循环程序复杂度符号化上界的有效方法.分别针对含有赋值语句的循环和带条件分支的循环,提出了其程序复杂度符号化上界计算方法.与其他工作相比,该方法能够计算得到更精确的循环复杂度符号化上界,实验结果证明了该方法的有效性. |
| 关键词: 差分方程 最优化问题 程序停机 复杂度上界 闭合形式解 |
| DOI：10.3724/SP.J.1001.2011.03898 |
| 分类号: |
| 基金项目:国家自然科学基金(60703075, 60973105, 90718017); 国家教育部博士点专项基金(20070006055) |
|
| Computing Symbolic Complexity Bounds of Loops by Recurrence Solution |
|
XING Jian-Ying1, LI Meng-Jun1, LI Zhou-Jun2
|
|
1.College of Computer, National University of Defense Technology, Changsha 410073, China;2.School of Computer Science and Engineering, BeiHang University, Beijing 100191, China
|
| Abstract: |
| Computing symbolic complexity bounds of loops can prove program’s termination. Based on the solving techniques of recurrence equations and optimization problems, this paper presents a practical approach for computing complexity bounds of loops called P*-solvable loops. Two algorithms are given for loops with assignments only and loops with conditional branches respectively. Compared with some other works, this approach can attain more complexity bounds of loops. The experimental results demonstrate the practicality of this approach. |
| Key words: recurrence equation optimization problem program termination complexity bound closed form solution |
