Сравнение дизайна по контракту с типами систем

Недавно я прочитал документ, в котором сравнивались "Контракт-контракт" с Test-Driven-Development. Кажется, что много перекрытий, некоторая избыточность и немного синергии между DbC и TDD. Например, существуют системы автоматического генерации тестов на основе контрактов.

Каким образом DbC перекрывается с современной системой типов (например, в haskell или на одном из этих языков с типичным типом), и есть ли точки, в которых использование обоих вариантов лучше, чем либо?

Ответы

Ответ 1

В статье "Типированные контракты для функционального программирования" Ральфа Хинзе, Йохана Журинга и Андреса Лёха была эта удобная таблица, которая иллюстрирует, где заключаются контракты о местонахождении в спектре "проверки":

                   |   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

Ответ 2

Основные различия заключаются в том, что тестирование является динамическим и неполным, полагаясь на измерение, чтобы дать доказательства того, что вы полностью подтвердили, какое свойство вы тестируете, в то время как типы и typechecking - это формальная система, которая гарантирует, что все возможные пути кода были проверены против любых свойство, которое вы указываете в типах.

Тестирование свойства может только приближаться к пределу уровня уверенности, проверка типа для того же самого свойства предоставляется из коробки. Контракты увеличивают базовую линию для динамической проверки.

Ответ 3

Кажется, большинство ответов предполагает, что контракты проверяются динамически. Обратите внимание, что в некоторых системах контракты проверяются статически. В в таких системах вы можете рассматривать контракты как ограниченную форму зависимые типы, которые могут быть проверены автоматически. Сравните это с более богатыми зависимыми типами, которые проверяются в интерактивном режиме, например в Coq.

См. раздел "Проверка спецификаций" на странице Страница Dana Xu для документы по статической и гибридной проверке (статические с последующим динамическим) контракты на Haskell и OCaml. Контрактная система Сю включает в себя типы уточнения и зависимые стрелки, оба из которых зависят типы. Ранние языки с ограниченными зависимыми типами, которые автоматически проверяется: DML и ATS Пфеннинг и Си. В DML, в отличие от работы Xu, зависимые типы ограничены, поэтому что автоматическая проверка завершена.

Ответ 4

DBC ценен, если вы не можете выразить все предположения в самом систере типа. Простой пример haskell:

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

Тип:

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

Тем не менее, только значения больше равны 0 для n. Здесь DBC может вмешаться и, например, создать соответствующие свойства quickcheck.

(Конечно, в этом случае слишком легко проверить также отрицательные значения и исправить результат, отличный от undefined, но есть более сложные случаи.)