«Математическое доказательство программ»

Можно начать отсюда: http://en.wikipedia.org/wiki/Verifiability

Хм, интересно. А имеет вообще смысл доказывать программу, компилирующуюся недоказанным компилятором, интерпретирующуюся недоказанным интерпретатором, использующую недоказанные библиотеки и работающую в недоказанной ОС на недоказанном железе? Как с этим обстоят дела у производителей, в Ынтерпрайзе, так сказать?

верифицируют алгоритмы, в случаях, когда ошибка недопустима (например программа для чипа, управляющего искусственным сердцем). В Ынтерпрайзе проще юниттестов накидать на основные случаи.

То есть для рядового Ынтерпрайз-джавакодера, например, это всё и не нужно? Или же можно получить какую-то выгоду от использования этих методов? Там, кроме FSM вообще большинство слов для меня новые, если это нужно, существует связный учебник по этому делу?

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

Но это, судя по всему, не очень популярно. А почему? Слишком сложно? ненужно?

>А имеет вообще смысл доказывать программу

С точки зрения математики: Пределы доказуемости http://www.scorcher.ru/art/theory/any/gedel.php

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

Слишком затратно.

> А почему? Слишком сложно? ненужно?

И то, и то, imho. Слишком большие усилия, слишком невнятные результаты. Серебряную пулю в этом направлении делать пока не научились.

> существует связный учебник по этому делу?

http://lib.ru/CTOTOR/DEJKSTRA/

Дийкстра, "Наука программирования" -- классическая работа на эту тему. Есть более поздняя с тем же названием, в соавторстве с Грисом. И есть еще монографии типа "Элементы теории программ" (Абрамова, кажется).

man линейное программирование

> Но это, судя по всему, не очень популярно. А почему? Слишком сложно? ненужно?

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

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

Я года три назад активно увлекался этой задачей (хотел даже выбрать темой диссертации, да не сложилось). Я назвал этот подход "кларификацией" -- как комбинацию доказательства и построения. И проект назвал Clara. Где-то в архиве моей личной вики есть пара статей на эту тему. Вот думаю, на пенсии заняться более основательно.

> А имеет вообще смысл доказывать программу, компилирующуюся недоказанным компилятором, интерпретирующуюся недоказанным интерпретатором, использующую недоказанные библиотеки и работающую в недоказанной ОС на недоказанном железе? Как с этим обстоят дела у производителей, в Ынтерпрайзе, так сказать?

Вполне возможно верифицировать микроядерную ОС в области микроядра -- там чистая алгоритмика, оторванная от "реального мира". Я слышал, что микроядро QNX полностью верифицировано, но конкретных доказательств этого я не видел -- только слухи. Аналогично, поговаривают, что L4 и Mach тоже частично верифицированы. В приницпе, верификация Hurd могла бы стать неплохой задачей.

Аппаратура отлично верифицируется, хотя там принципиально другие принципы доказательства правильности. Очень активно этим занимаются IBM и Texas Instruments, я сам участвовал в аналогичном проекте в Aldec в 1999-2002 годах, но там работы были свернуты из-за отсутствия явной коммерческой выгоды -- они решили специализироваться на симуляторах.

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

> Дийкстра, "Наука программирования"

"Дисциплина программирования", конечно же. Никак не запомню. хотя по этим граблям уже сто раз ходил. А с Грисом -- "Наука программирования".

Все широко используемые алгоритмы доказываются. Можно посмотреть Кормена "Алгоритмы. Построение и анализ" или Гасфилда "Строки, деревья и подпоследовательности в алгоритмах" , там все алгоритмы доказываются.

>И проект назвал Clara

вроде, женскими именами называют алгоритмы кластеризации
а, вообще, очень интересно

> вроде, женскими именами называют алгоритмы кластеризации

Clara (лат.) -- чистая, ясная, понятная, красивая. Отсюда английское clear.

Это дань моему увлечению латынью в молодости :-).

> а, вообще, очень интересно

Значит, есть стимул поднять из бэкапов :-). Будет время -- пороюсь. Там история неприятная была -- я часть статьи потерял, а восстанавливать по памяти уже пропало желание.

Там одним из результатов, кстати, было доказательство того, что любую программу с goto (и его частными случаями) можно переписать без оных...

> Все широко используемые алгоритмы доказываются.

ИМХО бессмысленное словосочетание.

Про _почти_ все "широко используемые алгоритмы" доказано, "алгоритмы" они, или нет.

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

А "математическое доказательство программ" вообще о другом. Там идея в том, что есть алгоритм, реализованный на одном языке, и тот же алгоритм, реализованный на другом языке, и требуется доказать, что это тот же самый алгоритм. ИМХО довольно маргинальная ветвь ИТ, но иногда помогает.

http://programatica.cs.pdx.edu/

>Дийкстра, "Наука программирования" -- классическая работа на эту тему. Есть более поздняя с тем же названием, в соавторстве с Грисом. И есть еще монографии типа "Элементы теории программ" (Абрамова, кажется).

