将合同设计与类型系统进行比较

Question

我最近阅读了一篇文章,将"按合同设计"与"测试驱动开发"进行了比较.似乎有很多重叠,一些冗余,以及DbC和TDD之间的一点协同作用.例如,有一些系统可以根据合同自动生成测试.

DbC以什么方式与现代类型系统重叠(例如在haskell中,或者是那些依赖类型的语言之一)并且有两点使用两者都比哪一方更好？

Answer 1

Ralf Hinze,Johan Jeuring和AndresLöh撰写的"键入功能编程合同"这篇论文有一个方便的表格,说明了行踪合同在"检查"的设计范围内的作用:

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

看这里:

http://people.cs.uu.nl/andres/Contracts.html

Answer 2

似乎大多数答案都假设合同是动态检查的.请注意,在某些系统中,会静态检查合同.在这样的系统中,您可以将合约视为受限类型的依赖类型,可以自动检查.将此与更丰富的依赖类型进行对比,这些类型以交互方式进行检查,例如在Coq中.

有关Haskell和OCaml合同的静态和混合检查(静态跟随动态)的论文,请参阅Dana Xu页面上的"规范检查"部分.Xu的合同系统包括细化类型和从属箭头,两者都是依赖类型.具有自动检查的受限类型的早期语言包括Pfenning和Xi 的DML和ATS.在DML中,与Xu的工作不同,依赖类型受到限制,因此自动检查已完成.

Answer 3

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

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