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

Question

我正在研究几个C项目,我想使用自动定理证明来验证代码.理想情况下,我只想使用ATP来验证函数契约.C/gcc或外部软件/软件包/等中是否有任何功能可以实现按合同样式编码？

如果没有那么那只是激励我自己开始.

我对此的引用类似于Spec#或来自MSR的Sing#,但我是一个开源人员,我正在寻找开源解决方案.

Answer 1

开源:检查.

自动定理证明:检查.

你应该非常喜欢Frama-C及其ACSL规范语言.您可能已经听说过它的Caduceus祖先,但此时它被Frama-C/Jessie取代.

Answer 2

显然它没有内置到该语言中，但是有很多附加组件可以帮助您继续前进。其中大多数都是测试版 - 但您可能会考虑为它们做出贡献，而不是创建自己的。

RubyForge 的Design by Contract for C看起来非常有前途。GNU Nana已经存在很长时间了，可能会很好地满足您的需求。希望这些有帮助。

编辑：查看O'Reily 上有关 C 的契约设计的文章：

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