Separation Logic for Multiple Inheritance

Shengchao Qin, Chenguang Luo

    Research output: Contribution to journalArticle

    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.
    Original languageEnglish
    Pages (from-to)27-40
    JournalElectronic Notes in Theoretical Computer Science
    Volume212
    DOIs
    Publication statusPublished - 2008

    Fingerprint Dive into the research topics of 'Separation Logic for Multiple Inheritance'. Together they form a unique fingerprint.

  • Cite this