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

Question

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

或者，将问题重铸为一个只有一个答案的问题：使用按合同设计的最广泛使用的（非埃菲尔）开源项目是什么？

Answer 1

您问题的“非埃菲尔”部分很有趣。当编程语言支持合同时，合同就会发挥其全部意义，否则它只是一种很好的注释语法。

这将我们带到了支持合同的语言。我知道除了埃菲尔之外的三个：

• ESC/Java使用名为JML的语言向 Java 添加合同。
• 适用于所有 .NET 语言的.NET 合约（在字节码级别工作）
• Frama-C使用语言ACSL将合约添加到 C

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

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

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