将契约设计与类型系统进行比较

Question

我最近读了一篇论文，将合同设计与测试驱动开发进行了比较。 DbC 和 TDD 之间似乎有很多重叠、一些冗余以及一些协同作用。例如，有基于合同自动生成测试的系统。

DbC 以什么方式与现代类型系统重叠（例如在 haskell 中，或其中一种依赖类型的语言），并且使用两者是否比其中任何一个更好？

Answer 1

Ralf Hinze 的论文函数式编程的类型化合约， Johan Jeuring 和 Andres Löh 制作了这张方便的表格，说明了合同在“检查”设计范围中的位置：

                   |   static checking    |   dynamic checking
-------------------------------------------------------------------
simple properties  | static type checking | dynamic type checking
complex properties | theorem proving      | contract checking

Answer 2

似乎大多数答案都假设合约是动态检查的。
请注意，在某些系统中，合约是静态检查的。在
在此类系统中，您可以将合同视为一种受限制的形式
可以自动检查的依赖类型。对比一下这个
具有更丰富的依赖类型，可以交互检查，例如
在柯克。

请参阅 Dana Xu 页面 上的“规格检查”部分，了解
关于静态和混合检查（静态后动态）的论文
Haskell 和 OCaml 的合同。徐氏的契约制度包括
细化类型和依赖箭头，两者都是依赖的
类型。具有受限依赖类型的早期语言是
自动检查包括 DML 和 ATS。
在 DML 中，与 Xu 的工作不同，依赖类型受到限制，因此
自动检查完成。

Answer 3

主要区别在于，测试是动态且不完整的，依赖于测量来证明您已经完全验证了您正在测试的任何属性，而类型和类型检查是一个正式的系统，可确保所有可能的代码路径都已针对您正在测试的任何属性进行了验证以类型说明。

对属性的测试只能达到同一属性的类型检查提供的开箱即用的保证级别的限制。合同增加了动态检查的基线。

Answer 4

只要您无法表达类型系统本身的所有假设，DBC 就很有价值。简单的 haskell 示例：

take n [] = []
take 0 _  = []
take n (a:as) = take (n-1) as

类型为：

take :: Int -> [a] -> [a]

然而，对于 n 来说，只有大于等于 0 的值才可以。这是 DBC 可以介入的地方，例如，生成适当的快速检查属性。

（当然，在这种情况下，检查负值并修复除未定义之外的结果也太容易了 - 但还有更复杂的情况。）

Answer 5

我认为DbC和type的系统没有可比性。 DbC 和类型系统（甚至验证系统）之间存在混淆。例如，我们可以找到比较DbC和Liquid Haskell工具或DbC和QuickCheck框架。恕我直言，这是不正确的：类型的系统以及形式证明系统只断言一个 - 你：你在我们的脑海中有一些算法，并且你声明了这些算法的属性。然后你实现这些算法。类型系统以及形式证明系统验证实现代码是否对应于声明的属性。

DbC 验证的不是内部事物（实现/代码/算法），而是外部事物：代码外部事物的预期功能。它可以是环境、文件系统、数据库、调用者的状态，当然还有你自己的状态，任何东西。典型的合约在运行时工作，而不是在编译时或特殊验证阶段。

DbC 的规范示例显示了如何在 HP 芯片中发现错误。发生这种情况是因为 DbC 声明了外部组件的属性：芯片的属性、其状态、转换等。如果您的应用程序遇到意外的外部世界状态，它会将这种情况报告为异常。这里的神奇之处在于：1）您在一个地方定义合约并且不要重复自己2）合约可以轻松关闭（从编译的二进制文件中删除）。恕我直言，它们更接近方面，因为它们不像子例程调用那样“线性”。

我在这里回顾一下，DbC 比类型系统更有助于避免现实世界的错误，因为大多数真正的错误是由于对外部世界/环境/框架/操作系统组件/等的行为的误解而发生的。类型和证明帮助仅有助于避免您自己的简单错误，这些错误可以通过测试或建模（在 MatLab、Mathematica 等中）发现。

简而言之：您无法在具有类型系统的 HP 芯片中找到错误。当然，存在一种幻觉，认为索引单子之类的东西是可能的，但具有这种尝试的真实代码将看起来超级复杂、不支持且不实用。但我认为可能存在一些混合方案。