Implementing Application-Specific Object-Oriented Theories in HOL

  • Kenro Yatake
  • Toshiaki Aoki
  • Takuya Katayama
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


This paper presents a theory of Object-Oriented concepts embedded shallowly in HOL for the verification of OO analysis models. The theory is application-specific in the sense that it is automatically constructed depending on the type information of the application. This allows objects to have attributes of arbitrary types, making it possible to verify models using not only basic types but also highly abstracted types specific to the target domain. The theory is constructed by definitional extension based on the operational semantics of a heap memory model, which guarantees the soundness of the theory. This paper mainly focuses on the implementation details of the theory.


Operational Semantic Object Reference Object Constraint Language Null Object Heap Memory 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    OMG. Unified Modeling Language,
  2. 2.
  3. 3.
    Warmer, J., Kleppe, A.: The object constraint language: precise modeling with UML. Addison-Wesley, Reading (1999)Google Scholar
  4. 4.
    Nipkow, T., von Oheimb, D., Pusch, C.: μJava: Embedding a Programming Language in a Theorem Prover. In: Foundations of Secure Computation. IOS Press, Amsterdam (2000)Google Scholar
  5. 5.
    Jacobs, B., et al.: LOOP project,
  6. 6.
    von Oheimb, D.: Hoare Logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience 13, 1173–1214 (2001)zbMATHCrossRefGoogle Scholar
  7. 7.
    Poetzsch-Heffer, A., Muller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, p. 162. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  8. 8.
    Poetzsch-Heffer, A., Muller, P.: Logical Foundations for Typed Object-Oriented Languages. In: Programming Concepts and Methods, PROCOMET (1998)Google Scholar
  9. 9.
    van den Berg, J., Huisman, M., Jacobs, B., Poll, E.: A type-theoretic memory model for verification of sequential Java programs. Techn. Rep. CSI-R9924, Comput. Sci. Inst., Univ. of Nijmegen (1999)Google Scholar
  10. 10.
    Marché, C., Paulin-Mohring, C.: Reasoning on Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 179–194. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  11. 11.
    Naraschewski, W., Wenzel, M.: Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. Tecnische Universitat Munchen (1998)Google Scholar
  12. 12.
    Aoki, T., Tateishi, T., Katayama, T.: An Axiomatic Formalization of UML Models. Practical UML-based Rigorous Development Methods, 13–28 (2001)Google Scholar
  13. 13.
    Marcano, R., Levy, N.(eds.): Using B formal specifications for analysis and verification of UML/OCL models. In: Workshop on consistency problems in UML-based software development. 5th International Conference on the Unified Modeling Language. Dresden, Germany (October 2002)Google Scholar
  14. 14.
    Lano, K., Clark, D., Androutsopoulos, K.: UML to B: Formal Verification of Object-Oriented Models. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 187–206. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Smaragdakis, Y., Batory, D.: Implementing layered designs with mixin layers. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, p. 550. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. 16.
    Fisler, K., Krishnamurthi, S.: Modular verification of collaboration-based software designs. In: Symposium on the Foundation of Software Engineering (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Kenro Yatake
    • 1
  • Toshiaki Aoki
    • 1
    • 2
  • Takuya Katayama
    • 1
  1. 1.Japan Advanced Institute of Science and TechnologyIshikawaJapan
  2. 2.PRESTO JST 

Personalised recommendations