Abstract Interpretation Based Correct Verification for Functional Invariant

The discovery of function invariant is an effective method for improving software quality.As the detecting may contain invalid invariant defects, this paper proposes an abstract interpretation based correct verification for functional invariant.Firstly functional invariants transfer to polynomial relations.Secondly we abstract analysis the foundation of the correctness of polynomial relations with polynomial program and the weakest precondition.Finally we construct polynomial algorithm and verify the function invariant is correct or not with the results obtained.As the same time we state this verification with functional invariant of an C program.