Reasoning about object-oriented programs requires an appropriate technique to reflect a fundamental "general relativity" property of the approach: every operation is relative to a current object, which changes with every qualified call; such a call needs access to the context of the client object. The notion of negative variable, discussed in this article, provides a framework for reasoning about OO programs in any semantic framework. We introduce a fundamental rule describing the semantics of object-oriented calls, its specific versions for such frameworks as axiomatic (Hoare-style) logic and denotational semantics, and its application to such problems as alias analysis and the consistency of concurrent programs. The approach has been implemented as part of a verification environment for a major object-oriented language and used to perform a number of proofs and analyses. © 2014 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Meyer, B., & Kogtenkov, A. (2014). Negative variables and the essence of object-oriented programming. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8373, 171–187. https://doi.org/10.1007/978-3-642-54624-2_9
Mendeley helps you to discover research relevant for your work.