Dafny 可以以非交互方式使用，例如从 python 程序中使用吗？

Question

我想查询某个特定的 Dafny 程序是否进行了验证。 Dafny 通常用于在 Visual Studio IDE 中以交互方式开发程序。

但是，我需要以非交互方式执行查询。特别是我需要从 python 程序中查询 Dafny。这可能吗？

Answer 1

您可以从 python 调用dafny.exe，将包含您希望验证的 dafny 程序的文件名作为参数传递。请参阅此other answer on how to call external commands from python。

您可以通过使用/? 开关运行dafny.exe 来获得有关dafny 命令行参数的帮助。

您需要解析 dafny 的输出以确定验证是否成功。 dafny test suite 以这种方式工作。

您可能想查看 code of this project，它执行类似的操作，但来自 Java。