afp-mirror
/
Featherweight_OCL
1
0
Fork 0
Code Issues 0 Pull Requests 0 Releases 9 Wiki Activity
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.
24 Commits
1 Branch
1.4 MiB
 
 
Branch: master
Branches Tags
${ item.name }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Featherweight_OCL/CITATION

86 lines
4.6 KiB
Raw Permalink Blame History 

  1. To cite the use of this formal theory, please use

  2. 

  3.   Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight

  4.   OCL: A Proposal for a Machine-Checked Formal Semantics for OCL

  5.   2.5. In Archive of Formal Proofs,

  6.   2014. http://www.isa-afp.org/entries/Featherweight_OCL.shtml, Formal

  7.   proof development

  8. 

  9. A BibTeX entry for LaTeX users is

  10. 

  11. @Article{ brucker.ea:featherweight:2014,

  12.       abstract  = {The Unified Modeling Language (UML) is one of the

  13.                   few modeling languages that is widely used in

  14.                   industry. While UML is mostly known as diagrammatic

  15.                   modeling language (e.g., visualizing class models),

  16.                   it is complemented by a textual language, called

  17.                   Object Constraint Language (OCL). OCL is based on a

  18.                   three-valued logic that turns UML into a formal

  19.                   language. Unfortunately the semantics of this

  20.                   specification language, captured in the "Annex A" of

  21.                   the OCL standard, leads to different interpretations

  22.                   of corner cases. We formalize the core of OCL:

  23.                   denotational definitions, a logical calculus and

  24.                   operational rules that allow for the execution of

  25.                   OCL expressions by a mixture of term rewriting and

  26.                   code compilation. Our formalization reveals several

  27.                   inconsistencies and contradictions in the current

  28.                   version of the OCL standard. Overall, this document

  29.                   is intended to provide the basis for a

  30.                   machine-checked text "Annex A" of the OCL standard

  31.                   targeting at tool implementors.},

  32.        author	= {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},

  33.        file	= {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf},

  34.        filelabel= {Outline},

  35.        issn	= {2150-914x},

  36.        journal	= {Archive of Formal Proofs},

  37.        month	= {jan},

  38.        note	= {\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}, Formal proof development},

  39.        pdf	= {https://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf},

  40.        title	= {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},

  41.        url	= {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014},

  42.        year	= {2014},

  43. }

  44. 

  45. 

  46. An overview of the formalization is given in:

  47. 

  48.   Achim D. Brucker and Burkhart Wolff. Featherweight OCL: A study for

  49.   the consistent semantics of OCL 2.3 in HOL. In Workshop on OCL and

  50.   Textual Modelling (OCL 2012). , pages 19-24, 2012. The semantics for

  51.   the Boolean operators proposed in this paper was adopted by the OCL

  52.   2.4 standard.

  53. 

  54. A BibTeX entry for LaTeX users is

  55. 

  56. @InProceedings{ brucker.ea:featherweight:2012,

  57.     abstract = {At its origins, OCL was conceived as a strict

  58.                 semantics for undefinedness, with the exception of the

  59.                 logical connectives of type Boolean that constitute a

  60.                 three-valued propositional logic. Recent versions of

  61.                 the OCL standard added a second exception element,

  62.                 which, similar to the null references in programming

  63.                 languages, is given a non-strict semantics.\\\\In this

  64.                 paper, we report on our results in formalizing the

  65.                 core of OCL in higher-order logic (HOL). This

  66.                 formalization revealed several inconsistencies and

  67.                 contradictions in the current version of the OCL

  68.                 standard. These inconsistencies and contradictions are

  69.                 reflected in the challenge to define and implement OCL

  70.                 tools (e.g., interpreters, code-generators, or theorem

  71.                 provers) in a uniform manner.},

  72. 

  73.     author   = {Achim D. Brucker and Burkhart Wolff},

  74.     booktitle= {Workshop on OCL and Textual Modelling (OCL 2012)},

  75.     doi      = {10.1145/2428516.2428520},

  76.     isbn     = {978-1-4503-1799-3},

  77.     keywords = {OCL, HOL-OCL, formal semantics},

  78.     note     = {The semantics for the Boolean operators proposed in this paper

  79.                 was adopted by the OCL 2.4 standard.},

  80.     pages    = {19--24},

  81.     pdf      = {https://www.brucker.ch/bibliography/download/2012/brucker.ea-featherweight-2012.pdf},

  82.     talk     = {talk:brucker.ea:featherweight:2012},

  83.     title    = {Featherweight OCL: A study for the consistent semantics of OCL 2.3 in HOL},

  84.     url      = {https://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2012},

  85.     year     = {2012},

  86. }