Формальная проверка правильности алгоритма

COQ - это помощник по проверке правильности вывода ocaml. Хотя это довольно сложно. Я так и не успел взглянуть на него, но мой коллега начал, а затем перестал использовать его через два месяца. В основном это было потому, что он хотел сделать все быстрее, но если вам нужно проверить алгоритм, это может быть хорошей идеей.

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

1. Обычно намного проще проверить / доказать правильность, когда нет побочных эффектов, но это не абсолютное требование.
2. Возможно, вы захотите ознакомиться с документацией по формальному языку спецификаций, например Z. Формальная спецификация сама по себе не является доказательством, но часто является его основой.

Я думаю, что проверка правильности алгоритма означала бы его соответствие спецификации. Существует раздел теоретической информатики под названием Формальные методы, который может быть тем, что вы ищете, если вам нужно подойти как можно ближе к доказательствам. Из википедии,

Формальные методы - это особый вид математически обоснованных методов спецификации, разработки и проверки программных и аппаратных систем.

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

Обычно доказательства правильности очень специфичны для рассматриваемого алгоритма.

Однако есть несколько хорошо известных приемов, которые используются и используются снова. Например, с рекурсивными алгоритмами вы можете использовать инварианты цикла.

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

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

Купите эти книги: https://rads.stackoverflow.com/amzn/click/com/0387964800

Книга Гриса «Научное программирование» - отличный материал. Терпеливый, тщательный, полный.

«Логика в компьютерных науках», написанная Хутом и Райаном, дает достаточно читаемый обзор современных систем для проверки систем. Когда-то давно люди говорили о проверке правильности программ - с помощью языков программирования, которые могут иметь, а могут и не иметь побочных эффектов. Из этой и других книг у меня складывается впечатление, что реальные приложения разные - например, доказывают, что протокол верен, или что модуль с плавающей запятой микросхемы может правильно делиться, или что подпрограмма без блокировки для управления связанными списками верна.

ACM Computing Surveys Vol 41, выпуск 4 (октябрь 2009 г.) - специальный выпуск о проверке программного обеспечения. Похоже, вы можете найти хотя бы одну из статей без учетной записи ACM, выполнив поиск по запросу «Формальные методы: практика и опыт».

Инструмент Frama-C, для которого Elazar предлагает демонстрационное видео в комментариях, дает вам спецификацию язык, ACSL, для написания функциональных контрактов и различные анализаторы для проверки этого функция C удовлетворяет своим условиям контракта и безопасности, таким как отсутствие ошибок времени выполнения.

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

Если вы знакомы с LISP, вам обязательно стоит проверить ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html

Дисциплина программирования Дейкстры и его EWD закладывают основу для формальной верификации как науки в программировании. Более простая работа - это Системное программирование Вирта, которое начинается с простого подхода к использованию проверки. Вирт использует для языка Паскаль до ISO; Дейкстра использует формализм, подобный Алгол-68, который называется Guarded (GCL). Формальная проверка достигла зрелости со времен Дейкстры и Хора, но эти более старые тексты все еще могут быть хорошей отправной точкой.

Инструмент PVS, разработанный ребятами из Стэнфорда, представляет собой систему спецификации и проверки. Я работал над этим и нашел его очень полезным для Theoram Proving.

WRT (1), вам, вероятно, придется создать модель алгоритма таким образом, чтобы «улавливать» побочные эффекты алгоритма в программной переменной, предназначенной для моделирования таких побочных эффектов на основе состояния.