Re: сертификация
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Tue, 27 Apr 2010 17:08:03 +0300:
>> >> OG> В будущем правда имеется перспектива использования формальных
>> >> OG> методов для доказательства корректности работы программы.
>> >>
>> >> С добрым утром. Век уже как доказано, что эта задача в общем виде
>> >> алгоритмически неразрешима.
>> >>
>> >> То есть для реального доказательства надо либо ОЧЕНЬ специально писать
>> >> проверяемую программу, либо _придумывать_ доказательство для данной
>> >> конкретной. Причем во втором случае размер доказательства (и,
>> >> соответственно, вероятность ошибок уже в нем) растет принципиально
>> >> быстрее, чем размер самой программы. Даже не экспоненциально, а что-то
>> >> типа гиперэкспоненты.
>> >>
>> OG> Это и подразумевалось. Доказательства выполняются вручную в
>> OG> proof assistant.
>>
>> OG> Сейчас некоторые процессоры имеют доказательство корретности
>> OG> работы некоторых своих подчастей.
>>
>> От то-то и оно, что _некоторые_ процессоры и _некоторых_ подчастей. По
>> сравнению с кодом хотя бы libc там доказывать-то нечего... И все равно
>> полного доказательства про весь процессор нету. Да и в том, что есть,
>> еще надо доказать отсутствие ошибок :-)
>>
OG> Я бы сказал так - на Си код тяжело верифицировать,
OG> скорее всего придется отказаться от существующего кода
OG> и писать на более формальном языке - например Лиспе.
У меня фортунка на эту тему любимая есть...
Greenspun's Tenth Rule of Programming: any sufficiently complicated C
or Fortran program contains an ad hoc informally-specified bug-ridden
slow implementation of half of Common Lisp.
-- Phil Greenspun
"Including Common Lisp."
-- Robert Morris
Реализацию лиспа, на которой оно выполняется, кто доказывать будет?
-Пушкин- МакКарти?
И в общем, да, ты тот лисп вообще видел? Программы на нем писал?
Отлаживал? А реальные программы, не учебные задачи? Я б тебя еще
понял, если б ты Хаскель назвал - тот чисто функциональный, там
действительно существенно легче верифицировать. А как только у тебя
в языке есть присваивание - все, туши свет...
>> OG> Доказательство же позволит избежать полного невозможного
>> OG> перебора для тестирования.
>>
>> Нивапрос. Если его удастся, во-первых, построить, а во-вторых,
>> проверить.
OG> Построить действительно на данный момент тяжело.
OG> Проверка же выполняется просто -
OG> убедаемся в правильности формализации
OG> и коректности правил вывода.
"Ты пальцем покажи". В смысле - предъяви доказательство правильности
формализации любого _практического_ программно-аппаратного комплекса.
OG> Доказательство проверится автоматичеки.
Автоматическую проверялку доказательства уже доказали? А автомат, на
котором оно проверяет?
>> Тесты ту же вероятность обычно дают дешевле.
>>
OG> В доказательстве нет места вероятности.
Это очень наивное утверждение. Мягко говоря, не соответствующее
действительности. Говорю как человек, который не только знает историю
великой теоремы Ферма, но и сам на практике предъявлял доказательство,
ошибку в котором нашел только третий проверяющий.
Я, знаешь ли, теорией доказательств на практике занимался...
OG> Тесты могут обнаружить ошибку,
OG> но не могут гарантировать их отсутствие,
OG> тогда как доказательство гарантирует.
Упущено ключевое слово. _Верное_ доказательство. И вот в этом слове и
прячется вероятность.
--
Правки Белявского, сделанные им в рабочей копии головы
-- Из коммитлога.
Reply to: