Re: An observation

Date view Thread view Subject view Author view Attachment view

From: Burkhart Wolff (
Date: Tue 10 Sep 2002 - 15:05:37 BST


Bauer, Robert wrote:

>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
>using ocl to define the semantics is somewhat questionable.  Note, that
>is used in the sense that a compiler has a semantic analysis phase rather
>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 
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 
paves the way for prototypical tool support and is more flexible for the 
stage of the semantics definition.

Some aspect of this question is debatable, however: our definition for 
the union of set's
for example, is:

  "union        == (lift2(strictifyN(%X.
                              ((drop (Rep_Set X)) Un (drop(Rep_Set 

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 
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 
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,
    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 

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


[1] Achim D. Brucker <> 
and Burkhart Wolff <>.
*A Proposal for a Formal OCL Semantics in Isabelle/HOL 
In /Theorem Proving in Higher Order Logics/. Lecture Notes in Computer 
Science Springer-Verlag, 2002.
(BibTeX entry 
( Springer-Verlag 
[2] 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 Springer-Verlag, 2002.
(BibTeX entry 
( Springer-Verlag <>)

Date view Thread view Subject view Author view Attachment view