什么使通过合同进行设计成为一种工具？

Question

合同式设计基于Hoare逻辑，通过前后条件和不变量的推理来证明程序的正确性。

使这种推理成为可能的语言的手段和先决条件是什么？

可以静态地检查它，还是它只是运行时断言的一种形式？

Answer 1

在回答第一个问题时，设计或扩展支持DbC的语言似乎没有任何障碍。然而，DbC不仅向语言引入了断言，而且还引入了一组规则，这些规则告诉我们如何在存在(多个)继承和重声明的情况下组合这些断言。因此，除非语言工具知道如何执行注释，否则简单的注释无法轻松地转换为可执行代码。

至于第二个问题，最初通过合同设计的™是在埃菲尔引入的，实际上是为了运行时检查。随着时间的推移，出现了一些变化，我只想提及其中的一些变化：

1. 定期汇编。在一段时间内，埃菲尔特征所谓的无效安全，即保证永远不会调用Void目标(即NullReferenceException类型的例外是不可能的)。这项技术依赖于一些规则。为了使无效安全的编程变得可行，并且接近于常规程序员的推理，它们涉及某种形式的断言。例如，触发异常的方法在表单False中具有后置条件，以指示调用此类方法之后的任何代码都是不可访问的。然后编译器知道在这样的调用之后没有理由检查无效的安全规则，因为它永远不会被执行。
2. 测试生成。通过查看规范，先决条件和后置条件可以作为自动生成测试的良好基础。当静态分析在运行时参与测试生成和测试执行检查断言时，这种技术是静态和动态方法的混合体。这种工具的一个例子是AutoTest。
3. 代码验证。一些不同语言的验证工具依赖于DbC规范来证明正确性。对于Java，它是JML，对于埃菲尔- AutoProof。在后者的当前网页中，您可以找到一个指向在线版本的链接，该链接提供了一些示例，您可以尝试找出示例代码的错误所在并修复它。它利用DbC，并使用一些模型类来严格描述容器的行为，形式为正常的前后条件。分析是完全静态的，也就是说，如果工具说所有断言都是满意的，那么在运行时就不会出现断言冲突，并且断言检查可以安全地关闭。