Могут ли функции Haskell быть проверены/проверены/проверены/проверены с правильными свойствами?

Продолжая идеи из: Есть ли доказуемые языки в реальном мире?

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

После того, как вы задали вышеупомянутый вопрос и получили феноменальный ответ (спасибо всем!), я решил сузить свой поиск доказуемого, прагматичного подхода к Haskell. Я выбрал Haskell, потому что он действительно полезен (есть many web фреймворки, написанные для него, это кажется хорошим эталоном) И Я думаю, что он достаточно строг, функционально, что он может быть доказуемым или, по крайней мере, разрешить тестирование инвариантов.

Здесь я хочу (и не смог найти)

Я хочу фреймворк, который может смотреть на функцию Haskell, добавлять, писать в psudocode:

add(a, b):
    return a + b

- и проверьте, сохраняются ли определенные инварианты над каждым состоянием выполнения. Я бы предпочел для некоторых формальных доказательств, однако я бы согласился на что-то вроде проверки модели.
В этом примере инвариантным было бы то, что при заданных значениях a и b возвращаемое значение всегда равно сумме a + b.

Это простой пример, но я не считаю невозможным существование такой структуры. Разумеется, был бы верхний предел сложности функции, которая могла бы быть проверена (10 строковых входов в функцию, безусловно, занимали бы много времени!), Но это будет способствовать более тщательному проектированию функций и ничем не отличается от использования других формальных методы. Представьте, что вы используете Z или B, когда вы определяете переменные/наборы, вы чертовски уверены, что вы даете переменным наименьшие возможные диапазоны. Если ваш INT никогда не будет выше 100, убедитесь, что вы его инициализируете как таковое! Подобные методы и надлежащая декомпозиция задач должны - я думаю, - допускать удовлетворительную проверку чисто функционального языка, такого как Haskell.

Я еще не очень опытен формальными методами или Haskell. Дайте мне знать, если моя идея звуковая, или, может быть, вы думаете, что haskell не подходит? Если вы предлагаете другой язык, убедитесь, что он прошел тест "has-a-web-framework" и прочитайте оригинал question: -)

Ответ 1

Ну, с чего начать, поскольку вы берете маршрут Haskell:

Вы знакомы с карри-ховардской перепиской? Существуют системы, используемые для проверки на машинах, основанные на этом, которые во многих отношениях являются просто функциональными языками программирования с очень мощными системами типов.
Вы знакомы с областями абстрактной математики, которые предоставляют полезные концепции для анализа кода Haskell? Различных ароматов алгебры и некоторых кусков теории категорий много.
Имейте в виду, что у Haskell, как и на всех языках, имеющих Turing, всегда есть возможность итерации. В общем, гораздо труднее доказать, что что-то всегда будет истинным, чем доказать, что либо что-то будет истинным, либо будет зависеть от неизменяющего значения.

Если вы серьезно собираетесь доказывать это, а не просто тестировать, это то, о чем нужно помнить. Основным правилом является следующее: Сделать недопустимые состояния причиной ошибок компилятора. Предотвратите недействительные данные от кодирования в первую очередь, а затем пусть проверяющий тип выполняет утомительную часть для вас.

Если вы хотите пойти еще дальше, если память служит мне помощником по проверке Coq имеет функцию "extract to Haskell", которая будет позвольте вам доказать произвольные свойства о критических функциях, затем переведите доказательства в код Haskell.

Для того, чтобы делать вещи в стиле фантазийного типа непосредственно в Haskell, Олег Киселев - Великий Мастер. Вы можете найти примеры на его сайте опрятных трюков, таких как полиморфные типы более высокого ранга для кодирования статических доказательств проверки границ массива.

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

Еще один шаг, который вы можете предпринять, построив легкую проверку и причудливые системные трюки, должен использовать тот факт, что Haskell хорошо работает как хост-язык для встраивания доменные языки; сначала создайте тщательно ограниченный подъязык (в идеале, тот, который не является Turing-полным), о котором вы можете более легко доказать полезные свойства, а затем использовать программы в этом DSL для предоставления ключевых компонентов основной функциональности в вашей общей программе. Например, вы можете доказать, что функция с двумя аргументами ассоциативна, чтобы оправдывать параллельное сокращение набора элементов с помощью этой функции (так как порядок применения функции не имеет значения, а только порядок аргументов).

