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

Ну, с нескольких вещей для начала, раз уж вы выбираете путь Haskell:

• Вы знакомы с перепиской Карри-Ховарда? Существуют системы, используемые для проверенных машиной доказательств, основанных на этом, которые во многих отношениях являются просто функциональными языками программирования с очень мощными системами типов.

• Вы знакомы с областями абстрактной математики, которые предоставляют полезные концепции для анализа кода Haskell? Возникает много различных разновидностей алгебры и кое-что из теории категорий.

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

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

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

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

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

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

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

• Последнего относительно легко избежать: не пишите их и не используйте их. Убедитесь, что каждый набор шаблонов соответствует всем возможным случаям, и никогда не используйте error или undefined. Единственная сложность - избегать стандартных библиотечных функций, которые могут вызывать ошибки. Некоторые из них явно небезопасны, например fromJust :: Maybe a -> a или head :: [a] -> a, но другие могут быть более тонкими. Если вы обнаружите, что пишете функцию, которая действительно, действительно ничего не может сделать с некоторыми входными значениями, то вы позволяете кодировать недопустимые состояния по типу ввода, и вам нужно сначала исправить это.

• Второго легко избежать на поверхностном уровне, разбросав материал по разным чистым функциям, которые затем используются из выражения IO. Лучше, насколько это возможно, переместить всю программу в чистый код, чтобы ее можно было оценивать независимо от всего, кроме фактического ввода-вывода. Это в основном становится сложным только тогда, когда вам нужна рекурсия, управляемая внешним вводом, что подводит меня к последнему пункту:

• Слова к мудрым: Обоснованная рекурсия и продуктивная рекурсия. Всегда проверяйте, что рекурсивные функции либо переходят от некоторой начальной точки к известному базовому случаю, либо генерируют серию элементов по запросу. В чистом коде самый простой способ сделать это - рекурсивно свернуть конечную структуру данных (например, вместо функции, вызывающей себя напрямую при увеличении счетчика до некоторого максимума, создайте список, содержащий диапазон значений счетчика, и сверните его. ) или рекурсивно генерировать ленивую структуру данных (например, список прогрессивных приближений к некоторому значению), при этом тщательно никогда не смешивая их напрямую (например, не просто «найдите первый элемент в потоке, удовлетворяющий некоторому условию»; это может не Вместо этого возьмите значения из потока до некоторой максимальной глубины, затем выполните поиск по конечному списку, соответствующим образом обрабатывая ненайденный случай).

• Комбинируя последние два элемента, для тех частей, где вам действительно нужна IO с общей рекурсией, попробуйте построить программу как инкрементные компоненты, а затем сконденсируйте все неудобные части в единую «драйверную» функцию. Например, вы можете написать цикл событий графического интерфейса пользователя с чистой функцией, такой как mainLoop :: UIState -> Events -> UIState, тестом выхода, например, quitMessage :: Events -> Bool, функцией для получения ожидающих событий getEvents :: IO Events и функцией обновления updateUI :: UIState -> IO (), а затем фактически запустить это с помощью обобщенной функции, такой как runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO (). Это сохраняет сложные части по-настоящему чистыми, позволяя вам запускать всю программу с помощью сценария событий и проверять результирующее состояние пользовательского интерфейса, в то же время изолируя неудобные рекурсивные части ввода-вывода в единую абстрактную функцию, которую легко понять и которая часто неизбежно будет правильной. с помощью параметричности.

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

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

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

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

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

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

• Императивный язык, такой как C, C ++, Fortran, Python: здесь очень сложно что-либо формализовать. Модульные тесты и общие рассуждения - единственный способ получить хоть какую-то уверенность. Статическая типизация выявляет только тривиальные ошибки (что намного лучше, чем не ловить их!).

• Чисто функциональные языки, такие как Haskell, ML: система выразительных типов помогает выявлять нетривиальные ошибки и ошибки. Я бы сказал, что ручная проверка правильности практична для фрагментов длиной до 200 строк. (Например, я сделал пробу для своего рабочего пакета.) Quickcheck - это дешевая замена формализованным доказательствам.

• Языки с зависимой типизацией и помощники по проверке, такие как Agda, Epigram, Coq: проверка правильности всей программы возможна благодаря автоматизированной помощи с формализацией и обнаружением доказательств. Однако нагрузка по-прежнему высока.

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

Похоже, вам нужен 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/

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

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

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

Привычка - это упрощенный диалект 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

Конечно, сегодня самый популярный метод доказательства свойств программ - это модульное тестирование, которое дает сильные теоремы, но эти теоремы излишне конкретны. «Типы, считающиеся вредными», Пирс, слайд 66

Взгляните на Zeno. Цитата из вики-страницы:

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

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

Конечно, можно формально доказать некоторые свойства программ на Haskell. Мне пришлось сделать это на экзамене FP: учитывая два выражения, докажите, что они обозначают одну и ту же функцию. В целом это невозможно сделать, поскольку Haskell является полным по Тьюрингу, поэтому любой механический испытатель должен быть либо помощником доказательства (полуавтоматическим с руководством пользователя), либо средством проверки моделей.

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

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

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

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

Вы можете использовать инструмент hs-to-coq для преобразования Haskell в основном автоматически в Coq, а затем использовать вся мощь помощника доказательства Coq для проверки вашего кода Haskell. См. Документы https://arxiv.org/abs/1803.06960 и https://arxiv.org/abs/1711.09286 для получения дополнительной информации.