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

Is there a way to prove properties about my C++ programs?

本文关键字：程序属性 C++ 我的证明有没有更新时间：2023-10-16

我理解像Coq和Idris这样的语言可以用来证明用这些语言编写的程序的属性(根据我在这个问题上的一点经验来看(，但我想知道是否有一种平易近人的方法可以在已经存在的代码库上从外部做同样的事情。

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

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

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

其他有趣的工具包括上面评论中提到的Frama-C和来自Microsoft的静态分析仪VCC。但是，它们不适用于C++。