Separation Logic for Multiple Inheritance

Luo, C.; Qin, S.

doi:10.1016/j.entcs.2008.04.051

Separation Logic for Multiple Inheritance

Luo, C.; Qin, S.

Authors

C. Luo

S. Qin

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). Separation Logic for Multiple Inheritance. In 1st International Conference on Foundations of Informatics, Computing and Software, FICS 2008, 3-6 June, 2008, Shanghai, China ; proceedings (27-40). https://doi.org/10.1016/j.entcs.2008.04.051

Conference Name	International Conference on Foundations of Informatics, Computing and Software
Conference Location	Shanghai, China
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.