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

Question

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

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

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

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

Мне нужна структура, которая может смотреть на функцию Haskell, добавить, написанную в псевдокоде:

add(a, b):
    return a + b

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

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

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

Answer 1

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

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

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

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

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

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

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

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

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

---

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

• Последнее относительно легко избежать: не пишите их и не используйте их. Убедитесь, что каждый набор шаблонов соответствует каждому возможному случаю, и никогда не используйте 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 (), Благодаря этому сложные части остаются действительно чистыми, что позволяет вам запускать всю программу со сценарием событий и проверять полученное состояние пользовательского интерфейса, в то же время изолируя неудобные рекурсивные части ввода-вывода в единую абстрактную функцию, которую легко понять и которая зачастую неизбежно будет правильной. по параметричности.

Answer 2

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

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

Answer 3

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

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

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

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

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

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

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

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

Answer 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/

Answer 5

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

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

Answer 6

Посмотрите на Зено. Цитирование вики-страницы:

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

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

Answer 7

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

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

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

Полный Хьюм
  Полная рекурсия
PR-Hume
  Примитивные рекурсивные функции
Шаблон-Hume
  Предопределенные функции высшего порядка
  Индуктивные структуры данных
  Индуктивные нерекурсивные функции первого порядка
FSM-Hume
  Нерекурсивные структуры данных
HW-Hume
  Нет функций
  Нерекурсивные структуры данных

Конечно, самый популярный метод проверки свойств программы сегодня - это модульное тестирование, которое дает строгие теоремы, но эти теоремы слишком специфичны. "Виды, считающиеся вредными", Пирс, слайд 66

Answer 8

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

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

Answer 9

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

Answer 10

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

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

Answer 11

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