Ada/SPARK：我应该使用 GNATprove 吗？我在哪里可以找到它？

Question

在Learning Ada的第 22.1 章中，尝试构建示例。

它期望安装 GNATprove。我使用的是 Ubuntu 18.04 LTS，但没有看到任何提供它的软件包。当我尝试查找主存储库时，我发现的只是Open Do中的内容，当我单击下载按钮时，它似乎是一个损坏的链接。Google 几乎没有提供有关 GNATprove 的信息，这有点令人担忧。

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

Answer 1

GNATprove 是用于 SPARK 形式化验证的工具，即 Ada 的可证明子集。如果您想构建可靠的软件并确保它做正确的事情，那么 SPARK 当然值得一看！

获得 SPARK 的最简单方法是使用Alire安装社区版。或者，您可以从GitHub手动下载并安装 GNATprove 。更多详细信息可以在GitHub 上的 SPARK 项目中找到。社区版拥有您开始使用 Ada 和 SPARK 所需的一切。“Pro”的主要区别在于商业支持。