Object Propositions
Abstract
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. We thus offer an alternative to separation logic verification approaches. Object propositions can be more modular in some cases than separation logic because they can more effectively hide the exact aliasing relationships within a module. We validate the practicality of our approach by verifying an instance of the composite pattern. We implement our methodology in the intermediate verification language Boogie (of Microsoft Research), for the composite pattern example.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 2013
- Accession Number
- AD1019553
Entities
People
- Hannes Mehnert
- Jonathan Erik Aldrich
- Ligia Nistor
- Stephanie Balzer
Organizations
- Carnegie Mellon University