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

Question

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

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

Answer 1

您可以dafny.exe从 python 调用，将包含您希望验证的 dafny 程序的文件名作为参数传递。请参阅有关如何从 python 调用外部命令的其他答案。

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

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

你可能想看看这个项目的代码，它做了类似的事情，但来自 Java。