| 基于抽象解释的函数不变量正确性验证 |
| |
| 引用本文： | 武书彦,苏青琴,刘久富. 基于抽象解释的函数不变量正确性验证[J]. 微电子学与计算机, 2012, 29(10): 161-165 |
| |
| 作者姓名： | 武书彦 苏青琴 刘久富 |
| |
| 作者单位： | 1. 郑州牧业工程高等专科学校信息工程系,河南郑州,450011
2. 南京航空航天大学自动化学院,江苏南京,210016 |
| |
| 摘 要： | 函数不变量检测是提高软件质量的一种有效方法.针对检测方法可能带来无效的函数不变量的缺陷,提出一种以抽象解释理论为基础的函数不变量的正确性验证方法.首先将函数不变量转化成多项式关系;其次结合多项式程序与最弱前置条件抽象解释分析多项式关系正确性的判断依据;最后构造多项式关系算法,凭借得到的结果验证函数不变量正确与否.同时通过一个C程序中的函数不变量为例对该验证方法进行说明.
|
| 关 键 词： | 函数不变量 抽象解释 正确性验证 多项式关系 |
Abstract Interpretation Based Correct Verification for Functional Invariant |
| |
| WU Shu-yan,SU Qing-qin,LIU Jiu-fu. Abstract Interpretation Based Correct Verification for Functional Invariant[J]. Microelectronics & Computer, 2012, 29(10): 161-165 |
| |
| Authors: | WU Shu-yan SU Qing-qin LIU Jiu-fu |
| |
| Affiliation: | 1College of Information Engineering,Zhengzhou Animal Husbandry Engineering,Zhengzhou 450011,China 2College of Automation,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China) |
| |
| Abstract: | The discovery of function invariant is an effective method for improving software quality.As the detecting may contain invalid invariant defects,this paper proposes an abstract interpretation based correct verification for functional invariant.Firstly functional invariants transfer to polynomial relations.Secondly we abstract analysis the foundation of the correctness of polynomial relations with polynomial program and the weakest precondition.Finally we construct polynomial algorithm and verify the function invariant is correct or not with the results obtained.As the same time we state this verification with functional invariant of an C program. |
| |
| Keywords: | functional invariant abstract interpretation correct verification~ polynomial relations |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
