Object Propositions

The presence of aliasing makes modular verification of object-oriented code difficult. If multiple clients depend on the properties of an object, one client may break a property that others depend on. We have developed a modular verification approach based on the novel abstraction of object propositions, which combine 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. Our permission system allows verification using a mixture of linear and nonlinear reasoning. This allows it to provide more modularity in some cases than competing separation logic approaches, because it can more effectively hide the exact aliasing relationships within a module. We validate our approach on an instance of the composite pattern that illustrates our system’s practicality. We implement our methodology in the intermediate verification language Boogie (of Microsoft We propose a method for modular verification of object-oriented code in the presence of aliasing, i.e., the existence of multiple references to the same object. The seminal work of Parnas [22] describes the importance of modular programming, where the information hiding criteria is use