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

Question

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

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

Answer 1

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

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

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