Abstract
We present a general storage model that reflects features of object oriented (OO) languages with pure reference semantics. Based on this model, we develop an OO Separation Logic (OOSL) to specify and verify OO programs. Many inference rules in the Separation Logic still hold in OOSL. Additionally, OOSL has certain properties important to OO reasoning. We introduce Hoare-Triple for a small OO language, and use the Schorr-Waite Marking Algorithm as a verification example. © 2012 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Yijing, L., & Zongyan, Q. (2012). A separation logic for OO programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6921 LNCS, pp. 88–105). https://doi.org/10.1007/978-3-642-27269-1_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
