Separation Logic for Multiple Inheritance

Luo, C.; Qin, S.

Abstract

As an extension to Floyd-Hoare logic, separation logic has been used to facilitate reasoning about imperative programs manipulating shared mutable data structures. Recently, it has also been extended to support modular reasoning in Java-like object-oriented languages where only single inheritance is allowed. In this paper we propose an extension of separation logic to support also the reasoning for multiple inheritance in C++ -like languages. To cater for multiple inheritance, we modified the standard storage model for separation logic in a way that the correct reference to a field or a method can be easily determined. On top of this storage model, a set of proof rules are proposed. Our verification system also provides basic support for behavioral subtyping.

Citation

Luo, C., & Qin, S. (2008, June). Separation Logic for Multiple Inheritance. Presented at International Conference on Foundations of Informatics, Computing and Software, Shanghai, China

• Presentation Conference Type: Conference Paper (published)
• Conference Name: International Conference on Foundations of Informatics, Computing and Software
• Start Date: Jun 3, 2008
• End Date: Jun 6, 2008
• Publication Date: Apr 30, 2008
• Deposit Date: Nov 23, 2009
• Publicly Available Date: Jan 4, 2010
• Volume: 212
• Pages: 27-40
• Series Title: Electronic notes in theoretical computer science
• Series ISSN: 1571-0661
• Book Title: 1st International Conference on Foundations of Informatics, Computing and Software, FICS 2008, 3-6 June, 2008, Shanghai, China ; proceedings.
• DOI: https://doi.org/10.1016/j.entcs.2008.04.051
• Keywords: Multiple Inheritance, Separation Logic, Verification.
• Public URL: https://durham-repository.worktribe.com/output/1160939