Статический анализ кода
От: dilettante  
Дата: 16.10.09 08:03
Оценка:
Здравствуйте!

Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете?
Интересует возможность практического применения.
Re: Статический анализ кода
От: VladD2 Российская Империя www.nemerle.org
Дата: 16.10.09 19:38
Оценка:
Здравствуйте, 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. Верификация пока что не всегда заканчивается в разумное время.
http://nemerle.org/Banners/?g=dark
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Re[2]: Статический анализ кода
От: MasterZiv СССР  
Дата: 17.10.09 08:36
Оценка:
VladD2 wrote:

А как там на счёт С++ ?
Posted via RSDN NNTP Server 2.1 beta
Re[3]: Статический анализ кода
От: VladD2 Российская Империя www.nemerle.org
Дата: 19.10.09 11:41
Оценка:
Здравствуйте, MasterZiv, Вы писали:

MZ>А как там на счёт С++ ?


Не знаю, думаю — никак.
Если тебя это интересует, то мыльники авторов доступны публично...
http://nemerle.org/Banners/?g=dark
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Re: Статический анализ кода
От: metaprogrammer  
Дата: 21.10.09 22:57
Оценка:
Здравствуйте, dilettante, Вы писали:

D>Здравствуйте!


D>Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете?

D>Интересует возможность практического применения.

http://www.coverity.com/
http://www.klocwork.com/
http://www.parasoft.com/

Всё это для C/C++. Работает как-то, ошибки находит. Не все, конечно.
Re: Статический анализ кода
От: 67108864 http://ajtkulov.blogspot.com
Дата: 23.10.09 18:54
Оценка:
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 — частично от туда же ноги растут.
Re[2]: Статический анализ кода
От: metaprogrammer  
Дата: 24.10.09 11:18
Оценка:
Здравствуйте, 67108864, Вы писали:

6>Теорема Райса-Шапиро (или просто Райса): по исходному коду нельзя понять никакие нетривиальные свойства вычисляемого алгоритма.

6>Поэтому надо добавлять информацию о постановке задачи (не для исполнения).

Анализ кода и доказательство кода всё же несколько разные задачи. Под анализом обычно понимают вывод совсем уж тривиальных свойств, для которых достаточно известных аннотаций к стандартным библиотекам.

6>Проблемы: на выходе логические утверждения — которые еще надо уметь доказывать(!).


Это как раз не проблема.

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


А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.
Re[3]: Статический анализ кода
От: minorlogic Украина  
Дата: 25.10.09 08:18
Оценка:
Здравствуйте, metaprogrammer, Вы писали:

M> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.


Автоматическая проверка на входные и выходные данные ?
... << RSDN@Home 1.2.0 alpha 4 rev. 1237>>
Ищу работу, 3D, SLAM, computer graphics/vision.
Re[4]: Статический анализ кода
От: metaprogrammer  
Дата: 25.10.09 11:39
Оценка:
Здравствуйте, minorlogic, Вы писали:

M>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.


M>Автоматическая проверка на входные и выходные данные ?


Без написанных ручками аннотаций?

С одной стороны, развитые системы типов — это тоже своего рода аннотации. Однако, насколько сложно заставить писать на Хаскелле программиста, всю жизнь портившего себе голову всякими сиплюсплюсами, все тут прекрасно знают. Чего уж говорить про аннотации более высокого уровня? С другой стороны, заведомо и намеренно ограниченная семантика DSLей тоже служит аннотацией, общей ко всему множество выразимых на DSL програм. Так что, например, декларативное описание грамматики в виде PEG, например, уже само по себе будет и аннотацией для проверки входных данных — только, к сожалению, в рантайме.
Re[5]: Статический анализ кода
От: minorlogic Украина  
Дата: 25.10.09 12:50
Оценка:
Здравствуйте, metaprogrammer, Вы писали:

M>Здравствуйте, minorlogic, Вы писали:


M>>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.


M>>Автоматическая проверка на входные и выходные данные ?


M> Без написанных ручками аннотаций?

Проверка что аннотации написаны
... << RSDN@Home 1.2.0 alpha 4 rev. 1237>>
Ищу работу, 3D, SLAM, computer graphics/vision.
Re[6]: Статический анализ кода
От: metaprogrammer  
Дата: 25.10.09 13:02
Оценка:
Здравствуйте, minorlogic, Вы писали:

M>> Без написанных ручками аннотаций?

M>Проверка что аннотации написаны

У такого языка программирования, я думаю, отдельного форума на RSDN никогда не будет. Так как все пять человек, его использующие, и без форума пообщаться смогут.
Re[3]: Статический анализ кода
От: dilettante  
Дата: 27.10.09 08:41
Оценка:
Здравствуйте, metaprogrammer, Вы писали:

M>Здравствуйте, 67108864, Вы писали:


M> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.


Почему? Как тогда возможно заставить его делать хоть что-нибудь, например — писать код?
Re[4]: Статический анализ кода
От: Mystic Украина http://mystic2000.newmail.ru
Дата: 27.10.09 11:09
Оценка:
Здравствуйте, dilettante, Вы писали:
D>Здравствуйте, metaprogrammer, Вы писали:

M>> А вот это уже проблема. Заставить программиста писать аннотации невозможно. Никогда.

D>Почему? Как тогда возможно заставить его делать хоть что-нибудь, например — писать код?

Скорее всего вопрос в цене.

Во-вторых, интересно, какие средства отладки есть для этих аннотаций? Не получится ли так, что программист будет два дня медитировать над кодом, который написал за полчаса, чтобы понять, каких аннотацией не хватает для доказательства???

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