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

Question

Прежде всего, возможно ли это только на алгоритмах, которые не имеют побочных эффектов?

Во-вторых, где я мог бы узнать об этом процессе, какие-нибудь хорошие книги, статьи и т.д.?

Answer 1

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

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

Answer 2

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

Answer 3

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

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

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

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

Answer 4

Купите эти книги: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800

Книга Грайса "Научное программирование" - отличная штука.Терпеливый, тщательный, завершенный.

Answer 5

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

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

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

Answer 6

Logic in Computer Science, написанная Хутом и Райаном, дает достаточно читаемый обзор современных систем для проверки систем.Когда-то давно люди говорили о доказательстве корректности программ - с помощью языков программирования, которые могут иметь побочные эффекты, а могут и не иметь.Впечатление, которое у меня сложилось из этой книги и других источников, заключается в том, что реальные приложения отличаются друг от друга - например, доказательство правильности протокола, или того, что блок с плавающей запятой чипа может правильно разделяться, или того, что процедура без блокировки для манипулирования связанными списками верна.

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

Answer 7

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

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

Answer 8

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

Answer 9

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

Answer 10

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

Answer 11

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