用 C 语言进行契约设计，用于自动定理证明
我正在开发几个 C 项目，我想使用自动定理证明来验证代码。 理想情况下，我只想使用 ATP 来验证函数契约。 C/gcc 或外部软件/软件包/等中是否有任何功能可以实现合同设计风格编码？
如果没有，那就是我自己开始的动力。
我对此的参考资料类似于 MSR 的 Spec# 或 Sing#，但我是一个开源人士，我正在寻找开源解决方案。
I'm working on a couple of C projects and I'd like to use automated theorem proving to validate the code. Ideally I'd just like to use the ATP to validate the functions contracts. Is there any functionality in C/gcc or external software/packages/etc that would enable design-by-contract style coding?
If not then thats just incentive to get started on my own.
My references for this would be something like Spec# or Sing# from MSR, but I'm an open source guy and I'm looking for open source solutions.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
开源：检查。
自动定理证明：勾选。
您应该非常喜欢 Frama-C 及其 Frama-C 。 cea.fr/acsl.html" rel="noreferrer">ACSL 规范语言。 您可能已经听说过它的 Caduceus 祖先，但目前它被认为已被 Frama-C/Jessie 取代。
Open-Source:check.
Automated Theorem Proving:check.
You should really like Frama-C and its ACSL specification language. You might have already heard about its Caduceus ancestor, but at this time it is considered superseded by Frama-C/Jessie.
显然它没有内置到该语言中，但是有很多附加组件可以帮助您继续前进。 其中大多数都是测试版 - 但您可能会考虑为它们做出贡献，而不是创建自己的。
RubyForge 的Design by Contract for C看起来非常有前途。 GNU Nana 已经存在很长时间了，可能会很好地满足您的需求。 希望这些有帮助。
编辑：查看O'Reily 的这篇文章 关于 C 的合同设计：
Obviously it is not built into the language, but there are plenty of add-ons to get you going. Most of them are beta - but you might consider contributing to them rather than starting your own.
The one at RubyForge, Design by Contract for C, looks very promising. GNU Nana has been around for a long time and will probably suit your needs fine. Hope these are helpful.
Edit: Check out this article at O'Reily on Design By Contract for C:
如果您有兴趣使用定理证明器验证 C 代码，您应该查看 VCC 项目。
从他们的网页：
VCC是微软研究院非常成熟的系统，已用于验证Microsoft Hyper-V。
VCC 也是开源的。
If you are interested in validating C code using theorem provers, you should check the VCC project.
From their webpage:
VCC is very mature system from Microsoft Research, and has been used to verify the hypervisor of Microsoft Hyper-V.
VCC is also open source.