dafny - Dafny 中的导入、包含和验证之间的关系是什么？

Question

我知道一个 Dafny 源文件可以包含在另一个文件中，从而在验证之前导致文件的文本连接。但是对于包含、导入以及何时验证哪些文件之间的关系，我没有清晰的心智模型。也许专家可以详细说明。谢谢。

Answer 1

这至少部分记录在Dafny 参考手册的各个部分中。

第 2.0 节讨论include：

包含的文件也遵守 Dafny 语法。Dafny 解析和处理原始源文件和所有包含文件的传递闭包，但不会在这些文件上调用验证程序，除非它们已在命令行中明确列出。

（强调我的）

3.1 节讨论了import，这是 Dafny 模块系统的一个特点。您只能import在模块内部使用，以使另一个模块中的定义可用。请注意，与其他一些语言不同，Dafny 模块系统独立于文件在磁盘上的存储方式。因此，如果您要导入的模块是在另一个文件中定义的，那么如果您还没有包含该文件，则可能必须包含该文件。

import对导入的模块是否验证没有直接影响。除非它们的文件在命令行中列出，否则不会验证其他文件中的模块。当前文件中的模块总是经过验证（无论它们是否被任何人导入）。