[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Semantics, calculi, and analysis for object-oriented specifications

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrial J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)

    MATH  Google Scholar 

  2. Abrial J.R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York (2009)

    Google Scholar 

  3. Ahrendt W., Baar T., Beckert B., Bubel R., Giese M., Hähnle R., Menzel W., Mostowski W., Roth A., Schlager S., Schmitt P.H.: The KeY tool. Softw. Syst. Model. 4(1), 32–54 (2005). doi:10.1007/s10270-004-0058-x

    Article  Google Scholar 

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

    MATH  Google Scholar 

  5. Boulton R., Gordon A., Gordon M.J.C., Harrison J., Herbert J., Tassel J.V.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds) Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, IFIP Transactions, vol. A-10, pp. 129–156. North-Holland, Nijmegen (1993)

    Google Scholar 

  6. Brucker, A.D.: An interactive proof environment for object-oriented specifications. Ph.D. thesis, ETH Zurich (2007). ETH Dissertation No. 17097

  7. Brucker, A.D., Doser, J., Wolff, B.: An MDA framework supporting OCL. Electronic Communications of the EASST 5 (2006)

  8. Brucker A.D., Doser J., Wolff B.: A model transformation semantics and analysis methodology for SecureUML. In: Nierstrasz, O., Whittle, J., Harel, D., Reggio, G. (eds) MoDELS 2006: Model Driven Engineering Languages and Systems. Lecture Notes in Computer Science, vol. 4199, pp. 306–320. Springer, Berlin (2006). doi:10.1007/11880240_22

    Google Scholar 

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

  10. Brucker A.D., Wolff B.: An extensible encoding of object-oriented data models in HOL. J. Autom. Reason. 41, 219–249 (2008). doi:10.1007/s10817-008-9108-3

    Article  Google Scholar 

  11. Church A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)

    Article  MATH  MathSciNet  Google Scholar 

  12. Gabbay D.M.: Labelled Deductive Systems, Oxford Logic Guides, vol. 1. Oxford University Press, New York (1997)

    Google Scholar 

  13. Gogolla M., Richters M.: Expressing UML class diagrams properties with OCL. In: Clark, T., Warmer, J. (eds) Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263, pp. 85–114. Springer, Heidelberg (2002)

    Google Scholar 

  14. Hähnle, R.: Efficient deduction in many-valued logics. In: International Symposium on Multiple-Valued Logics (ISMVL), pp. 240–249. IEEE Computer Society, Los Alamitos (1994). doi:10.1109/ismvl.1994.302195

  15. Hähnle R.: Tableaux for many-valued logics. In: D’Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds) Handbook of Tableau Methods, pp. 529–580. Kluwer, Dordrecht (1999)

    Google Scholar 

  16. Jones C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall, Upper Saddle River (1990) ISBN 0-13-880733-7

    MATH  Google Scholar 

  17. Kerber, M., Kohlhase, M.: A tableau calculus for partial functions. In: Collegium Logicum—Annals of the Kurt-Gödel-Society, vol. 2, pp. 21–49. Springer, New York (1996)

  18. Kleppe A., Warmer J., Bast W.: MDA Explained. The Model Driven Architecture: Practice and Promise. Addison-Wesley, Reading (2003)

    Google Scholar 

  19. Kobryn C.: UML 2001: a standardization odyssey. Commun. ACM 42(10), 29–37 (1999). doi:10.1145/317665.317673

    Article  Google Scholar 

  20. Leino K.R.M., Müller P.: Modular verification of static class invariants. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 26–42. Springer, Heidelberg (2005). doi:10.1007/11526841_4

    Google Scholar 

  21. Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC/Java user’s manual. Tech. Rep. SRC-2000-002, Compaq Systems Research Center (2000)

  22. Marché C., Paulin-Mohring C.: Reasoning about Java programs with aliasing and frame conditions. In: Hurd, J., Melham, T.F. (eds) Theorem Proving in Higher Order Logics (TPHOLS). Lecture Notes in Computer Science, vol. 3603, pp. 179–194. Springer, Heidelberg (2005). doi:10.1007/11541868_12

    Google Scholar 

  23. Nipkow T., Paulson L.C., Wenzel M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9

    Google Scholar 

  24. Richters, M.: A precise approach to validating UML models and OCL constraints. Ph.D. thesis, Universität Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14 (2002)

  25. Richters M., Gogolla M.: OCL: Syntax, semantics, and tools. In: Clark, T., Warmer, J. (eds) Object Modeling with the OCL: The Rationale behind the Object Constraint Language. Lecture Notes in Computer Science, vol. 2263, pp. 42–68. Springer, Heidelberg (2002)

    Google Scholar 

  26. Schmidt D.C.: Guest editor’s introduction: Model-driven engineering. Computer 39(2), 25–31 (2006). doi:10.1109/MC.2006.58

    Article  Google Scholar 

  27. Spivey J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall, Upper Saddle River (1992)

    Google Scholar 

  28. UML 2.0 OCL specification (2003). Available as OMG document. http://www.omg.org/cgi-bin/doc?ptc/03-10-14

  29. Unified modeling language specification (version 1.5) (2003). Available as OMG document. http://www.omg.org/cgi-bin/doc?formal/03-03-01

  30. Viganò L.: Labelled Non-Classical Logics. Kluwer, Dordrecht (2000)

    MATH  Google Scholar 

  31. von Oheimb, D.: Analyzing Java in Isabelle/HOL: formalization, type safety and Hoare logic. Ph.D. thesis, Technische Universität München (2001)

  32. 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) FME 2002: Formal Methods—Getting IT Right. Lecture Notes in Computer Science, vol. 2391, pp. 89–105. Springer, Heidelberg (2002). doi:10.1007/3-540-45614-7_6

    Chapter  Google Scholar 

  33. Wenzel M., Wolff B.: Building formal method tools in the Isabelle/Isar framework. In: Schneider, K., Brandt, J. (eds) TPHOLS 2007. Lecture Notes in Computer Science, vol. 4732, pp. 351–366. Springer, Heidelberg (2007)

    Google Scholar 

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

    MATH  Google Scholar 

  35. Woodcock J., Davies J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1996)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Achim D. Brucker

  2. Université Paris-Sud, Parc Club, 4, Rue Jaques Monod, 91893, Orsay Cedex, France

    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

Corresponding author

Correspondence to Achim D. Brucker.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Brucker, A.D., Wolff, B. Semantics, calculi, and analysis for object-oriented specifications. Acta Informatica 46, 255–284 (2009). https://doi.org/10.1007/s00236-009-0093-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-009-0093-8

Keywords

Search

Navigation