Прежде всего, возможно ли это только для алгоритмов, которые не имеют побочных эффектов?Формальная проверка правильности алгоритма
Во-вторых, где я могу узнать об этом процессе, о любых хороших книгах, статьях и т. Д.?
COQ является помощником по доказательству, который производит правильный выход ocaml. Это довольно сложно. Я никогда не обдумывал это, но мой коллега начал, а затем прекратил использовать его через два месяца. Это было главным образом потому, что он хотел сделать все быстрее, но если вам нужно проверить алгоритм, это может быть хорошей идеей.
Here is a course, который использует COQ и говорит о проверке алгоритмов.
И here is a tutorial о написании научных статей в COQ.
также, здесь, http://www.lix.polytechnique.fr/coq/getting-started – nlucaroni
Обычно доказательства правильности очень специфичны для алгоритма.
Однако есть несколько известных трюков, которые используются и повторно используются повторно. Например, с помощью рекурсивных алгоритмов вы можете использовать loop invariants.
Другой распространенный трюк сводит исходную проблему к проблеме, для которой доказательство корректности вашего алгоритма проще показать, а затем либо обобщает более легкую проблему, либо показывает, что более легкую проблему можно перевести на решение исходной проблемы. Here - описание.
Если у вас есть определенный алгоритм, вы можете лучше спросить, как построить доказательство для этого алгоритма, а не общий ответ.
Сокращение алгоритма (особенно описано в ссылке, которую вы предлагаете) является теоретическим инструментом, демонстрирующим, что проблема, по крайней мере, такая же сложная, как и другая. Эти доказательства, часто сделанные в модели расчета модели Тьюринга, являются ручными волнообразными делами и не похожими на формальные (проверенные машиной) доказательства. Они часто выполняются для трудностей, которые трудно практиковать (пример в вашей ссылке относится к проблеме Halting, показывая, что проблема NP-hard, уменьшая известную проблему NP-hard, она также популярна). Короче говоря, я не уверен, что сокращение проблемы, как связано, имеет какое-то отношение к формальной правильности. –
Хм, возможно, сокращение - это не правильный термин, который я должен использовать здесь. Когда я говорю о сокращении, я имел в виду что-то вроде следующего примера. Предположим, что у вас есть алгоритм, который вычисляет пересечение N прямоугольников, которые, как вы знаете, являются правильными. Предположим, что у вас есть еще одна проблема, для которой существует нетривиальный перевод этой проблемы в задачу вычисления пересечения N прямоугольников. Затем вы используете первый алгоритм для вычисления решения последней проблемы.Осталось только показать, что перевод правильный. – ldog
Но я вижу, что это сбивает с толку, это трюк, основанный на том, что вы используете известный алгоритм, который, как известно, правильный (в данном случае тот, который вычисляет пересечение N прямоугольников.) Я могу см., где возникает путаница относительно того, является ли это методом доказательства или предоставления правильного алгоритма. – ldog
Я считаю, что проверка правильности алгоритма подтвердила бы его соответствие спецификации. Существует филиал теоретической информатики под названием Formal Methods, который может быть тем, что вы ищете, если вам нужно как можно ближе подойти к доказательству. Из википедии,
Формальных методы представляют собой особый вид методов математической основы для спецификации, разработка и проверки программного обеспечения и аппаратных средств системы
Вы сможете найти много обучения ресурсы и инструменты из множества ссылок на связанной странице Википедии и из Formal Methods wiki.
Купить эти книги: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Книга Грис, науки программирования большой материал. Пациент, полный, полный.
И если вам нравится Z, будьте уверены, что вы найдете инструменты для его включения в процессе написания формально правильного алгоритма: http : //www.bmethod.com/php/methode-b-en.php –
Логика в области компьютерных наук, автор Huth and Ryan, дает достаточно читаемый обзор современных систем для проверки систем.Когда-то люди говорили о правильной проверке программ - с языками программирования, которые могут иметь или не иметь побочных эффектов. Впечатление, которое я получаю из этой книги и в других местах, заключается в том, что реальные приложения различны - например, доказывая правильность протокола или что блок чипа с плавающей запятой может разделить правильно или что функция блокировки для манипулирования связанными списками правильная.
ACM Computing Surveys Vol 41 Issue 4 (октябрь 2009 г.) является особой проблемой при проверке программного обеспечения. Похоже, вы можете получить хотя бы одну из статей без учетной записи ACM, ища «Формальные методы: практика и опыт».
«Формальные методы» охватывают все цели, которые вы указали. Я нахожусь в подполе «проверки программ правильно», и я должен признать, что до сих пор большие промышленные успехи исходили из других подполей (просто подождите до следующего года!). Конференция, такая как FMWEEK, несколько озадачивает, потому что она собирает людей со всеми этими разными подходами и целями, но у нас есть много общего и много для обмена. –
Инструмент Frama-C, для которого Elazar предлагает демонстрационное видео в комментариях, дает вам спецификационный язык, ACSL, для написания контрактов функций и различных анализаторов для проверки того, что функция C удовлетворяет его условиям контракта и безопасности, таким как отсутствие ошибок времени выполнения.
В расширенном учебнике ACSL by example показаны примеры фактических C-алгоритмов, которые задаются и проверяются, и отделяет свободные от побочных эффектов функции от эффективных (без побочных эффектов считаются проще и на первом месте руководство). Этот документ также интересен тем, что он не был написан разработчиками инструментов, которые он описывает, поэтому он дает более свежий и более дидактический взгляд на эти методы.
Если вы знакомы с LISP, то вы должны обязательно проверить acl2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
Дейкстров Дисциплины программирования и его EWDs заложить основу для формальной верификации как науки в программировании. Более простая работа - это систематическое программирование Вирта, которое начинается с простого подхода к использованию проверки. Вирт использует pre-ISO Pascal для языка; Дейкстра использует формализм, подобный Алголу-68, называемый Guarded (GCL). Формальная проверка созрела с Дейкстры и Хоара, но эти старые тексты все еще могут быть хорошей отправной точкой.
Инструмент PVS, разработанный ребятами из Stanford, является системой спецификации и проверки. Я работал над этим и нашел его очень полезным для теоретического доказательства.
WRT (1), вам, вероятно, придется создать модель алгоритма таким образом, чтобы «захватывать» побочные эффекты алгоритма в программной переменной, предназначенной для моделирования таких побочных эффектов на основе состояния.
Я не уверен, что вы имеете в виду о побочных эффектах. – ldog
Смотрите это: http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – joemoe
См. Http://stackoverflow.com/questions/476959/why-cant-programs-be-proven, в котором есть хорошие ответы. –