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

Question

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

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

Answer 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

Answer 2

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

. См. Раздел «Проверка спецификаций» на на странице Даны Сюй , где представлены статьи о статической и гибридной проверке (статическая сопровождаетсяпо динамике) контрактов для Haskell и OCaml.Система контрактов Xu включает в себя типы уточнения и зависимые стрелки, которые являются зависимыми типами.Ранние языки с ограниченными зависимыми типами, которые автоматически проверяются, включают DML и ATS Pfenning и Xi.В DML, в отличие от работы Сюй, зависимые типы ограничены, поэтому автоматическая проверка завершена.

Answer 3

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

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

Answer 4

DBC полезен, если вы не можете выразить все предположения в самом типе systen.Простой пример 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 с типамисистема.Конечно, существует иллюзия, что возможно что-то вроде индексированных монад, но реальный код с такими попытками будет выглядеть супер сложным, неподдерживаемым и не практичным.Но я думаю, что возможны некоторые гибридные схемы.