publication . Book . Report . 2013

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

Achim D. Brucker;
Open Access English
  • Published: 01 Sep 2013
  • Country: United Kingdom
\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 \in...
Funded by
Secure and Trustworthy Composite Services
  • Funder: European Commission (EC)
  • Project Code: 257930
  • Funding stream: FP7 | SP1 | ICT

[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 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 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. 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

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

[11] Object Management Group. UML 2.3.1 OCL specification, Feb. 2012. Available as OMG document formal/2012-01-01.

[12] M. Richters. A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universität Bremen, Logos Verlag, Berlin, BISS Monographs, No. 14, 2002.

Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue