Verifying Object-Oriented Code Using Object Propositions

The modular verification of object-oriented code is made dif-ficult by the presence of aliasing. If there are multiple clients depending on the properties of an object, one client may break the property that others depend on. Knowledge of both aliasing and predicates allows us to verify whether clients and implementations are compliant with specifications. We have developed a modular verification approach, by introducing the novel abstraction object propositions, that combines predicates and information about object aliasing. In our methodology, even if shared data is modified, we know that an object invariant specified by a client holds. This allows two references pointing to the same object to have a consistent view of the object. Our object invariant is different than a class invariant such as the ones in ESC/Java, as in ou