О, последнее. Некоторые советы по избежанию подводных камней, которые содержит Haskell, которые могут саботировать код, который в противном случае был бы безопасным по конструкции: ваши заклятые враги здесь общая рекурсия, IO monad и частичные функции:

Последнее относительно легко избежать: не пишите и не используйте их. Убедитесь, что каждый набор шаблонов соответствует любому возможному случаю и никогда не использует error или undefined. Единственная сложная задача - избежать стандартных функций библиотеки, которые могут вызвать ошибки. Некоторые из них, очевидно, небезопасны, например, fromJust :: Maybe a -> a или head :: [a] -> a, но другие могут быть более тонкими. Если вы обнаружите, что пишете функцию, которая действительно действительно не может ничего сделать с некоторыми входными значениями, тогда вы разрешаете недопустимые состояния кодироваться типом ввода и должны сначала исправить это.
Второе легко избежать на поверхностном уровне путем рассеивания материала через различные чистые функции, которые затем используются из выражения IO. Лучше всего, насколько это возможно, перенести всю программу в чистый код, чтобы его можно было оценивать независимо от всего, кроме фактического ввода-вывода. Это в основном становится сложным только тогда, когда вам нужна рекурсия, которая управляется внешним входом, что приводит меня к последнему элементу:
Слова мудрым: обоснованная рекурсия и производительная операция, Всегда убедитесь, что рекурсивные функции либо переходят от некоторой начальной точки к известному базовому случаю, либо генерируют ряд элементов по требованию. В чистом коде самый простой способ сделать это - либо рекурсивно свернуть конечную структуру данных (например, вместо функции, вызывающей себя непосредственно, при увеличении счетчика до некоторого максимума, создайте список, содержащий диапазон значений счетчика и сложите его ) или рекурсивное генерирование ленивой структуры данных (например, список прогрессивных приближений к некоторому значению), при этом никогда не смешивая сразу два (например, не просто "найти первый элемент в потоке, удовлетворяющий определенному условию", Вместо этого, возьмите значения из потока до некоторой максимальной глубины, затем выполните поиск в конечном списке, обработав не найденный случай соответственно).
Объединяя последние два элемента, для тех частей, где вам действительно нужно IO с общей рекурсией, попробуйте построить программу как инкрементные компоненты, а затем сконденсируйте все неудобные биты в одну "драйвер". Например, вы можете написать цикл событий GUI с чистой функцией, такой как mainLoop :: UIState -> Events -> UIState, тест на выход, такой как quitMessage :: Events -> Bool, функция для получения ожидающих событий getEvents :: IO Events и функция обновления updateUI :: UIState -> IO (), а затем фактически запустить вещь с обобщенной функцией типа runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). Это делает сложные части действительно чистыми, позволяя запускать всю программу с событием script и проверять полученное состояние пользовательского интерфейса, выделяя неудобные рекурсивные части ввода-вывода в единую абстрактную функцию, которую легко понять и часто будет неизбежно исправить parametricity.

Ответ 2

Вероятно, самое близкое к тому, что вы просите, это Haskabelle, инструмент, который поставляется с помощником проверки Isabelle, который может переводить файлы Haskell в теории Isabelle и позволяет вам доказывать что-то о них. Насколько я понимаю, этот инструмент разработан в рамках проекта HOL-ML-Haskell и их домашняя страница содержит некоторую информацию об этой теории.

Я не очень хорошо знаком с этим проектом, и я не очень много знаю о том, что с ним сделано. Но я знаю, что Брайан Хаффман играл с этими вещами, проверял свои документы и переговоры, они должны содержать соответствующие материалы.

Ответ 3

Я не уверен, что то, о чем вы просите, на самом деле сделает вас счастливыми.: -)

Проверка модели на язык общего назначения является нежелательной, поскольку модели должны быть специфичными для домена, чтобы быть практичными. Из-за теоремы о неполноте Гёделя просто нет метода автоматического поиска доказательств в достаточно выразительной логике.

