Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете?
Интересует возможность практического применения.
Здравствуйте, dilettante, Вы писали:
D>Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете? D>Интересует возможность практического применения.
Один из авторов Nemerle — Michał Moskal: http://research.microsoft.com/en-us/um/people/moskal/
сейчас работает именно над таким проектом (VCC) в рамках Microsoft Research и какой-то там матери.
Насколько я знаю уже применяют на практике.
Есть только две проблемы:
1. С нельзя проверить, так как язык дырявый. По этому приходится снабжать его специальными аннотациями.
2. Верификация пока что не всегда заканчивается в разумное время.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, dilettante, Вы писали:
D>Здравствуйте!
D>Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете? D>Интересует возможность практического применения.
D>Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете? D>Интересует возможность практического применения.
Теорема Райса-Шапиро (или просто Райса): по исходному коду нельзя понять никакие нетривиальные свойства вычисляемого алгоритма.
Поэтому надо добавлять информацию о постановке задачи (не для исполнения).
Полагаю, что все предъявленные системы основаны на логике Флойда-Хоара. Если указать пред/пост условие (+инвариант на циклы) для каждой строчки, то на выходе получим множество логических утверждений, доказав которые, мы, типа (всякие тонкости, типа переполнения стека, чтение/запись чужой памяти не рассматриваем), доказываем правильность работы программы.
Вот что делает следующая программка (вход: a, b, выход — ?) сразу не вкуришь
begin
p:= b;
t:= 0;
while a>=p do
begin
p:= p * 2;
t:= t + 1;
end;
a1:= a;
q:= 0;
while p <> b do
begin
p:=p div 2;
q:=q * 2;
if a >= p then
begin
a:= a - p;
q:= q + 1;
end
endif;
end;
end.
А после аннотации можно все строго доказать
var a, b, q, p, a1, t;
varaug n, m;
begin
{input (a=n) and (b=m) and (n > 0) and (m > 0)}
p:= b;
t:= 0;
{assert (t=0) and (p=b)}
while a>=p do {invariant (p = b * 2^t) and (t>=0)}
begin
p:= p * 2;
t:= t + 1;
end;
a1:= a;
q:= 0;
{assert (q=0) and (a1=a) and
(t>=0) and (p>a) and (p=b*2^t)}
while p <> b do {invariant (a < p) and (a1 = p * q + a)}
begin
p:=p div 2;
q:=q * 2;
{assert (a1 = p * q + a) and (2*p > a)}
if a >= p then
begin
a:= a - p;
q:= q + 1;
end
endif;
end;
{output (a1 = b * q + a) and (a < p)}
end.
Проблемы: на выходе логические утверждения — которые еще надо уметь доказывать(!).
Простенькие примеры на арифметику аннотировать еще можно, но перейдя к сортировке (уже необходимо понятие перестановки) или к каким-нибудь графовым задачам все становится сложно.
Не учитываются технические тонкости.
Есть еще пара подходов, не на Флойде-Хоара. Но там я — o(1) (можно сказать полный 0).
ИМХО, DBC в eiffel — частично от туда же ноги растут.
Здравствуйте, 67108864, Вы писали:
6>Теорема Райса-Шапиро (или просто Райса): по исходному коду нельзя понять никакие нетривиальные свойства вычисляемого алгоритма. 6>Поэтому надо добавлять информацию о постановке задачи (не для исполнения).
Анализ кода и доказательство кода всё же несколько разные задачи. Под анализом обычно понимают вывод совсем уж тривиальных свойств, для которых достаточно известных аннотаций к стандартным библиотекам.
6>Проблемы: на выходе логические утверждения — которые еще надо уметь доказывать(!).
Это как раз не проблема.
6>Простенькие примеры на арифметику аннотировать еще можно, но перейдя к сортировке (уже необходимо понятие перестановки) или к каким-нибудь графовым задачам все становится сложно.
А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.
Здравствуйте, minorlogic, Вы писали:
M>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.
M>Автоматическая проверка на входные и выходные данные ?
Без написанных ручками аннотаций?
С одной стороны, развитые системы типов — это тоже своего рода аннотации. Однако, насколько сложно заставить писать на Хаскелле программиста, всю жизнь портившего себе голову всякими сиплюсплюсами, все тут прекрасно знают. Чего уж говорить про аннотации более высокого уровня? С другой стороны, заведомо и намеренно ограниченная семантика DSLей тоже служит аннотацией, общей ко всему множество выразимых на DSL програм. Так что, например, декларативное описание грамматики в виде PEG, например, уже само по себе будет и аннотацией для проверки входных данных — только, к сожалению, в рантайме.
Здравствуйте, metaprogrammer, Вы писали:
M>Здравствуйте, minorlogic, Вы писали:
M>>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.
M>>Автоматическая проверка на входные и выходные данные ?
M> Без написанных ручками аннотаций?
Проверка что аннотации написаны
Здравствуйте, minorlogic, Вы писали:
M>> Без написанных ручками аннотаций? M>Проверка что аннотации написаны
У такого языка программирования, я думаю, отдельного форума на RSDN никогда не будет. Так как все пять человек, его использующие, и без форума пообщаться смогут.
Здравствуйте, metaprogrammer, Вы писали:
M>Здравствуйте, 67108864, Вы писали:
M> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.
Почему? Как тогда возможно заставить его делать хоть что-нибудь, например — писать код?
Здравствуйте, dilettante, Вы писали: D>Здравствуйте, metaprogrammer, Вы писали:
M>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда. D>Почему? Как тогда возможно заставить его делать хоть что-нибудь, например — писать код?
Скорее всего вопрос в цене.
Во-вторых, интересно, какие средства отладки есть для этих аннотаций? Не получится ли так, что программист будет два дня медитировать над кодом, который написал за полчаса, чтобы понять, каких аннотацией не хватает для доказательства???
В-третьих, простое математическое вычисление лучше подходит для доказательства правильности. Как перенести систему аннотаций уже на шахматы я представляю себе слабо (надо доказать, что данные генератор ходов делает все возможные хода из данной позиции). Особенно для какого-нить хитрого представления доски.
