HOL-OCL: Experiences, Consequences and Design Choices

By Achim D. Brucker and Burkhart Wolff.

Based on experiences gained from an embedding of the Object Constraint Language (OCL) in higher-order logic , we explore several key issues of the design of a formal semantics of the OCL. These issues comprise the question of the interpretation of invariants, pre- and postconditions, their transformation, an executable sub-language and the possibilities of refinement notions. A particular emphasize is put on the issue of mechanized deduction in UML/OCL specification.

Keywords:
OCL, Formal semantics, Constraint languages, Refinement, Higher-Order Logic

Supplementary material:
[ Slides  ]

Please cite this work as follows:
A. D. Brucker and B. Wolff, “HOL-OCL: Experiences, consequences and design choices,” in UML 2002: Model engineering, concepts and tools, J.-M. Jézéquel, H. Hussmann, and S. Cook, Eds. Heidelberg: Springer-Verlag, 2002, pp. 196–211. doi: 10.1007/3-540-45800-X_17. Author copy: https://logicalhacking.com/publications/brucker.ea-hol-ocl-2002/

BibTeX
@InCollection{ brucker.ea:hol-ocl:2002,
  abstract  = {Based on experiences gained from an embedding of the Object
               Constraint Language (OCL) in higher-order
               logic~\cite{brucker.ea:proposal:2002}, we explore several key
               issues of the design of a formal semantics of the OCL. These
               issues comprise the question of the interpretation of
               invariants, pre- and postconditions, their transformation, an
               executable sub-language and the possibilities of refinement
               notions. A particular emphasize is put on the issue of
               mechanized deduction in UML/OCL specification.},
  keywords  = {OCL, Formal semantics, Constraint languages, Refinement,
               Higher-Order Logic},
  location  = {Dresden},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {UML 2002: Model Engineering, Concepts and Tools},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {2460},
  pages     = {196--211},
  editor    = {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and Stephen
               Cook},
  title     = {{HOL-OCL}: Experiences, Consequences and Design Choices},
  doi       = {10.1007/3-540-45800-X_17},
  areas     = {formal methods, software},
  isbn      = {3-540-44254-5},
  issn      = {0302-9743},
  year      = {2002},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-hol-ocl-2002/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-hol-ocl-2002/brucker.ea-hol-ocl-2002.pdf},
}