Это означает, что вы должны писать доказательства самостоятельно, что ставит вопрос о том, стоит ли затратить потраченное время. Конечно, усилия создают что-то очень ценное, а именно уверенность в правильности вашей программы. Вопрос заключается не в том, является ли это обязательным условием, а является ли затраченное время слишком большой стоимостью. Дело в доказательствах заключается в том, что, хотя у вас может быть "интуитивное" понимание того, что ваша программа правильная, часто очень сложно формализовать это понимание как доказательство. Проблема с интуитивным пониманием заключается в том, что она очень подвержена случайным ошибкам (опечатки и другие глупые ошибки). Это основная дилемма написания правильных программ.

Итак, исследование правильности программы - это упрощение формализации доказательств и автоматическая проверка их правильности. Программирование является неотъемлемой частью "простоты формализации"; очень важно писать программы в стиле, о котором легко рассуждать. В настоящее время мы имеем следующий спектр:

Императивный язык, такой как C, С++, Fortran, Python: очень сложно оформить что-либо здесь. Единичные тесты и общие рассуждения - единственный способ получить хотя бы некоторую уверенность. Статическая типизация ловит только тривиальные ошибки (что намного лучше, чем их не поймать!).
Чисто функциональные языки, такие как Haskell, ML: Система выраженного типа помогает поймать нетривиальные ошибки и ошибки. Доказательство правильности вручную практично для фрагментов примерно до 200 строк, я бы сказал. (Например, я сделал доказательство для своего рабочего пакета. Quickcheck является дешевой заменой формализованных доказательств.
В зависимости от типизированных языков и помощников по устранению недостатков, таких как Agda, Epigram, Coq: проверка правильных целых программ возможна благодаря автоматизированной помощи с формализацией и обнаружением доказательств. Однако бремя остается высоким.

По-моему, нынешнее сладкое пятно для написания правильных программ - это чисто функциональное программирование. Если жизнь зависит от правильности вашей программы, вам лучше идти на уровень выше и использовать помощника по проверке.

Ответ 4

Похоже, что вы хотите ESC/Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

О, и у Agda теперь есть веб-фреймворк (по крайней мере, доказательство концепции): http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

Ответ 5

Вы посмотрели на quickcheck? Он может предложить некоторые из вещей, которые вам нужны.

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

Ответ 6

Ваш, казалось бы, простой пример, add (a, b), на самом деле трудно проверить - с плавающей запятой, переполнением, переполнением, прерываниями, проверяется компилятор, проверяется аппаратное обеспечение и т.д.

Habit - упрощенный диалект Haskell, который позволяет проверить свойства программы.

Hume - это язык с 5 уровнями, каждый из которых ограничен и поэтому легче проверить:

Full Hume
  Full recursion
PR−Hume
  Primitive Recursive functions
Template−Hume
  Predefined higher−order functions
  Inductive data structures
  Inductive  Non−recursive first−order functions
FSM−Hume
  Non−recursive data structures
HW−Hume
  No functions
  Non−recursive data structures

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

Ответ 7

Посмотрите Zeno. Цитирование страницы wiki:

Zeno - это автоматическая система проверки свойств программы Haskell; разработанный в Имперском колледже Лондона Уильямом Соннеком, Софией Дроссопулоу и Сьюзан Эйзенбах. Он направлен на решение общей проблемы равенства между двумя членами Хаскелла для любого входного значения.

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

Ответ 8

Конечно, возможно доказать некоторые свойства программ Хаскелла формально. Я должен был сделать это на моем экзамене FP: учитывая два выражения, докажите, что они обозначают одну и ту же функцию. Это невозможно сделать в целом, так как Haskell - это Turing-complete, поэтому любой механический прокси должен либо быть помощником проверки (полуавтоматический с руководством пользователя), либо моделью проверки.

Были предприняты попытки в этом направлении, см., например, P-logic: проверка свойств для программ Haskell или Доказательство правильности функциональных программ используя Mizar. Оба являются академическими работами, описывающими методы больше, чем реализациями.

Ответ 9

Некоторые недавние усилия MSR Cambridge: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

Ответ 10

Инструмент AProVE (по крайней мере) способен доказать прекращение программ Haskell, что является частью проверки правильности. Более подробную информацию можно найти в этой статье (более короткая версия).

Кроме того, вас может заинтересовать Dependent Types. Здесь система типов расширена и используется, чтобы сделать неправильные программы невозможными.