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