程序不变量检测技术
收稿日期: 2010-03-11
修回日期: 2010-06-23
网络出版日期: 2011-03-25
基金资助
湖南省教育厅基金资助项目（08C516）；湖南省自然科学基金资助项目（05JJ30117）
Detection Techniques of Program Invariants
Received date: 2010-03-11
Revised date: 2010-06-23
Online published: 2011-03-25
刘树锟1,阳小华2 . 程序不变量检测技术[J]. 计算机工程与科学, 2011 , 33(3) : 108 -112 . DOI: 10.3969/j.issn.1007130X.2011.
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, preconditions invariants and postconditions 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.
［1］Mitchell R,Mckim J,孟岩. Design by Contract 原则与实践［M］.北京:人民邮电出版社,2003.
［2］Yang J,Evans D,Bhardwai D,et al.Perracotta: Mining Temporal API Rules from Imperfect traces［C］∥Proc of ICSE’06,2006：282291.
［3］Saff D, Artzi S, Perkins J.H ,et al. Automatic Test Factoring for Java［C］∥Proc of the 21st Annual Int’l Conference on Automated Software Engineering, 2005:114123.
［4］Ernst M D. Dynamically Discovering Likely Program Invariants:［Ph D Dissertation］［D］.Department of Computer Science and Engineering, University of Washington,2000.
［5］Braberman V, Fernández F,Garbervetsky D,et al.Parametric Prediction of Heap Memory Requirements［C］∥Proc of Int’l Symp on Memory Management, 2008:141150.
［6］Lorenzoli D, Mariani L, Pezzè M. Automatic Generation of Software Behavioral Models［C］∥Proc of the 30th Int’l Conf on Software Engineering,2008:501510.
［7］Ernst M D, Perkins J H, Guo P J. The Daikon System for Dynamic Detection of Likely Invariants［J］. Science of Computer Programming, 2007, 69(3):3545.
/
| 〈 |
|
〉 |