Недавно я прочитал документ, в котором сравнивались "Контракт-контракт" с Test-Driven-Development. Кажется, что много перекрытий, некоторая избыточность и немного синергии между DbC и TDD. Например, существуют системы автоматического генерации тестов на основе контрактов.
Каким образом DbC перекрывается с современной системой типов (например, в haskell или на одном из этих языков с типичным типом), и есть ли точки, в которых использование обоих вариантов лучше, чем либо?
В статье "Типированные контракты для функционального программирования" Ральфа Хинзе, Йохана Журинга и Андреса Лёха была эта удобная таблица, которая иллюстрирует, где заключаются контракты о местонахождении в спектре "проверки":
| static checking | dynamic checking
-------------------------------------------------------------------
simple properties | static type checking | dynamic type checking
complex properties | theorem proving | contract checking
Смотрите здесь:
Основные различия заключаются в том, что тестирование является динамическим и неполным, полагаясь на измерение, чтобы дать доказательства того, что вы полностью подтвердили, какое свойство вы тестируете, в то время как типы и typechecking - это формальная система, которая гарантирует, что все возможные пути кода были проверены против любых свойство, которое вы указываете в типах.
Тестирование свойства может только приближаться к пределу уровня уверенности, проверка типа для того же самого свойства предоставляется из коробки. Контракты увеличивают базовую линию для динамической проверки.
Кажется, большинство ответов предполагает, что контракты проверяются динамически. Обратите внимание, что в некоторых системах контракты проверяются статически. В в таких системах вы можете рассматривать контракты как ограниченную форму зависимые типы, которые могут быть проверены автоматически. Сравните это с более богатыми зависимыми типами, которые проверяются в интерактивном режиме, например в Coq.
См. раздел "Проверка спецификаций" на странице Страница Dana Xu для документы по статической и гибридной проверке (статические с последующим динамическим) контракты на Haskell и OCaml. Контрактная система Сю включает в себя типы уточнения и зависимые стрелки, оба из которых зависят типы. Ранние языки с ограниченными зависимыми типами, которые автоматически проверяется: DML и ATS Пфеннинг и Си. В DML, в отличие от работы Xu, зависимые типы ограничены, поэтому что автоматическая проверка завершена.
DBC ценен, если вы не можете выразить все предположения в самом систере типа. Простой пример haskell:
take n [] = []
take 0 _ = []
take n (a:as) = take (n-1) as
Тип:
take :: Int -> [a] -> [a]
Тем не менее, только значения больше равны 0 для n. Здесь DBC может вмешаться и, например, создать соответствующие свойства quickcheck.
(Конечно, в этом случае слишком легко проверить также отрицательные значения и исправить результат, отличный от undefined, но есть более сложные случаи.)