On the Semantics of Object-oriented Data Structures and Path Expressions (Extended Version)

Book English OPEN
Brucker, A.D. ; Longuet, D. ; Tuong, F. ; Wolff, B. (2013)

\UML/ØCL is perceived as the de-facto standard for specifying object-oriented models in general and data models in particular. Since recently, all data types of \UML/ØCL comprise two different exception elements: \inlineoclinvalid (“bottom” in semantics terminology) and \inlineoclnull (for “non-existing element”). This has far-reaching consequences on both the logical and algebraic properties of ØCL expressions as well as the path expressions over object-oriented data structures, \ie, class models. In this paper, we present a formal semantics for object-oriented data models in which all data types and, thus, all class attributes and path expressions, support \inlineoclinvalid and \inlineoclnull. Based on this formal semantics, we present a set of ØCL test cases that can be used for evaluating the support of \inlineoclnull and \inlineoclinvalid in ØCL tools.
  • References (12)
    12 references, page 1 of 2

    [1] P. B. Andrews. Introduction to Mathematical Logic and Type Theory: To Truth through Proof. Kluwer Academic Publishers, 2nd edition, 2002. ISBN 1-402-00763- 9.

    [2] M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In G. Barthe, L. Burdy, M. Huisman, J.-L. Lanet, and T. Muntean, editors, Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), volume 3362 of LNCS, pages 49-69. Springer, May 25 2005. ISBN 978-3-540-24287-1. doi: 10.1007/b105030.

    [3] A. D. Brucker and B. Wolff. An extensible encoding of object-oriented data models in HOL. Journal of Automated Reasoning, 41:219-249, 2008. ISSN 0168-7433. doi: 10.1007/s10817-008-9108-3. URL http://www.brucker.ch/bibliography/ abstract/brucker.ea-extensible-2008-b.

    [4] A. D. Brucker and B. Wolff. HOL-OCL - A Formal Proof Environment for UML/OCL. In J. Fiadeiro and P. Inverardi, editors, Fundamental Approaches to Software Engineering (FASE08), number 4961 in LNCS, pages 97-100. Springer, 2008. doi: 10.1007/978-3-540-78743-3_8. URL http://www.brucker. ch/bibliography/abstract/brucker.ea-hol-ocl-2008.

    [5] A. D. Brucker and B. Wolff. Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and Textual Modelling (OCL 2012), pages 19-24, 2012. ISBN 978-1-4503-1799-3. doi: 10. 1145/2428516.2428520. URL http://www.brucker.ch/bibliography/abstract/ brucker.ea-featherweight-2012.

    [6] A. D. Brucker, M. P. Krieger, and B. Wolff. Extending OCL with null-references. In S. Gosh, editor, Models in Software Engineering, number 6002 in LNCS, pages 261-275. Springer, 2009. doi: 10.1007/978-3-642-12261-3_25. URL http://www. brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009. Selected best papers from all satellite events of the MoDELS 2009 conference.

    [7] P. Chalin and F. Rioux. Non-null references by default in the Java modeling language. In SAVCBS '05: Proceedings of the 2005 conference on Specification and verification of component-based systems, page 9. ACM Press, 2005. ISBN 1- 59593-371-9. doi: 10.1145/1123058.1123068.

    [8] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68, June 1940.

    [9] G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML reference manual (revision 1.2), Feb. 2007. Available from http://www.jmlspecs.org.

    [10] Object Management Group. UML 2.0 OCL specification, Apr. 2006. Available as OMG document formal/06-05-01.

  • Metrics
    views in OpenAIRE
    views in local repository
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    White Rose Research Online - IRUS-UK 0 2
Share - Bookmark