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

Question

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

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

Answer 1

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

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

Answer 2

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

Answer 3

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

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

Answer 4

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

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

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

Answer 5

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

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

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

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

Answer 6

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

Answer 7

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

Answer 8

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

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

Answer 9

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

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

Answer 10

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