Luo, C. and Qin, S. (2008) 'Separation logic for multiple inheritance.', Electronic notes in theoretical computer science., 212 . pp. 27-40.
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.
|Keywords:||Multiple Inheritance, Separation Logic, Verification.|
|Full text:||(AM) Accepted Manuscript|
Download PDF (167Kb)
|Publisher Web site:||http://dx.doi.org/10.1016/j.entcs.2008.04.051|
|Record Created:||23 Nov 2009 13:20|
|Last Modified:||02 Dec 2011 16:16|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Look up in GoogleScholar | Find in a UK Library|