design-by-contract - 使用最广泛的使用契约式设计的开源项目是什么？

Question

我很好奇在 Eiffel 社区之外的实践中使用了多少按契约(Contract)设计。是否有任何使用契约(Contract)设计的活跃开源项目？

或者，将问题重新定义为一个只有一个答案的问题:使用最广泛使用的(非埃菲尔的)使用契约(Contract)设计的开源项目是什么？

Answer 1

您问题的“非埃菲尔”部分很有趣。当编程语言支持契约时，契约就发挥了所有的意义，否则它只是一个很好的注释语法。

这将我们带到了支持合约的语言。除了埃菲尔，我知道三个:

ESC/Java使用名为 JML 的语言向 Java 添加契约.

.NET contracts适用于所有 .NET 语言(在字节码级别工作)

Frama-C使用语言 ACSL 向 C 添加契约

前两个有可执行的合约。优点:可以作为运行时断言。缺点:缺乏完全指定功能在合约中做什么的表达能力。您基本上只能编写健全性检查。

另一方面，ACSL 契约(Contract)更具表现力，且不可执行。它们可以完全指定排序函数应始终终止，并按顺序保留与原始数组中相同的元素。 ACSL 合约可用于静态分析，尤其是 Hoare 风格的最弱前提计算。

并且只有真正熟悉最后一个(免责声明:我在 Frama-C 上工作，但 ACSL 部分是很多人的工作，其中一些人的贡献比我多得多)，我只能提到“ACSL by示例”，一个带有 ACSL 契约(Contract)的开源 C 库，目前由 Fraunhofer FIRST 开发。它尚未发布，但将作为 Device-soft 的一部分项目。如果您有兴趣，我相信您可以获得初步版本。请随时联系最后一个网页上提到的联系人。