Кстати так "A Method of Programming" это просто более новая версия "A Discipline of Programming", или нужно читать и то и другое?

Спасибо за ссылки. А SICP - это про сабж или нет? Я когда-то начал его, да забросил за другими делами.

> формально доказать корректность протокола, можно доказать отсутствие дедлоков в параллельном алгоритме

см. например, про сети Петри

фтщтшьщгы> не очень популярно. А почему? Слишком сложно? ненужно?

потому что придётся передоказывать при каждом изменении среды (запуске нового процесса, обработке новых событий для протокола)

Но конструктивное доказательство по идее возможно (если строить среду из верифицированых по отдельности компонент). Получится что-то вроде конструктивной математики (есть конструктивное доказательство -- можем что-то сказать, нет -- не ясно и ничего сказать не можем)

Что-то подобное было для .NET managed/unmanaged, верифицируемость сборок при запуске / при компиляции. Правда, если рассматривать сборку как "черный ящик", это ещё надо доказать (например, автоматически, как в подходе вроде delta debugging)

> Вполне возможно верифицировать микроядерную ОС в области микроядра --

то ли EROS то ли Coyotos ЕМНИП, полностью верифицирован автоматически, программой

>то ли EROS то ли Coyotos ЕМНИП, полностью верифицирован автоматически, программой

Coyotos это развитие идей EROS (KeyCos), фраза применима к обоим. а по сабжу ещё есть L4.Verified

Есть вот такой проект, acl2

http://www.cs.utexas.edu/users/moore/acl2/

Строится модель вычислительной системы (естественно, вычислительной системы лиспа), начиная "от Адама". Вещь сложная в использовании, тормозная и умеет мало. Но всё же умеет формулировать, доказывать и принимать от пользователя помощь в доказательстве теорем, касающихся свойств вычислительных систем. Также немного "шарит" в математике, т.е., пониимает свойства чисел, алгебраических операций и т.п. Естественно, можное её расширять новыми теориями.

> "Математическое доказательство _каких-то_свойств_ программ"

Добавлю простой пример, который наглядно демонстрирует весь геморой формального доказательства корректности программ. Имеем такой код

if (p(...)) printf("a"); else printf("b");

Имеем спецификацию

printf("a");

Надо показать формально, что программа соответствует спецификации, при условии что p(x) - логическое выражение соотв. какой-нибудь еще недоказанной математической гипотезе. Например, хотяб вот этой http://ru.wikipedia.org/wiki/%D0%93%D0%B8%D0%BF%D0%BE%D1%82%D0%B5%D0%B7%D0%B0.... Задача мягко говоря не из простых :) Тут не то что об автоматизации, тут о ручном строгом доказательстве корректности говорить не приходится.

Ну это какгбы в общем случае. На деле (если это слово применимо к такой экзотической ветке IT) чтобы удешивить и автоматизировать процесс доказательства свойств программ рассматривают ограниченные подмножества программ, непоноценные аксиоматики, для которых существует простая решающая процедура. Например та же арифметика Пресбургера. Эвристические решатели. Всякие стратегии перебора вариантов переписывания термов и прочее и прочее. А чаще всего адскую смесь из того и другого и третьего. Однако, как показывает практика, ни одного сколько нибудь нетривиального решателя до тру-интерпрайз уровня еще не доведено :)

Если смотреть прагматично, то проверка правильности программ во многом интегрирована в существующие языки. Например декларации типов, в т.ч., типов и числа параметров функций, деклараторы const, деклараторы final в Java - всё это служит для спецификации некоторых ограничений на программу. Если расширять язык деклараций, можно и расширять возможности компилятора (или другой среды) по возможности их проверки.

Функции assert можно тоже рассматривать как часть механизма верификации программы, просто верификация откладывается до момента исполнения :) Механизм сборки мусора - это другая вещь. Здесь накладывается ограничение на язык, которое не даёт строить программы с определёнными видами ошибок.

Конечно, язык деклараций можно расширять как угодно (при знании компилятора). Искусство состоит в том, чтобы этот язык не превратился для компилятора/средства анализа в язык притч, читая которые, нужно думать над каждым словом.

Глядя на современные используемые на практике языки программирования, я вижу, что можно было бы добавить ещё немало деклараций, которые было бы не так сложно реализовать, но которые добавили бы много надёжности. Несколько примеров.

1. В лиспе есть декларация dynamic-extent, декларирующая, что объект можно разместить на стеке, а не в куче.

2. В С часто возвращаемым значением является указатель. Не всегда понятно, кто отвечает за удаление этого указателя, и нужно ли его вообще удалять. Неплохо было бы сделать декларацию, которая сообщала об этом.

Например,

fresh char *strdup(const char *str1)

или

old char *strstr(const char *s1, const char *s2);

а может быть, даже

