A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models

  • Bernhard Reus
  • Martin Wirsing
  • Rolf Hennicker
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2029)


The Object Constraint Language OCL offers a formal notation for constraining the modelling elements occurring in UML diagrams. In this paper we apply OCL for developing Java realizations of UML design models and introduce a new Hoare-Calculus for Java classes which uses OCL as assertion language. The Hoare rules are as usual for while programs, blocks and (possibly recursive) method calls. Update of instance variables is handled by an explicit substitution operator which also takes care of aliasing. For verifying a Java subsystem w.r.t. a design subsystem specified using OCL constraints we define an appropriate realization relation and illustrate our approach by an example.


Operational Semantic Logical Variable Design Class Proof Obligation Java Class 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In Michel Bidoit and Max Dauchet, editors, Theory and Practice of Software Development: Proceedings / TAPSOFT’ 97, 7th International Joint Conference CAAP/FASE, volume 1214 of Lecture Notes in Computer Science, pages 682–696. Springer-Verlag, 1997.Google Scholar
  2. 2.
    J. Alves-Foss, editor. Formal Syntax and Semantics of Java, volume 1523 of Lect. Notes Comp. Sci. Springer, Berlin, 1999.Google Scholar
  3. 3.
    K.R. Apt. Ten Years of Hoare’s Logic: A Survey-Part I. TOPLAS, 3(4):431–483, 1981.zbMATHCrossRefGoogle Scholar
  4. 4.
    K.R. Apt and E.R. Olderog. Verification of Sequential and Concurrent Programs. Springer, 1991.Google Scholar
  5. 5.
    M. Bidoit, R. Hennicker, F. Tort, and M. Wirsing. Correct realizations of interface constraints with OCL. In UML’99, The Unified Modeling Language-Beyond the Standard, Fort Collins, USA, volume 1723 of Lecture Notes in Computer Science. Springer-Verlag, 1999.Google Scholar
  6. 6.
    R. Bornat. Pointer aliasing in Hoare logic. In Mathematics of Program Construction, volume 1837 of Lecture Notes in Computer Science, pages 102–126. Springer-Verlag, 2000.CrossRefGoogle Scholar
  7. 7.
    C. Calcagno, S. Ishtiaq, and P.W. O’Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Principles and Practice of Declarative Programming. ACM Press, 2000.Google Scholar
  8. 8.
    P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. From Sequential to Multi-Threaded Java: An Event-Based Operational Semantics. In M. Johnson, editor, Proc. 6 th Int. Conf. Algebraic Methodology and Software Technology, volume 1349 of Lect. Notes Comp. Sci., pages 75–90, Berlin, 1997. Springer.Google Scholar
  9. 9.
    P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An Event-Based Structural Operational Semantics of Multi-Threaded Java. In Alves-Foss [2], pages 157–200.Google Scholar
  10. 10.
    F.S. de Boer. A WP-calculus for OO. In W. Thomas, editor, Foundations of Software Science and Computations Structures, volume 1578 of Lecture Notes in Computer Science. Springer-Verlag, 1999.Google Scholar
  11. 11.
    D. D’Souza and A.C. Wills. Objects, components and frameworks with UML: the Catalysis approach. Addison-Wesley, Reading, Mass., etc., 1998.Google Scholar
  12. 12.
    James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. Addison-Wesley, Reading, Mass., 1996.zbMATHGoogle Scholar
  13. 13.
    C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12:576–583, 1969.zbMATHCrossRefGoogle Scholar
  14. 14.
    Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In Object Oriented Programming: Systems, Languages and Applications (OOPSLA), volume 35, pages 208–228. ACM SIGPLAN Notices, 2000.Google Scholar
  15. 15.
    K. Rustan M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. Technical Report KRML 65-0, SRC, 1996.Google Scholar
  16. 16.
    B. Liskov and J. Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811–1841, 1994.CrossRefGoogle Scholar
  17. 17.
    Object Management Group. Unified Modeling Language-Object Constraint Language Specification. Technical report, available at, 1998.
  18. 18.
    A. Poetzsch-Heffter and P. Muller. A logic for the verification of object-oriented programs. In R. Berghammer and F. Simon, editors, Programming Languages and Fundamentals of Programming, Lecture Notes in Computer Science. Springer-Verlag, 1997.Google Scholar
  19. 19.
    A. Poetzsch-He-ter and P. Muller. A programming logic for sequential Java. In S. D. Swierstra, editor, European Symposium on Programming (ESOP), Lecture Notes in Computer Science. Springer-Verlag, 1999.Google Scholar
  20. 20.
    B. Reus and M. Wirsing. A Hoare-Logic for Object-oriented Programs. Technical report, LMU Munchen, 2000.Google Scholar
  21. 21.
    J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Manual. Addison-Wesely, Reading, Mass., etc., 1998.Google Scholar
  22. 22.
    D. von Oheimb. Hoare logic for mutual recursion and local variables. In V. Raman C. Pandu Rangan and R. Ramanujam, editors, Found. of Software Techn. and Theoret. Comp. Sci., volume 1738 of LNCS, pages 168–180. Springer, 1999.CrossRefGoogle Scholar
  23. 23.
    J. Warmer and A. Kleppe. The Object Constraint Language. Addison-Wesley, Reading, Mass., etc., 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Bernhard Reus
    • 1
  • Martin Wirsing
    • 2
  • Rolf Hennicker
    • 2
  1. 1.School of Cognitive and Computing SciencesUniversity of Sussex at BrightonUK
  2. 2.Institut für InformatikLudwig-Maximilians-Universität MünchenGermany

Personalised recommendations