Abstract

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.

PDF available at https://hal.inria.fr/hal-00998923/document