Extending OCL with Null-References

By Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff.

From its beginnings, OCL is based on a strict semantics for undefinedness, with the exception of the logical connectives of type Boolean that constitute a three-valued propositional logic. Recent versions of the OCL standard added a second exception element, which, similar to the null references in object-oriented programming languages, is given a non-strict semantics. Unfortunately, this extension has been done in an ad hoc manner, which results in several inconsistencies and contradictions.

In this paper, we present a consistent formal semantics (based on our HOL-OCL approach) that includes such a non-strict exception element. We discuss the possible consequences concerning class diagram semantics as well as deduction rules. The benefits of our approach for the specification-pragmatics of design level operation contracts are demonstrated with a small case-study.

Keywords:
HOL-OCL, UML, OCL, Null Reference, Formal Semantics

Please cite this work as follows:
A. D. Brucker, M. P. Krieger, and B. Wolff, “Extending OCL with null-references,” in Models in software engineering, S. Gosh, Ed. Heidelberg: Springer-Verlag, 2009, pp. 261–275. doi: 10.1007/978-3-642-12261-3_25. Selected best papers from all satellite events of the MoDELS 2009 conference.. Author copy: https://logicalhacking.com/publications/brucker.ea-ocl-null-2009/

BibTeX
@InCollection{ brucker.ea:ocl-null:2009,
  author      = {Achim D. Brucker and Matthias P. Krieger and Burkhart Wolff},
  wsbooktitle = {The Pragmatics of {OCL} and Other Textual Specification
                 Languages},
  note        = {Selected best papers from all satellite events of the MoDELS
                 2009 conference.. 
                 Author copy: \url{https://logicalhacking.com/publications/brucker.ea-ocl-null-2009/}},
  booktitle   = {Models in Software Engineering},
  publisher   = {Springer-Verlag },
  address     = {Heidelberg },
  series      = {Lecture Notes in Computer Science },
  number      = {6002},
  editor      = {Sudipto Gosh},
  pages       = {261--275},
  doi         = {10.1007/978-3-642-12261-3_25},
  language    = {USenglish},
  title       = {Extending {OCL} with Null-References},
  year        = {2009},
  location    = {Denver, Colorado, USA},
  areas       = {formal methods, software},
  abstract    = {From its beginnings, OCL is based on a strict semantics for
                 undefinedness, with the exception of the logical connectives
                 of type Boolean that constitute a three-valued propositional
                 logic. Recent versions of the OCL standard added a second
                 exception element, which, similar to the null references in
                 object-oriented programming languages, is given a non-strict
                 semantics. Unfortunately, this extension has been done in an
                 ad hoc manner, which results in several inconsistencies and
                 contradictions.
                 
                 In this paper, we present a consistent formal semantics (based
                 on our HOL-OCL approach) that includes such a non-strict
                 exception element. We discuss the possible consequences
                 concerning class diagram semantics as well as deduction rules.
                 The benefits of our approach for the specification-pragmatics
                 of design level operation contracts are demonstrated with a
                 small case-study.},
  bibkey      = {brucker.ea:ocl-null:2009},
  keywords    = {HOL-OCL, UML, OCL, Null Reference, Formal Semantics},
  pdf         = {https://logicalhacking.com/publications/brucker.ea-ocl-null-2009/brucker.ea-ocl-null-2009.pdf},
}