Negative Variables and the Essence of Object-Oriented Programming
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.
KeywordsProgram logic operational semantics object-oriented language
Unable to display preview. Download preview PDF.
- 4.Ádám, D., Müller, P.: Reasoning about Method Calls in Interface Specifications. Journal of Object Technology 5(5); Special Issue: ECOOP 2005 Workshop FTfJP, pp. 59–85 (June 2006), http://www.jot.fm/issues/issues200606/article3
- 5.Fronk, A.: An Approach to Algebraic Semantics of Object-Oriented Languages. – Software-Technology. University of Dortmund, Germany (2003), doi:2003/2682Google Scholar
- 6.Hoare, C.A.R.: Procedures and Parameters, An Axiomatic Approach. In: Symposium on Semantics of Algorithmic Languages, pp. 102–116 (1971), doi:10.1007/BFb0059696Google Scholar
- 7.Kassios, I.T., Kritikos, E.: A Discipline for Program Verification based on Backpointers and its Use in Observational Disjointness. ETH Zurich, Department of Computer Science (2012), http://dx.doi.org/10.3929/ethz-a-007560318
- 8.Rustan, K., Leino, M.: Ecstatic: An object-oriented programming language with an axiomatic semantics. Digital Equipment Corporation Systems Research Center (1996)Google Scholar
- 9.Meyer, B., Kogtenkov, A., Stapf, E.: Avoid a Void: The Eradication of Null Dereferencing. In: Jones, C.B., Roscoe, A.W., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 189–211. Springer (2010)Google Scholar
- 10.Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall (1997)Google Scholar
- 11.Meyer, B.: Steps Towards a Theory and Calculus of Aliasing. International Journal of Software and Informatics (2011)Google Scholar
- 12.Meyer, B.: Towards a Calculus of Object Programs. In: Festschrift, J.B., Breitman, K., Horspool, N. (eds.). Springer (2012)Google Scholar
- 14.Nienaltowski, P.: Practical framework for contract-based concurrent object-oriented programming. – PhD dissertation 17061, Department of Computer Science, ETH Zurich (February 2007). Other SCOOP references at http://se.inf.ethz.ch/research/cme/
- 16.Schoeller, B.: Aliased-based Reasoning for Object-Oriented Programs. Tech. Report, ETH Zurich (2005), http://se.ethz.ch/people/schoeller/pdfs/10-Annual_Report_CSE_ETHZ_2005.pdf
- 17.Shield, J.: Towards an Object-Oriented Refinement Calculus. - PhD Thesis, The University of Queensland (2004)Google Scholar