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

Question

我很好奇在Eiffel社区之外的实践中使用了多少契约式设计。有没有使用契约式设计的开放源码项目？

或者，将这个问题改写成一个只有一个答案的问题:使用契约式设计的最广泛使用的(非Eiffel)开源项目是什么？

Answer 1

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

这就把我们带到了支持契约的语言。除了埃菲尔，我只知道三个：

• ESC/Java使用名为JML.
• .NET contracts的语言为所有Java语言添加约定(在字节码上工作level)
• Frama-C使用ACSL

语言向C添加约定

前两个都有可执行的合同。优点:可以作为运行时断言使用。缺点:缺乏表达能力，无法完全指定函数在契约中的作用。基本上，您只能编写健全性检查。

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

只有对最后一个非常熟悉(免责声明:我在Frama-C上工作，但ACSL部分是很多人的工作，其中一些人的贡献比我多得多)，我只能提到"ACSL by example"，这是一个开源的C库，目前由Fraunhofer首先开发了ACSL合同。它还没有发布，但它将作为Device-soft项目的一部分。如果你感兴趣的话，我相信你可以得到一个初步的版本。请随时与最后一个网页上提到的联系人联系。