Negative Variables and the Essence of Object-Oriented Programming

  • Bertrand Meyer
  • Alexander Kogtenkov
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


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.


Program logic operational semantics object-oriented language 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local Verification of Global Invariants in Concurrent Programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 480–494. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  3. 3.
    Darvas, Á., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol. 4422, pp. 336–351. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 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),
  5. 5.
    Fronk, A.: An Approach to Algebraic Semantics of Object-Oriented Languages. – Software-Technology. University of Dortmund, Germany (2003), doi:2003/2682Google Scholar
  6. 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. 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),
  8. 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. 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. 10.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall (1997)Google Scholar
  11. 11.
    Meyer, B.: Steps Towards a Theory and Calculus of Aliasing. International Journal of Software and Informatics (2011)Google Scholar
  12. 12.
    Meyer, B.: Towards a Calculus of Object Programs. In: Festschrift, J.B., Breitman, K., Horspool, N. (eds.). Springer (2012)Google Scholar
  13. 13.
    Müller, P. (ed.): Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  14. 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
  15. 15.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica 6(4), 319–340 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Schoeller, B.: Aliased-based Reasoning for Object-Oriented Programs. Tech. Report, ETH Zurich (2005),
  17. 17.
    Shield, J.: Towards an Object-Oriented Refinement Calculus. - PhD Thesis, The University of Queensland (2004)Google Scholar
  18. 18.
    Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based generic type system for object-oriented programs. Frontiers of Computer Science 7(1), 109–134 (2013), doi:10.1007/s11704-012-1307-8MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Bertrand Meyer
    • 1
    • 2
    • 3
  • Alexander Kogtenkov
    • 3
    • 2
  1. 1.ETH ZurichSwitzerland
  2. 2.Eiffel SoftwareSanta BarbaraUSA
  3. 3.ITMO National Research UniversitySaint PetersburgUSA

Personalised recommendations