Skip to main content
SpringerLink
Log in

Extensible Universes for Object-Oriented Data Models

  • Conference paper
ECOOP 2008 – Object-Oriented Programming (ECOOP 2008)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5142))

Included in the following conference series:

Abstract

We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. This datatype package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, accessors functions, coercions between dynamic and static types, characteristic sets, their relations reflecting inheritance, and the necessary class invariants. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for an object-oriented core-language called imp++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andrews, P.B.: Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)

    MATH  Google Scholar 

  2. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Google Scholar 

  3. Basin, D.A., Kuruma, H., Takaragi, K., Wolff, B.: Verification of a signature architecture with HOL-Z. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) Formal Methods 2005. LNCS, vol. 3582, pp. 269–285. Springer, Heidelberg (2005)

    Google Scholar 

  4. Berghofer, S., Wenzel, M.T.: Inductive Datatypes in HOL – Lessons Learned in Formal-Logic Engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics 1999. LNCS, vol. 1690. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Bierman, G.M., Parkinson, M.J.: Effects and effect inference for a core Java calculus. Electronic Notes in Theoretical Computer Science 82(7), 1–26 (2003)

    Article  Google Scholar 

  6. Brucker, A.D.: An Interactive Proof Environment for Object-oriented Specifications. Ph.d. thesis, ETH Zurich, 2007. ETH Dissertation No. 17097

    Google Scholar 

  7. Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9(2), 152–172 (2003)

    Google Scholar 

  8. Brucker, A.D., Wolff, B.: The HOL-OCL book. Tech. Rep. 525, ETH Zurich (2006)

    Google Scholar 

  9. Brucker, A.D., Wolff, B.: HOL-OCL – A Formal Proof Environment for UML-OCL. In: Fiadeiro, J., Inverardi, P. (eds.) Fundamental Approaches to Software Engineering FASE 2008, vol. 4961, pp. 97–100. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  10. Drossopoulou, S., Eisenbach, S.: Describing the semantics of Java and proving type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 41–82. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Flatt, M., Krishnamurthi, S., Felleisen, M.: A programmer’s reduction semantics for classes and mixins. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol. 1523, pp. 241–269. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, New York (1993)

    MATH  Google Scholar 

  13. Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GI. ACM Transactions on Programming Languages and Systems 23(3), 396–450 (2001)

    Article  Google Scholar 

  14. Leino, K.R.M., Müller, P.: Modular verification of static class invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) Formal Methods 2005. LNCS, vol. 3582, pp. 26–42. Springer, Heidelberg (2005)

    Google Scholar 

  15. Marché, C., Paulin-Mohring, C.: Reasoning about Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics 2005. LNCS, vol. 3603, pp. 179–194. Springer, Heidelberg (2005)

    Google Scholar 

  16. Melham, T.F.: A package for inductive relation definitions in HOL. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) International Workshop on the HOL Theorem Proving System and its Applications (TPHOLs), pp. 350–357. IEEE Computer Society Press, Los Alamitos (1992)

    Google Scholar 

  17. Müller, O., Nipkow, T., von Oheimb, D., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9(2), 191–223 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  18. Naraschewski, W., Wenzel, M.: Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics 1998. LNCS, vol. 1479, pp. 349–366. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  19. Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10(2), 171–186 (1998)

    Article  MATH  Google Scholar 

  20. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  21. Nipkow, T., von Oheimb, D.: Javaℓight is type-safe—definitely. In: ACM Symp. Principles of Programming Languages POPL, pp. 161–170. ACM Press, New York (1998)

    Chapter  Google Scholar 

  22. Unified modeling language specification (version 1.5) (2003), Available as OMG document formal/03-03-01

    Google Scholar 

  23. Paulson, L.C.: A fixedpoint approach to (co)inductive and (co)datatype definitions. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 187–211. MIT Press, Cambridge (2000)

    Google Scholar 

  24. Smith, G., Kammüller, F., Santen, T.: Encoding Object-Z in Isabelle/HOL. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 82–99. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) Formal Methods Europe 2002. LNCS, vol. 2391, pp. 89–105. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SAP Research, Vincenz-Priessnitz-Str. 1, 76131, Karlsruhe, Germany

    Achim D. Brucker

  2. Universität des Saarlandes, 66041, Saarbrücken, Germany

    Burkhart Wolff

Authors
  1. Achim D. Brucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Burkhart Wolff
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Vitek

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brucker, A.D., Wolff, B. (2008). Extensible Universes for Object-Oriented Data Models. In: Vitek, J. (eds) ECOOP 2008 – Object-Oriented Programming. ECOOP 2008. Lecture Notes in Computer Science, vol 5142. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70592-5_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70592-5_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70591-8

  • Online ISBN: 978-3-540-70592-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation