1

我的问题是关于 Boogie，但由于没有可用的 Boogie 标签，我使用 dafny 标签作为与 Boogie 密切相关的标签。

我按照文档中的说明在 Visual Studio 上构建了 Boogie。接下来我应该做什么来编写 Boogie 代码或等效地如何运行 Test 文件夹中的 .bpl 文件？据我了解，Boogie 虽然是一种中间验证语言，但也可以独立使用。

谢谢你。

4

2 回答 2

1

Boogie 没有交互式 VS 模式。如果您想在编辑器中编写 Boogie 代码并获得设计时反馈，那么可用的最佳模式是在 emacs 中，请参阅https://github.com/boogie-org/boogie-friends。不过，这种 emacs 模式不会给您错误跟踪或验证调试器信息。

于 2017-03-20T22:43:16.260 回答
0

Boogie 依赖于Z3，因此请确保它可用。

然后，从命令行：

  • boogie.exe /help
  • boogie.exe file_to_verify.bpl
于 2017-03-20T08:19:16.400 回答