Re: OCL foundation

Re: OCL foundation

From: Achim D. Brucker ^lt;>
Date: Wed 15 Mar 2006 - 07:07:50 GMT
Message-ID: <>
Steffen Zschaler <> schrieb:
> Hi,
> As far as I know, the formal (in your sense) foundation used to be in=20
> Mark Richter's PhD thesis. This used to be the semantics chapter of a=20
> pre-final version of the submission, but was then moved to the=20
> non-normative appendix in favour of the MMF-based approach that is now=20
> in the standard. During revisions it seems to have disappeared magically.=

sad but true, that's one reason why we base our work (HOL-OCL [1]) on
version 03-10-14 of the OCL 2.0 specification. On of the ideas behind
our work is to provide a formal semantics for OCL in terms of
higer-order logic (HOL), especially Isabelle/HOL [2].  

This is somewhat different to the more algebraic approach taken by
Mark Richters (i.e., the semantics presented in the appendix of the
OCL 2.0 standard [3]). We use this semantics as the foundation of our
definitions, but in contrast to this semantics, we show, that our
semantics conforms to the normative part of the standard, i.e.,
chapter 11. We are doing this by proving all properties described in
chapter 11 of the standard. Thus, while most of our definitions differ
syntactically from the one in the standard (i.e., we define
the ->forall() on sets in terms of the HOL forall and not using
->iterate(), we later on prove, that we our ->forall() definitions 
has the required properties).

Achim and Burkhart

[3] UML 2.0 OCL Specification, OMG document 03-10-14. 

PS: Sorry if this mail is send twice, the first one seems to get lost
Received on Wed Mar 15 07:08:24 2006