From: Achim D. Brucker ^lt;*brucker@spamfence.net*>

Date: Wed 15 Mar 2006 - 07:07:50 GMT

Message-ID: <slrne1ffa6.ro.brucker@nakagawa.inf.ethz.ch>

Date: Wed 15 Mar 2006 - 07:07:50 GMT

Message-ID: <slrne1ffa6.ro.brucker@nakagawa.inf.ethz.ch>

Hi, Steffen Zschaler <sz9@inf.tu-dresden.de> 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 [1] http://www.brucker.ch/projects/hol-ocl/index.en.html [2] http://isabelle.in.tum.de [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 somewhere...Received on Wed Mar 15 07:08:24 2006