程序不变量检测技术  

Detection Techniques of Program Invariants

作　　者：刘树锟[1] 阳小华[2] 

机构地区：[1]湖南涉外经济学院计算机科学与技术学部,湖南长沙410205 [2]南华大学计算机科学与技术学院,湖南衡阳421001

出　　处：《计算机工程与科学》2011年第3期108-112,共5页Computer Engineering & Science

基　　金：湖南省教育厅基金资助项目(08C516);湖南省自然科学基金资助项目(05JJ30117)

摘　　要：基于合约的程序设计是提高软件质量的一种重要技术,已经得到了很大的发展。合约描述了程序内部的基本属性、程序良性运行的保证条件以及运行后的期望结果。作为合约的一种表达形式,程序不变量一般包含类不变量、前置条件和后置条件。程序不变量是程序中隐含的属性,它可以应用于程序验证、软件测试技术、逆向工程、程序质量保证等领域。本文结合当前主流的程序不变量研究的相关成果和基于合约的程序不变量程序设计方法,分别从源程序编配技术、测试用例生成技术、程序运行轨迹收集技术和程序不变量分析技术四个方面,对程序不变量挖掘的关键方法和原理进行了详细的剖析。Design by contract is an important technology which can be used to improve software quality. Contract can express the basic properties which are invisible to the users and the conditions used to guarantee the correct results of programs. Program invariant is a kind of contract including class invariants, pre-conditions invariants and post-conditions invariants. The program invariants can be applied to the range of program verification and software test. In this paper, the current mainstream research technology of detecting program invariants is described and the main process and key methods of discovering the invariants are shown.

关 键 词：程序不变量 检测技术 程序编配 运行追踪 

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