Audience
- Romain Aissat
- Thibaut Balabonski
- Frédéric Boulanger
- Chantal Keller
- Yakoub Nemouchi
- Hai Nguyen Van
- Benoît Valiron
- Burkhart Wolff
Project
Frédéric Tuong
Introduction
In this talk, Frederic introduced his work about the automation of a translation process from a subset of the language UML/OCL to a subset of the language Isabelle. The translation process is formally implemented in Isabelle/HOL, so both AST (or Meta-Model) in input and in output are described by means of Isabelle/HOL datatypes.
The Translation Process
The general process one can follow to secure the semantics of a language is to shallow embed it into some theorem prover (which we assume trusted in the experimenting context). However shallow embedding UML/OCL in Isabelle/HOL has only been performed for a subset of UML/OCL, because there exist types in UML/OCL that do not seem straightforward to be expressed in higher order logic, and hence in the type system of HOL. While the shallow embedding in HOL of the core calculus of UML/OCL and its basic data-structures (such as boolean, integer, set) has been implemented, a new strategy was furthermore developed for the Object-oriented part, because it manipulates for instance dependent types (to constrain multiplicities of object's accessors). So instead of shallow embedding the Object-oriented calculus part, the considered solution is to deeply embed it (in Isabelle/HOL), as well as deep embedding Isabelle in Isabelle/HOL, so that a mapping can ultimately be established between these two deep embedded representations. Finally, given a UML/OCL file in input, the mapping would automatically produce an Isabelle certificate in output, with a number of properties particularly associated for the given file in input.
More precisely, starting from a particular example of a class model in input, the result of this translation is an Object-oriented Isabelle/HOL theory instantiated for this input, containing among others:
- declarations of class types associated to the UML/OCL classes in input,
- the definition of the universe of these class types,
- different lemmas expressing the semantics of UML/OCL test and cast operations (oclIsTypeOf, oclIsKindOf, oclAsType) as well as the semantics of object attributes that implicitly occur in many forms (as role names, as inheriting attributes, etc).
This translation process could have been implemented directly in SML (in which Isabelle/HOL is written), however Frederic used Isabelle/HOL itself:
- to manipulate the API of Isabelle through some (recursively) typed and abstract datatypes
- to directly reuse libraries provided by the main distribution of Isabelle (formalized red-black trees...) or formalized libraries in the Archive of Formal Proof
- to prove the termination of this translation process, i.e. the termination of the generation of Isabelle certificates
- to check the well-formedness of the UML/OCL Meta-Model (by defining datatypes in Isabelle instead of defining datatypes in SML)
- to directly reuse folding selectors and recursors of Meta-Models, which are automatically generated when defining datatypes in Isabelle
Further investigations would allow to prove general properties on Meta-Models, for example after combining with formalized libraries on lambda-calculus, and to know that the generation of the theory .thy file is automatically well-typed without the need to open it in Isabelle/jEdit, especially relevant when considering resulting .thy file of various size (e.g. 12 classes in input corresponds to 14 Kilo-lemmas in output, for 90 classes we obtain 4 Mega-lemmas).
The implementation of this process required to write by hand two meta-models in Isabelle/HOL: the first one for representing the UML/OCL language, the second one for Isabelle/HOL itself. Then we use the code-generation of Isabelle (namely export_code) to generate these meta-models (together with the translation functions) in all languages that Isabelle supports as targets, so Haskell, OCaml, Scala and SML. By executing the translation process on some provided UML/OCL instances in input, we finally obtain in the hard disk a respective .thy file in output.
Alternatively, to give the user an overview of the final result in an interactive way, this extraction process is directly integrated in Isabelle/jEdit, so that each UML/OCL command can output in the output window what they are going to generate without evaluating generated code (same interactivity as sledgehammer). This is called the deep (exportation) mode. On the other hand, instead of printing in the output window, another mode is provided to directly evaluate in real-time what these UML/OCL commands would have printed. This is the shallow (reflection) mode. In particular, for both deep and shallow modes, the code reflection mechanism (code_reflect) was used to reflect (i.e. export in RAM memory then evaluate) the translation functions into SML, so that the reflected Isabelle Meta-Model in SML can be bound to the Isar API, which stands as the main interface of the raw source code and kernel of Isabelle.
A global view of the translation process
Application
More generally, besides the study of the semantics of languages, the presented translation process can serve to implement tactics during the development of proofs (i.e. writing Isabelle tactics in Isabelle), or as a meta-tool to define new packages or commands. As exercice, Frederic proposed to meta-generate the following Isabelle code shown in a previous meeting:
Isabelle club 23 Sep. 2015 (Ondřej Kunčar and Andrei Popescu, ITP 2015)
As start, one can extend the definition of the command "lemma ⋅" registered in the file Scratch3.thy .