Dynamically Discovering Functional Likely Program Invariants Based on Relational Database Theory

Dynamic likely program invariant detection technology is an available instrument for discovering contract from large program in non-formal description. It is of benefit to contract technology exerting more influence on program quality assurance. Since the research of invariant detection technology has just started that the rough detection usually use hypothesis verification approach which relies on the experience of the detector and his degree of understanding of the detected program so that there is serious lack of accuracy and efficiency. This paper tempts to divide the invariants into two kinds that one is called functional invariant and the other is non-functional type based on relational data theory before starting the invariant detection. The paper focuses on the approach of detecting functional likely invariant, which accomplish detecting existence of them by discovering functional dependence set of the program variable at first and then detecting the forms of the existent invariants after deducing the function dependence set. Experiments demonstrate that this approach not only solves the problems of blind detection to improve the efficiency but also reduces the possibility of missing important functional invariants compared with the traditional hypothesis verification approach such as Daikon.