如何快速入门Isabelle的形式化语言标准来形式化描述建模语言？

Question

我目前正在解决模型转换正确性的问题。我看了很多文章，发现伊莎贝尔定理证明器是解决问题的好选择。现在想用伊莎贝尔定理证明器进行分析验证。但我不知道如何用 Isabelle 自己的语言标准 形式化我的建模语言（包括源模型、目标模型、转换本身）。换句话说，我想快速学习伊莎贝尔的正式语言来描述我的建模语言。我在官网上下载了很多文档，但始终无法确定如何快速上手。希望该领域的研究人员能给初学者一些建议，非常感谢。

Answer 1

推荐具体语义书：

http://concrete-semantics.org/

它教您如何在 Isabelle 中对小型编程语言建模以及如何指定其语义。

我想建模语言的方法与此类似。

1.Describe 使用代数数据类型的源语言和目标语言的抽象语法。 2. 定义两者的语义。 3. 将转换定义为函数。