Jak*_*old 12 c++ verification coq proof-of-correctness
我理解像Coq和Idris这样的语言如何用于证明用这些语言编写的程序的属性(根据我在该主题中的一点经验来判断.)但是我想知道是否有一种平易近人的方式在外部做同样的事情,在现有的代码库.
有没有办法使用像Coq或其他专业工具这样的工具来证明用C++编写的算法的正确性？如果是这样,这样做有什么要求？
这取决于"证明财产"的含义.据我所知,有许多静态分析工具可用于检查C程序的简单属性,它们在表现力,易用性,分析的可靠性等方面差异很大.它们通常用于检查程序是否免费运行时错误,但不是很好检查完整的功能规范.对于这种属性,您可能不得不诉诸一个更强大的证明器,要求您手动记下证明,而不是自动检查一个.
既然你提到Coq,我想推荐你使用两个基于Coq的工具来验证C程序(但是它们不适用于C++):在后一类中,有一个Verified Software Toolchain,一个推理逻辑嵌入在Coq中的C程序.您可以使用它来编写有关程序行为的证据,并让Coq检查它们,包括显示程序是否符合其功能规范.在前一类中,有Verasco,一种自动静态分析工具,可以检查程序是否存在运行时错误.这些工具的一个很好的特性是它们本身就是经过验证的程序,这意味着您可以对它们提供的分析有更大的信心.
其他有趣的工具包括上面评论中提到的Frama-C和微软的静态分析仪VCC.但是,它们不适用于C++.