Isabelle/HOL中的VDM递归函数
摘要：递归函数的一般归纳原理需要应用。我们建议将其从维也纳开发方法规范语言（VDM-SL）直接翻译到Isabelle/HOL进行验证。本文介绍了在翻译递归函数时面临的挑战。这是对现有翻译的扩展，同时也是在Isabelle/HOL中支持递归函数的VDM数学工具的一个示例。
作者：Leo Freitas, Peter Gorm Larsen
论文ID：2303.17457
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-03-31