有没有办法证明我的 C++ 程序的属性？

Posted 2023-02-19

【中文标题】有没有办法证明我的 C++ 程序的属性？

【英文标题】：Is there a way to prove properties about my C++ programs?

【发布时间】：2015-02-12 17:23:36

【问题描述】：

我了解如何使用 Coq 和 Idris 之类的语言来证明用这些语言编写的程序的属性（根据我在该主题上的一点经验来判断。），但我想知道是否有一种平易近人的方法可以在外部做同样的事情，在已经存在的代码库。

有没有办法使用像 Coq 这样的工具或其他一些专门的工具来证明用 C++ 编写的算法的正确性？如果是这样，这样做的要求是什么？

【问题讨论】：

对于 C，有Frama-C，它试图推理程序的行为。如果您的代码算法代码与C兼容/可编译为C，您也许可以使用它。

【参考方案1】：

这取决于“证明属性”的含义。据我所知，用于检查C程序简单属性的静态分析工具有很多，它们在表达性、易用性、分析的合理性等方面差异很大。它们通常用于检查程序是否免费运行时错误，但对于检查完整的功能规范不是很好。对于此类属性，您可能不得不求助于更强大的证明者，该证明者需要您手动写下证明，而不是自动为您检查。

既然您提到了 Coq，我想向您推荐两个基于 Coq 的工具来验证 C 程序（但是它们不适用于 C++）：在后一类中，有 Verified Software Toolchain，一个逻辑用于推理嵌入在 Coq 中的 C 程序。您可以使用它来编写有关程序行为的证明并让 Coq 检查它们，包括证明程序符合其功能规范。在前一类中，有Verasco，这是一种自动静态分析工具，可以检查您的程序是否存在运行时错误。这些工具的一个很好的特点是它们本身就是经过验证的程序，这意味着您可以对它们提供的分析更有信心。

其他有趣的工具包括Frama-C，如上面评论中所述，以及VCC，微软的静态分析器。但是，它们不适用于 C++。