More Flexible Object Invariants with Less Specification Overhead.

Object invariants are used to specify valid object states. They play a central role for reasoning about the correctness of object-oriented software. Current verification methodologies require additional specifications to support the flexibility of modern object oriented programming concepts. This increases the specification effort and represents a new source of error. The presented methodology reduces the currently required specification overhead. It is based on an automatic control flow analysis between code positions violating invariants and code positions requiring their validity. This analysis helps to prevent specification errors, possible in other approaches. Furthermore, the presented methodology distinguishes between valid and invalid invariants within one object. This allows a (more) flexible definition of invariants.