VDM recursive functions in Isabelle/HOL
| Autor: | Freitas, Leo, Larsen, Peter Gorm |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. |
| Databáze: | arXiv |
| Externí odkaz: |
|