The proof assistant Isabelle/HOL is made available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. Following the techniques in [9] and the theoretical groundwork in [4], we show the major milestones for the implementation of a B-Tool and the resulting refinement method inside the Isabelle/HOL platform. The prototype HOL-B provides IDE support, documentation support, a theory for the Z-Mathematical Toolkit underlying the B-Method, and a generated denotational semantics for a B MACHINE specification implemented as a specification construct in Isabelle/HOL. Extended by more automated proof machinery geared to refinements, HOL-B can serve as a more portable, flexible and extensible tool for Event-B that may profit from the large Isabelle/HOL libraries providing Algebra and Analysis theories.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{BallenghienW24,
author = {Beno{\^{\i}}t Ballenghien and
Burkhart Wolff},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Event-B as {DSL} in Isabelle and {HOL} Experiences from a Prototype},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {241--247},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_18},
doi = {10.1007/978-3-031-63790-2\_18},
timestamp = {Fri, 19 Jul 2024 23:15:46 +0200},
biburl = {https://dblp.org/rec/conf/zum/BallenghienW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}