c - 用 C 语言进行契约(Contract)设计，用于自动定理证明

Question

我正在处理几个 C 项目，我想使用自动定理证明来验证代码。理想情况下，我只想使用 ATP 来验证功能契约(Contract)。 C/gcc 或外部软件/软件包/等中是否有任何功能可以启用按契约(Contract)设计样式编码？

如果没有，那就是我自己开始的动力。

我对此的引用类似于 MSR 的 Spec# 或 Sing#，但我是一个开源人士，我正在寻找开源解决方案。

Answer 1

开源:检查。

自动定理证明:检查。

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