摘要：The concept of an invariant is fundamental to object-oriented programming,because it provides information on the overall behaviour of the class and/or its objects. An invariant is a predicate,that is true in every state that is proclaimed as valid. A strong invariant is a predicate,that is true in every valid state and false in every invalid state. Basically,we can divide them into two categories:object invariants and class invariants. Object invariants describe the consistency of object,i.e. non-static fields. Analysis of invariants takes the most important place in object-oriented program verification and can be directed in two ways – as prescribed and as described. This paper considers both analyses which are based on the strongest dynamic postconditions of methods with the guard as the precondition,thus,determining all possible transitions and only them. In addition,since dynamic postconditions are logical functions of the initial-final states,our solution is based solely on the first-order predicate logic.
