Back to Search
Start Over
VDM recursive functions in Isabelle/HOL
- Publication Year :
- 2023
-
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.
- Subjects :
- Computer Science - Formal Languages and Automata Theory
Subjects
Details
- Database :
- arXiv
- Publication Type :
- Report
- Accession number :
- edsarx.2303.17457
- Document Type :
- Working Paper