我目前正在解决模型转换的正确性问题。我阅读了很多文章，发现Isabelle定理证明者是解决该问题的不错选择。现在，我想使用Isabelle定理证明者进行分析和验证。但是我不知道如何使用Isabelle自己的语言标准将我的建模语言（包括源模型，目标模型，转换本身）形式化。换句话说，我想快速学习Isabelle的形式语言来描述我的建模语言。我在官方网站上下载了许多文档，但无法确定如何快速入门。我希望该领域的研究人员可以为初学者提供一些建议，非常感谢。
我会推荐具体的语义书：
http://concrete-semantics.org/
它教您如何在Isabelle中为小型编程语言建模以及如何指定其语义。
我想这种方法对于建模语言将是相似的。
1。使用代数数据类型描述源语言和目标语言的抽象语法。2.定义两者的语义。3.将转换定义为函数。