**From:** Burkhart Wolff (*wolff@informatik.uni-freiburg.de*)

**Date:** Tue 10 Sep 2002 - 15:05:37 BST

**Next message:**Tony Simons: "Denotation, Meaning (and Humble Pie) (was Re: [wg@2uworks.org])"**Previous message:**Joaquin Miller: "RE: [wg@2uworks.org] Re: Book"**In reply to:**Bauer, Robert: "An observation"

Hi, Bauer, Robert wrote: >Mitch, > >Like you, I am unfamilar with the 2U document and like you, I am often >confused because the notions of semantic domain, etc., in this thread >are quite different from the standard usage in the formal methods and >formal semantics community. > We made the same observations which laid to our work on an embedding of UML/OCL in Isabelle/HOL (see [1],[2]). > >The call for a formal semantics is a good one and the deep embedding of OCL >in HOL is a good start; however, since OCL cannot fully express the >metamodel, >using ocl to define the semantics is somewhat questionable. Note, that >semantics >is used in the sense that a compiler has a semantic analysis phase rather >than >in the denotational, axiomatic, or operational sense. > We fully agree - using OCL in order to define OCL is a bad idea. Even if OCL would be extended to capture all the needs of such a definition, the problem is simply shifted to the meta-level: This semantics would again need a semantics, and again, the mathematical standards for such an enterprise are Standard Set Theory (ZF-Theory) or HOL, whose typed set-theory is sufficient for OCL (including inheritance). For a formal, machine-based analysis, is HOL even more attractive here. Note however, that there is no need for a *deep* embedding - a shallow embedding paves the way for prototypical tool support and is more flexible for the current stage of the semantics definition. Some aspect of this question is debatable, however: our definition for the union of set's for example, is: (uniondef) "union == (lift2(strictifyN(%X. strictifyN(%Y. Abs_Set(lift ((drop (Rep_Set X)) Un (drop(Rep_Set Y))))))))" This definition is somewhat illegible and not what a textbook definition would look like. However, this is not the result of shallow representation. This particular form is a result of a combinator-based operator representation we chose: For each of the features of OCL-semantics (like "all operations are strict", or: "all collection types have smashed semantics" etc) we defined combinators that "do the trick once and for all". Thus, uniformity in the semantics for all operators can be assured, changes can be integrated a lot easier, and for a theorem prover this presentation has advantages too. It is possible to rewrite all our definitions into textbook-style. One could, in fact, generate a semantic definition textbook for OCL that is then guaranteed typechecked and fits perfect to the properties (the theorems) of OCL. The following Isabelle-script: fun bubble2 thm = let val thm = thm RS meta_eq_to_obj_eq; val thm = thm RS fun_cong RS fun_cong RS fun_cong; val thm = simplify(HOL_ss addsimps [lift2_def,lift1_def, strictifyN_def,strictify_def]) (thm) in thm end; converts via "bubble union_def" into: val it = "(xb ->union( xa )) x = (if xb x = UU then UU else if xa x = UU then UU else Abs_SSet (|.drop (Rep_Set (xb x)) Un drop (Rep_Set xa x).|)) This is a definition in shallow style; a translation into deep style (still automatic) would yield: "I[[xb ->union( xa ))]] x = (if I[[xb]] x = UU then UU else if I[[xa]] x = UU then UU else Abs_SSet (|.drop (Rep_Set ( I[[xb]] x)) Un drop (Rep_Set I[[xa]] x).|)) A suitable display-engine (e.g. LaTex) could automatically display this in usual mathematical notation and conver, e.g. UU to \bottom, Un to \cup etc... >Ok, well just my two cents worth - still think the discussion is worthwhile >and am interested >in reading comments etc., but note: if you want to reason, you need a >formal system so that >you can be sure that your reasoning is rigorous within that system. > We agree, and as we outlined above, there is meanwhile standard technolology that makes a typechecked and verified "Textbook-semantics" for a language such as OCL feasible. Achim Brucker and Burkhart Wolff Bibliography: [1] Achim D. Brucker <http://www.informatik.uni-freiburg.de/%7Ebrucker> and Burkhart Wolff <http://www.informatik.uni-freiburg.de/%7Ewolff>. *A Proposal for a Formal OCL Semantics in Isabelle/HOL <http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/2002/ocl_semantic.pdf>*. In /Theorem Proving in Higher Order Logics/. Lecture Notes in Computer Science Springer-Verlag, 2002. (abstract <http://wailoa.informatik.uni-freiburg.de/cgi/publications//extract_abstract.cgi?DATABASE=softech&KEY=brucker.ea:proposal:2002>) (BibTeX entry <http://wailoa.informatik.uni-freiburg.de/cgi/publications//extract_by_key.cgi?DATABASE=softech&KEY=brucker.ea:proposal:2002.bib&FILE=ocl_semantic.bib>) (PDF <http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/2002/ocl_semantic.pdf>) (slides <http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/2002/ocl_semantic_slides.pdf>) (© Springer-Verlag <http://link.springer.de/link/service/series/0558/tocs/t2410.htm>) [2] Achim D. Brucker <http://www.informatik.uni-freiburg.de/%7Ebrucker> and Burkhart Wolff <http://www.informatik.uni-freiburg.de/%7Ewolff>. *HOL-OCL: Experiences, Consequences and Design Choices <http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/2002/holocl_experiences.pdf>*. In /UML 2002: Model Engineering, Concepts and Tools/. Lecture Notes in Computer Science Springer-Verlag, 2002. (abstract <http://wailoa.informatik.uni-freiburg.de/cgi/publications//extract_abstract.cgi?DATABASE=softech&KEY=brucker.ea:hol-ocl:2002>) (BibTeX entry <http://wailoa.informatik.uni-freiburg.de/cgi/publications//extract_by_key.cgi?DATABASE=softech&KEY=brucker.ea:hol-ocl:2002.bib&FILE=holocl_experiences.bib>) (PDF <http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/2002/holocl_experiences.pdf>) (© Springer-Verlag <http://www.springer.de/comp/lncs/index.html>)

**Next message:**Tony Simons: "Denotation, Meaning (and Humble Pie) (was Re: [wg@2uworks.org])"**Previous message:**Joaquin Miller: "RE: [wg@2uworks.org] Re: Book"**In reply to:**Bauer, Robert: "An observation"