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


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.


UML, OCL, Formal Semantics, Isabelle/HOL, Reflection


OCL 2014

Article complet

Projet IRT

Projet FSF

Inscrivez-vous à la newsletter de l'IRT SystemX

et recevez chaque mois les dernières actualités de l'institut :