верификация алгоритма

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

— Donald E. Knuth

А у меня тип везде один и тот же - граф и граф

Тогда в чём ты хочешь убедиться? Что данный объект (результат алгоритма) является графом?

http://en.wikipedia.org/wiki/List_of_model_checking_tools

Кнут сцуко юморист :)

в том, что алгоритм на самом деле преобразует граф A в граф B.

Может быть, agda/coq - на самом деле, то, что нужно. Тогда приведите, пожалуйста, соответствующий пример

Вот тебе пример верифицированного qsort'а на agda http://habrahabr.ru/post/148769/

Но лучше таки возьми утилиты для проведения верификации модели.

Вот на примере сортировки http://twanvl.nl/blog/agda/sorting

Обрати внимание на типы sort : (xs : List A) → Sorted' A.

То есть sort для любого списка возвращает отсортированный список из этих же элементов (а не просто список на входе и список на выходе).

Так и в твоём случае. Надо описать тип графа B и указать как он соотносится с графом A.

Для Coq есть GraphBasics:

This library offers inductive definitions of basics in graph theory. The goal is to offer the possibility to write proofs and programs on graphs in the same formalism : the Coq language. It now contains : vertices, arcs, edges, degrees, graphs, directed graphs, paths, acyclic graphs, connected graphs and tree.

Зависимые типы не только описывают данные, но и выражают утверждение.

Например, если ты хочешь доказать, что твой алгоритм переводит графы со свойством A в графы со свойством B, то твой «входной» тип — это не просто «граф»; это пара (g, доказательство свойства A для g).

Более точно, если тип графов обозначить через G, то у тебя будет:

G : Set — это значит просто, что G — это тип.

A : G -> Set — то есть, для любого g : G мы имеем тип A g.

На самом деле, элементы «A g» имеет смысл считать /доказательствами/ того, что свойство A выполняется для конкретного графа g. Это — зависимый тип, так как для двух разных графов g1 и g2 типы «A g1» и «A g2» будут разными.

Наконец, на вход твоего алгоритма будет подана пара

(g : G, p : A g)

Соответственно, на выходе ты хочешь получить

(h : G, q : B h)

Но на самом деле это не совсем правильно, так как получается, что определяя h твой алгоритм может воспользоваться не только g, но и p.

Правильнее будет написать твой алгоритм как функцию

f : G -> G

после чего завести такой тип:

(g : G) -> (p : A g) -> B (f g)

Если ты сумеешь придумать функцию, имеющую именно такой тип, то, в результате, у тебя будет способ по любому графу g и доказательству свойства A для g получить доказательство свойства B для графа (f g) — что тебе и нужно.

Разумеется это можно обобщить на более общие свойства функций. То есть, если ты придумал некоторое свойство C, которому должна удовлетворять функция f в целом, то

C : (G -> G) -> Set

и тебе надо просто придумать функцию типа «C f». А уж агдочка проверит, что все вычисления ты выписал корректно.

Вопрос немного не по теме, но близко.

Это всё очень круто, но что делать, если верифицировать нужно алгоритм (точнее, его реализацию) на другом языке (Си, плюсы)? Есть какой-то способ сопоставления Си-кода агде? Я просто далек от этой темы и, вероятно, это очень глупый вопрос :)

а что скажете про Maude System? никак не могу понять область применения

но что делать, если верифицировать нужно алгоритм (точнее, его реализацию) на другом языке (Си, плюсы)?

В принципе, есть такой способ: алгоритм пишется не на C, а на некоем похожем на него DSL, но с ясной семантикой. Затем на Agda пишется интерпретатор этого DSL, после чего алгоритм становится Agda-функцией. Исходник на C генерится из этого DSL.

Это всё очень муторно и тоскливо. Использовать сам C для формальной верификации почти нереально, ибо семантически он НЕМЫСЛИМО сложен.

Ничего не скажу, бо не знаю.

Для сишки уже есть нормальная денотационная семантики? :)

Вся проблема с верификацией сводится к тому, что тебе нужно для начала точно сформулировать то, что ты хочешь доказать. Не просто «что мой код корректен», а полностью описать, что ты имеешь в виду под этим утверждением. Доказательство того, что у тебя на входе граф и на выходе граф — элементарно. Другое дело, когда эти графы должны иметь специфический вид.

Как только ты это сформулируешь в терминах теории типов и логики, бери мануал по Agda или Coq, и оно реализуется как по маслу.

A shallow survey of formal methods for C code

Спасибо, посмотрю

Что все так носятся с денотационными семантиками? Провальная это изначально идея. Языки, особенно императивные, следует описывать операционными семантиками.

Смотри сюда: https://code.google.com/p/c-semantics/