Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection
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 Featherweight
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.