Computer Engineering & Science >
Detection Techniques of Program Invariants
Received date: 2010-03-11
Revised date: 2010-06-23
Online published: 2011-03-25
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.
LIU Shukun 1,YANG Xiaohua2 . Detection Techniques of Program Invariants[J]. Computer Engineering & Science, 2011 , 33(3) : 108 -112 . DOI: 10.3969/j.issn.1007130X.2011.
［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.
/
| 〈 |
|
〉 |