问使用伊莎贝尔定理证明程序的过程是在编程模式下编码，然后在证明模式下被验证吗？

EN

我不确定我是否理解你的问题，但我会尽力回答它的一部分。

然而，

在形式化建模语言时遇到了一些问题。

你能澄清你遇到的问题，或者给出一个你想要形式化的建模语言的具体例子吗？

应该在编程模式下自编一个带有.thy后缀的理论文件，然后在验证模式下运行它以获得正确性的证明吗？

Isabelle没有单独的编程和验证模式。您可以将函数定义和引理混合在同一个.thy文件中。

正确性的大部分方面都是在引理/定理中完成的，但是即使您只是在Isabelle中定义了递归函数，您也已经得到了一些正确性的保证:您需要证明您的定义是定义良好的。

伊莎贝尔有许多编码字段，如数据类型、常数、函数、定义、引理和定理。我是否应该分别对这些代码进行编码以证明模型转换的正确性？

正如我前面所说，您不需要将它们分离到不同的文件中。然而，一切都必须按照伊莎贝尔的顺序来定义。例如，如果要证明函数的某些内容，则必须在源代码中的引理之前定义该函数。如果函数在某些数据结构上工作，则对应的类型定义必须在函数之前。