VDM recursive functions in Isabelle/HOL
Formal Languages and Automata Theory
2023-03-31 v1
Abstract
For recursive functions general principles of induction needs to be applied. Instead of verifying them directly using the Vienna Development Method Specification Language (VDM-SL), we suggest a translation to Isabelle/HOL. In this paper, the challenges of such a translation for recursive functions are presented. This is an extension of an existing translation and a VDM mathematical toolbox in Isabelle/HOL enabling support for recursive functions.
Cite
@article{arxiv.2303.17457,
title = {VDM recursive functions in Isabelle/HOL},
author = {Leo Freitas and Peter Gorm Larsen},
journal= {arXiv preprint arXiv:2303.17457},
year = {2023}
}