old(s1) char *strstr(const char *s1, const char *s2);

если функция удаляет указатель, который ей передали, то можно сделать декларацию eats ("ест").

void free(eats void *p);

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

start_of_mem_block void *malloc(size_t n);

Тогда free может поменять свой вид:

void free(eats start_of_mem_block void *p);

При наличии таких деклараций, комилятор мог бы задёшево отловить немало ошибок, связанных с памятью. Но не все, конечно... И возникли бы трудности, если бы мы сначала прибавили к указателю на начало блока единицу, а потом отняли её обратно. Может быть, для этого стоило бы ввести тип, или декларацию, или аспект offset_of_memory_block

3. В ФП языках не помешала бы декларация pure ("чистый"), которая говорит, что функция является чистой. На самом-то деле, нет чисто ФП языков - самые чистые из них прячут побочные эффекты, как скелет в шкафу. Поэтому, неплохо иметь способ чётко отделять "чистое" от "нечистого". Тут всё довольно просто - функция будет pure, если она построена из чистых примитивов и вызывает только pure функции. Значит, компилятор может проверить чистоту функции за время O(сложность определения).

4. Аналогичная декларация io_free - для функций, которые не имеют доступа к любым операциям, связанным с вводом-выводом.

5. Где-то в каком-то ассемблере (сам не видел) есть декларация reenterab, гарантирующая реентерабильность кода.

6. Декларация O(numeric_expr), которая утверждает, что функция выполняется за O(numeric_expr) вызовов примитивов. Самое простое - это O(1) - такая функция не должна иметь циклов, быть io_free и вызывать только функции и примитивы O(1). При этом, все функции O(1) должны быть упорядочиваемы так, чтобы исключить взаимную рекурсию. Сложнее будет с декларациями O(не_константа). Но, например, в функции с циклом for (int i=0;i<n;i++) { ... (const n) } легко можно доказать, что она вызывает O(n) примитивов. Другой случай - это рекурсивный факториал. В нём есть рекурсия, но в ходе рекурсии значение аргумента убывает. Значит, можно задекларировать его как-нибудь вот так:

O(n) positive int recursive_factorial(recursively_decreases positive int n)

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

ifdef(DEBUG) { ... }

7. Я ещё не написал про throws, но я не знаю, насколько эта декларация обязывает - никогда ей не пользовался.

К этому можно добавить, что многие декларации писать не обязательно - компилятор вполне может вывести их, когда они нужны. Например, если мы декларируем функцию f как O(1), а функцию g никак не декларируем, при этом, f вызывает g, то компилятор может озаботиться проверкой декралации O(1) для g и без нашего на то указания. Это чем-то похоже на выведение типов, которое используется в ocaml и в некоторых расширениях лиспа.

Мне вот, кстати, интересно, есть ли язык, в котором такие декларации собраны вместе? Я могу точно сказать, что в лиспе они НЕ собраны (а жаль). Также они не собраны в С/++, да и вообще ни в одном известном мне языке.

>3. В ФП языках не помешала бы декларация pure ("чистый"), которая говорит, что функция является чистой. На самом-то деле, нет чисто ФП языков - самые чистые из них прячут побочные эффекты, как скелет в шкафу. Поэтому, неплохо иметь способ чётко отделять "чистое" от "нечистого". Тут всё довольно просто - функция будет pure, если она построена из чистых примитивов и вызывает только pure функции. Значит, компилятор может проверить чистоту функции за время O(сложность определения).

в случае Haskell это в принципе работает, ибо монада IO является односторонней : всякая функция, имеющая в сигнатуре IO является не чистой

>4. Аналогичная декларация io_free - для функций, которые не имеют доступа к любым операциям, связанным с вводом-выводом

а в чём существенная разница 3 и 4 пункта ?

>Мне вот, кстати, интересно, есть ли язык, в котором такие декларации собраны вместе?

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

> в случае Haskell это в принципе работает, ибо монада IO является односторонней : всякая функция, имеющая в сигнатуре IO является не чистой

Возможно ли средствами рефлексии узнать, есть ли в сигнатуре данной функции IO? Возможно ли узнать, есть ли где-либо в вызываемых функциях IO? Возможно ли сказать,что "не IO"? Если да, то Хаскель в этом смысле действительно крут :) Вообще же (не в Хаскеле) разница между вводом-выводом и побочными эффектами, конечно же, есть. При наличии ввода-вывода завершение/не-завершение функции начинает зависеть от внешнего по отношению к программе мира. Хотя, с точки зрения реализации, разницы почти нет: в обоих случаях есть некий набор разрешённых операций и мы декларируем, что в функции используются только они.

> про декларацию асимптотической сложности слышу впервые. упрощу вопрос - есть ли хотя бы один язык, в котором есть такая декларация ? :)

Я тоже не знаю. Скорее всего, в acl2 есть или неявно присутствует, т.к. там вроде обсуждается вопрос, завершится ли вызов или нет.