Towards a K Semantics for OCL

We give a formal definition to a significant subset of the Object Constraint Language (ocl) in the K framework. The chosen subset includes the usual arithmetical, Boolean (including quantifiers), and string expressions; collection expressions (including iterators and navigation); and pre/post conditions for methods. Being executable, our definition provides us, for free, with an interpreter for the chosen subset of ocl. It can be used for free in K definitions of languages having ocl as a component We illustrate some of the advantages of K by comparing our semantical definition of ocl with the official semantics from the language's standard. We also report on a tool implementing our definition that users can try online.