• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

J4 ›› 2011, Vol. 33 ›› Issue (3): 108-112.doi: 10.3969/j.issn.1007130X.2011.

• 论文 • 上一篇    下一篇

程序不变量检测技术

刘树锟1,阳小华2   

  1. (1.湖南涉外经济学院计算机科学与技术学部,湖南 长沙 410205;
    2.南华大学计算机科学与技术学院,湖南 衡阳 421001)
  • 收稿日期:2010-03-11 修回日期:2010-06-23 出版日期:2011-03-25 发布日期:2011-03-25
  • 作者简介:刘树锟(1979),男,河北南皮人,硕士,讲师,CCF会员(E200013072M),研究方向为软件工程和数据库技术。阳小华(1963),男,湖南衡阳人,博士,教授,研究方向为软件工程、数据库技术和信息检索技术。
  • 基金资助:

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

Detection Techniques of Program Invariants

LIU Shukun 1,YANG Xiaohua2   

  1. (1.Department of Computer Science and Technology,Hunan International Economics University,Changsha 410205;
    2.School of Computer Science and Technology,University of South China,Hengyang 421001,China )
  • Received:2010-03-11 Revised:2010-06-23 Online:2011-03-25 Published:2011-03-25

摘要:

基于合约的程序设计是提高软件质量的一种重要技术,已经得到了很大的发展。合约描述了程序内部的基本属性、程序良性运行的保证条件以及运行后的期望结果。作为合约的一种表达形式,程序不变量一般包含类不变量、前置条件和后置条件。程序不变量是程序中隐含的属性,它可以应用于程序验证、软件测试技术、逆向工程、程序质量保证等领域。本文结合当前主流的程序不变量研究的相关成果和基于合约的程序不变量程序设计方法,分别从源程序编配技术、测试用例生成技术、程序运行轨迹收集技术和程序不变量分析技术四个方面,对程序不变量挖掘的关键方法和原理进行了详细的剖析。

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

Abstract:

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.

Key words: program invariant;detection technology;program instrument;running trace