Paper on OCL Semantics



Date view Thread view Subject view Author view Attachment view

From: Burkhart Wolff (wolff@informatik.uni-freiburg.de)
Date: Fri 24 May 2002 - 17:31:51 BST


Dear all,

A while ago, we started a project to formalize UML/OCL
in Isabelle/HOL as a basis for:

 - a deeper insight into OCL semantics
 - a proof on consistency
    as a result of the conservativity of the logical embedding
 - proof support over OCL specifications
 - test-case generation.

 Our first results of our work are summarized in the paper
 "A Proposal for a Formal Semantics in Isabelle/HOL"
 that will appear in the proceedings of the TPHOLs2002
 in LNCS. (see on our institute's publication page
 www.informatik.uni-freiburg.de/~softech, alternatively
http://wailoa.informatik.uni-freiburg.de/cgi/publications-neu//extract_abstract.cgi?KEY=brucker.ea:proposal:2002

)



In a couple of days, an extended version will also be available.

Among others, it contains an (optional) formal semantics for

- method invocation based on late-binding a la Java

- a semantics for recursive query methods based on least

  fixed-points.



Achim and Burkhart

Date view Thread view Subject view Author view Attachment view