### Abstract

The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in industry. While UML is mostly known as diagrammatic modeling language (e.g., visualizing class models), it is complemented by a textual language, called Object Constraint Language (OCL). The current version of OCL is based on a four-valued logic that turns UML into a formal language. Any type comprises the elements "invalid" and "null" which are propagated as strict and non-strict, respectively. Unfortunately, the former semi-formal semantics of this specification language, captured in the "Annex A" of the OCL standard, leads to different interpretations of corner cases. We formalize the core of OCL: denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. Overall, this document is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.

### License

BSD License

### History

October 13, 2015
  afp-devel@ea3b38fc54d6 and hol-testgen@12148
  Update of Featherweight OCL including a change in the abstract.
January 16, 2014
  afp-devel@9091ce05cb20 and hol-testgen@10241
  New Entry: Featherweight OCL

### Topics

- Computer science/System description languages

### Session Featherweight_OCL

- UML_Types
- UML_Logic
- UML_PropertyProfiles
- UML_Boolean
- UML_Void
- UML_Integer
- UML_Real
- UML_String
- UML_Pair
- UML_Bag
- UML_Set
- UML_Sequence
- UML_Library
- UML_State
- UML_Contracts
- UML_Tools
- UML_Main
- Analysis_UML
- Analysis_OCL
- Design_UML
- Design_OCL

## Cite

×

Featherweight_OCL-AFP

    @article{Featherweight_OCL-AFP,
      author  = {Achim D. Brucker and Frédéric Tuong and Burkhart Wolff},
      title   = {Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Featherweight_OCL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Jan 16, 2014 : Isabelle2013-2