General aspects of the as prescribed analysis of invariants in the class

An invariant in the class is a predicate, which is true in every state that is proclaimed as valid, independently of what is considered to be a state. In addition, invariants themselves may be based on the behavior of a particular object or a class as a whole. 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 as prescribed analysis which is based on strongest postconditions of methods with the guard as the precondition, thus, determining all reachable states and only them.