Local mirror of Featherweight OCL entry of the Archive of Formal Proofs (AFP). https://www.isa-afp.org/entries/Featherweight_OCL.shtml
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

86 lines
4.6 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight
  3. OCL: A Proposal for a Machine-Checked Formal Semantics for OCL
  4. 2.5. In Archive of Formal Proofs,
  5. 2014. http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal
  6. proof development
  7. A BibTeX entry for LaTeX users is
  8. @Article{ brucker.ea:featherweight:2014,
  9. abstract = {The Unified Modeling Language (UML) is one of the
  10. few modeling languages that is widely used in
  11. industry. While UML is mostly known as diagrammatic
  12. modeling language (e.g., visualizing class models),
  13. it is complemented by a textual language, called
  14. Object Constraint Language (OCL). OCL is based on a
  15. three-valued logic that turns UML into a formal
  16. language. Unfortunately the semantics of this
  17. specification language, captured in the "Annex A" of
  18. the OCL standard, leads to different interpretations
  19. of corner cases. We formalize the core of OCL:
  20. denotational definitions, a logical calculus and
  21. operational rules that allow for the execution of
  22. OCL expressions by a mixture of term rewriting and
  23. code compilation. Our formalization reveals several
  24. inconsistencies and contradictions in the current
  25. version of the OCL standard. Overall, this document
  26. is intended to provide the basis for a
  27. machine-checked text "Annex A" of the OCL standard
  28. targeting at tool implementors.},
  29. author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
  30. file = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},
  31. filelabel= {Outline},
  32. issn = {2150-914x},
  33. journal = {Archive of Formal Proofs},
  34. month = {jan},
  35. note = {\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}, Formal proof development},
  36. pdf = {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},
  37. title = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
  38. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014},
  39. year = {2014},
  40. }
  41. An overview of the formalization is given in:
  42. Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for
  43. the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and
  44. Textual Modelling (OCL 2012). , pages 19-24, 2012. The semantics for
  45. the Boolean operators proposed in this paper was adopted by the OCL
  46. 2.4 standard.
  47. A BibTeX entry for LaTeX users is
  48. @InProceedings{ brucker.ea:featherweight:2012,
  49. abstract = {At its origins, OCL was conceived as a strict
  50. semantics for undefinedness, with the exception of the
  51. logical connectives of type Boolean that constitute a
  52. three-valued propositional logic. Recent versions of
  53. the OCL standard added a second exception element,
  54. which, similar to the null references in programming
  55. languages, is given a non-strict semantics.\\\\In this
  56. paper, we report on our results in formalizing the
  57. core of OCL in higher-order logic (HOL). This
  58. formalization revealed several inconsistencies and
  59. contradictions in the current version of the OCL
  60. standard. These inconsistencies and contradictions are
  61. reflected in the challenge to define and implement OCL
  62. tools (e.g., interpreters, code-generators, or theorem
  63. provers) in a uniform manner.},
  64. author = {Achim D. Brucker and Burkhart Wolff},
  65. booktitle= {Workshop on OCL and Textual Modelling (OCL 2012)},
  66. doi = {10.1145/2428516.2428520},
  67. isbn = {978-1-4503-1799-3},
  68. keywords = {OCL, HOL-OCL, formal semantics},
  69. note = {The semantics for the Boolean operators proposed in this paper
  70. was adopted by the OCL 2.4 standard.},
  71. pages = {19--24},
  72. pdf = {https://www.brucker.ch/bibliography/download/2012/brucker.ea-featherweight-2012.pdf},
  73. talk = {talk:brucker.ea:featherweight:2012},
  74. title = {Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL},
  75. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012},
  76. year = {2012},
  77. }