The Strong Object Invariant
The Strong Object Invariant

Summary/Abstract: The concept of an invariant is fundamentalto object-oriented programming, because it providesinformation on the overall behaviour of the class and/orits objects. An invariant is a predicate, that is true inevery state that is proclaimed as valid. A stronginvariant is a predicate, that is true in every valid stateand false in every invalid state. Basically, we can dividethem into two categories: object invariants and classinvariants. Object invariants describe the consistency ofobject, i.e. non-static fields. Analysis of invariants takesthe most important place in object-oriented programverification and can be directed in two ways – asprescribed and as described. This paper considers bothanalyses which are based on the strongest dynamicpostconditions of methods with the guard as theprecondition, thus, determining all possible transitionsand only them. In addition, since dynamic postconditionsare logical functions of the initial-final states, oursolution is based solely on the first-order predicate logic.

• Details
• Contents