×

zbMATH — the first resource for mathematics

Separation logic for multiple inheritance. (English) Zbl 1286.68320
Chen, Yixiang (ed.) et al., Proceedings of the 1st international conference on foundations of informatics, computing and software (FICS 2008), East China Normal University, Shanghai, China, June 3–6, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 212, 27-40 (2008).
Summary: 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.
For the entire collection see [Zbl 1279.68010].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
03B70 Logic in computer science
Software:
Eiffel
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] W. Chin, C. David, H.H. Nguyen, and S. Qin. Enhancing modular OO verification with separation logic. San Francisco, USA, January 2008. The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08) · Zbl 1295.68082
[2] K. Dhara and G. Leavens. Forcing behavioral subtyping through specification inheritance. Berlin, Germany, March 1996. Proceedings of the 18th International Conference on Software Engineering (ICSE-18)
[3] S. Isthiaq and P. O’Hearn. BI as an assertion language for mutable data structures. London, United Kingdom, January 2001. The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’01)
[4] Liskov, B., Data abstraction and hierarchy, ACM SIGPLAN notices, 23, 5, 1734, (May 1988)
[5] G. Leavens and D. Naumann. Behavioral subtyping is equivalent to modular reasoning for object-oriented programs. Technical Report 06-36, Department of Computer Science, Iowa State University, 2006
[6] Loeckx, J.; Sieber, K.; Stansifer, R., The foundations of program verification, (1984), John Wiley and Sons
[7] Liskov, B.; Wing, J., A behavioral notion of subtyping, ACM transactions on programming languages and systems, 16, 6, 1811-1841, (November 1994)
[8] Meyer, B., Eiffel: the language, Object-oriented series, (1992), Prentice Hall New York · Zbl 0779.68013
[9] P. O’Hearn. Resources, concurrency, and local reasoning. Proceedings of CONCUR’04, LNCS 3170, pp. 49-67 · Zbl 1099.68588
[10] P. O’Hearn, H. Yang, and J. Reynolds. Separation and information hiding. Venice, Italy, January 2004. The 31th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’04) · Zbl 1325.68069
[11] M. Parkinson. Local reasoning for Java. PhD thesis, Cambridge University, August 2005
[12] M. Parkinson and G. Biermann. Separation logic and abstraction. Long Beach, California, USA, January 2005. The 32th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05) · Zbl 1369.68151
[13] M. Parkinson and G. Biermann. Separation logic, abstraction and inheritance. San Francisco, California, USA, January 2008. The 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08) · Zbl 1295.68091
[14] J. Reynolds. Intuitionistic reasoning about shared mutable data structure. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare, 1999
[15] Reynolds, J., Separation logic: A logic for shared mutable data structures, ()
[16] Stroustrup, B., The C++ programming language, (1991), Addison-Wesley
[17] Stroustrup, B., Multiple inheritance for C++, The C/C++ users journal, (May 1999)
[18] Wasserrab, Daniel; Nipkow, Tobias; Snelting, Gregor; Tip, Frank, An operational semantics and type safety proof for multiple inheritance in C++, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.