c - C 语言中的契约式设计，用于自动定理证明

Question

我正在处理几个 C 项目，我想使用自动定理证明来验证代码。理想情况下，我只想使用 ATP 来验证功能合同。C/gcc 或外部软件/包/等中是否有任何功能可以实现按合同设计风格的编码？

如果不是，那只是我自己开始的动力。

我对此的参考可能是来自 MSR 的 Spec# 或 Sing#，但我是一名开源人员，我正在寻找开源解决方案。

Answer 1

开源：检查。

自动定理证明：检查。

您应该非常喜欢Frama-C及其ACSL规范语言。您可能已经听说过它的 Caduceus 祖先，但目前它被认为已被 Frama-C/Jessie 取代。

Answer 2

显然它没有内置在语言中，但是有很多附加组件可以让您继续前进。它们中的大多数是测试版——但您可能会考虑为它们做出贡献，而不是自己开始。

RubyForge的 C 合同设计，看起来很有前途。GNU Nana已经存在了很长时间，可能会很好地满足您的需求。希望这些是有帮助的。

编辑：在 O'Reily 上查看这篇关于 C 合同设计的文章：

对 assert() 不满意并对契约式设计感到兴奋，我开始为 C 创建自己的契约式设计实现。在查看了一些可用于 Java 1的解决方案后，我决定使用对象约束语言的一个子集来快递合同[4]。使用 Ruby 和 Racc，我为 C 创建了 Design by Contract，这是一个代码生成器，可以将嵌入在 C 注释中的合同转换为 C 代码以检查合同。

Answer 3

如果您对使用定理证明器验证 C 代码感兴趣，您应该查看VCC 项目。从他们的网页：

VCC 是并发 C 程序的机械验证器。VCC 采用一个 C 程序，用函数规范、数据不变量、循环不变量和幽灵代码进行注释，并尝试证明这些注释是正确的。如果成功，VCC 承诺您的程序实际上符合其规范。

VCC 是微软研究院非常成熟的系统，已经用于验证微软 Hyper-V的管理程序。VCC 也是开源的。