Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection

Delphine Longuet (Université Paris-Sud), Frédéric Tuong (IRT SystemX), Burkhart Wolf (LRI)

Résumé

We show how modern proof environments comprising code generators and reflection facilities can be used for the effective construction of a tool for OCL. For this end, we define a UML/OCL meta-model in HOL, a meta-model for Isabelle/HOL in HOL, and a compiling function between them over the vocabulary of the libraries provided by Feather-weight OCL. We use the code generator of Isabelle to generate executable code for the compiler, which is bound to a USE tool like syntax integrated in Isabelle/Featherweight OCL. It generates for an arbitrary class model an object-oriented datatype theory and proves the relevant properties for casts, type-tests, constructors and selectors automatically.