问比较契约式设计与类型系统

EN

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

似乎大多数答案都假设合同是动态检查的。请注意，在某些系统中，合同是静态检查的。在这样的系统中，您可以将合同看作是可以自动检查的依赖类型的受限形式。这与更丰富的依赖类型形成对比，后者是以交互方式检查的，例如在Coq中。

有关Dana Xu's page和OCaml合同的静态和混合检查(先静态后动态)的论文，请参阅Haskell上的“规范检查”部分。徐的契约体系包括精化类型和从属箭头，两者都是从属类型。自动检查受限依赖类型的早期语言包括Pfenning和Xi的DML和ATS。在DML中，与Xu的工作不同，依赖类型受到限制，因此自动检查是完整的。

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

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