Applying Formal Semantics of an Object-oriented Language to Program Invariant Checking