Separation Logic for Multiple Inheritance

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