Ada/SPARK : should I be using GNATprove? 我在哪里可以找到它？

Question

关于本文的第 22.1 章 Learning Ada ，尝试构建示例。

它期望安装 GNATprove。我使用的是 Ubuntu 18.04 LTS，但没有看到任何提供它的软件包。当我试图找到主仓库时，我发现的只是 Open Do ，当我单击下载按钮时，它似乎是一个损坏的链接。 Google 对 GNATprove 几乎没有什么可提供的，这有点令人担忧。

我是 Ada 的新手，所以我真的不知道我应该使用什么，所以如果 GNATprove 不是正确的东西，请告诉我。我通常还期待一个免费的软件工具链——这是一个合理的期望还是我应该期望需要“专业”版本来了解 Ada/SPARK 的全部内容？

Answer 1

GNATprove 是 the tool used for the formal verification of SPARK ，即 Ada 的可证明子集。如果您想构建可靠的软件并确保它做正确的事情，那么 SPARK 肯定值得一看!

让您接触 SPARK 的最简单方法是从 https://www.adacore.com/download 下载 GNAT 社区版其中包括 GNATprove。社区版拥有您开始使用 Ada 和 SPARK 所需的一切。 “Pro”的主要区别在于商业支持。