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~citebrucker.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
Categories: ,
Documents: (article) (slides) (handout)
Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff.
HOL-OCL: Experiences, Consequences and Design Choices.
In UML 2002: Model Engineering, Concepts and Tools. Lecture Notes in Computer Science (2460), pages 196-211, Springer-Verlag, 2002.
Keywords: OCL, Formal semantics, Constraint languages, Refinement, higher-order logic
(article) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-45800-X_17) (
| 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.}, | |
| address | = | {Heidelberg}, | |
| author | = | {Achim D. Brucker and Burkhart Wolff}, | |
| booktitle | = | {UML 2002: Model Engineering, Concepts and Tools}, | |
| doi | = | {10.1007/3-540-45800-X_17}, | |
| editor | = | {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and Stephen Cook}, | |
| isbn | = | {3-540-44254-5}, | |
| issn | = | {0302-9743}, | |
| keywords | = | {OCL, Formal semantics, Constraint languages, Refinement, higher-order logic}, | |
| language | = | {USenglish}, | |
| location | = | {Dresden}, | |
| number | = | {2460}, | |
| pages | = | {196--211}, | |
| = | {http://www.brucker.ch/bibliography/download/2002/brucker.ea-hol-ocl-2002.pdf}, | ||
| project | = | {CSFMDOS}, | |
| publisher | = | {Springer-Verlag}, | |
| series | = | {Lecture Notes in Computer Science}, | |
| talk | = | {talk:brucker.ea:hol-ocl:2002}, | |
| title | = | {{HOL-OCL}: Experiences, Consequences and Design Choices}, | |
| url | = | {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2002}, | |
| year | = | {2002}, |