Каковы общие формальные методы для проверки правильности функционального кода?

10

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

Вступительная книга Грэма Хаттона « Программирование на Haskell» ( Google Books ), которую я читаю, изучая Haskell, затрагивает несколько методов рассуждения о таких программах, как

  • рациональное мышление
  • используя неперекрывающиеся шаблоны
  • список индукции

в главе 13, но это не очень подробно.

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

reference-request proof-techniques functional-programming books software-verification FK82
источник

Ответы:

5

Одним из методов де-факто для подтверждения результатов в функциональном программировании является группа Ричарда Берда.

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

В более общем смысле текст «Алгебра программирования» Берда и де Моора также касается правильности функциональных алгоритмов, таких как задачи оптимизации и динамического программирования.

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

Муса Аль-Хасси
источник
Спасибо! Конечно, если я найду больше ресурсов, я обязательно добавлю их в свой пост.
FK82
6

Вы можете начать с

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

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

Тогда вы можете продолжить

В этом томе вы узнаете, как задавать и проверять (проверять правильность) алгоритмы сортировки, деревья двоичного поиска, сбалансированные деревья двоичного поиска и очереди с приоритетами. Прежде чем использовать эту книгу, вы должны иметь некоторое представление об этих алгоритмах и структурах данных, доступных в любом стандартном учебнике по алгоритмам бакалавриата. Вы должны понимать все материалы в Томе 1 Основы программного обеспечения (Основы логики)

Предупреждение: VFA все еще находится в бета-версии!

Антон Трунов
источник
(Ваша вторая ссылка указывает на неправильное место.) Кроме того, в Agda есть проверенное функциональное программирование ; который использует Agda, формально язык программирования, но использует юникод и поэтому ближе к математической нотации.
Муса Аль-Хасси
Исправлено, спасибо. Да, я читал VFPiA, но это не в моем вкусе.
Антон Трунов
Спасибо за ваш ответ! Я думаю, что есть неправильное представление. Я не ищу функциональные методы для проверки алгоритмов (например, помощника по проверке), но для методов проверки функционального кода (например, для проверки правильности функциональной реализации данного алгоритма) @ MusaAl-hassy ответ очень близок к моему желаемый ответ. Если бы я пропустил это и книги, которые вы цитировали, также охватывали этот аспект, не могли бы вы добавить соответствующие главы?
FK82
@ FK82 Вот Theorem app_assoc : ∀ l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)из главы списков . Этот пример выглядит как то, что вас интересует? Они начинают с функционального программирования в Coq, но затем переходят к рассуждениям о свойствах функциональных программ. Главы от Предисловия до IndPrinciples охватывают оба из них, и я сказал бы, что программирование и рассуждение там переплетены.
Антон Трунов
1
@ FK82 (1) Я полностью согласен с этим комментарием. (2) Возможно, вы захотите взглянуть на книгу Р. Берда «Функциональное мышление с Haskell» (2015). В книге множество примеров рассуждений о Хаскеле. (3) Кроме того, «Жемчужины разработки функциональных алгоритмов» (2010) того же автора могут быть вам полезны.
Антон Трунов
5

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

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

Коди
источник
Спасибо! Я на самом деле ищу методы в Хаскеле . Мое сообщение было отредактировано, чтобы включить весь функциональный код, но это намного выше моих намерений.
FK82
1
Мне неизвестны системы, специально предназначенные для проверки Haskell, но я хотел бы отметить, что 1) функциональное ядро ​​Coq (и Agda) по существу неотличимо от ядра Haskell (за исключением ограничения на полные функции) и 2) проверенные программы в Coq и Agda могут быть извлечены в Haskell (хотя я считаю, что извлечение в Haskell лучше поддерживается в Agda, где Coq более ориентирован на Ocaml)
cody
Хорошо знать! Однако это будет означать, что я переписываю свою программу (или соответствующие части) на Coq или Agda. Я не думаю, что это разумно в моем случае.
FK82 19.09.16
Есть пара очень экспериментальных «внешних интерфейсов», которые пытаются конвертировать Haskell в Isabelle или напрямую доказывать эквивалентности, используя Isabelle, но я бы не стал иметь слишком много акций в их зрелости. Я думаю, что переписать код в конечном итоге будет меньше работы.
Коди
4

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

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

Работа Артура Шаргеро объединяет программный логический подход с помощниками по проверке, см., Например, эту обзорную страницу .

Мартин Бергер
источник