On 2010.04.27 16:19, Artem Chuprina wrote:
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Tue, 27 Apr 2010
15:37:28 +0300:
>> OG> В будущем правда имеется перспектива использования формальных
>> OG> методов для доказательства корректности работы программы.
>>
>> С добрым утром. Век уже как доказано, что эта задача в общем виде
>> алгоритмически неразрешима.
>>
>> То есть для реального доказательства надо либо ОЧЕНЬ специально писать
>> проверяемую программу, либо _придумывать_ доказательство для данной
>> конкретной. Причем во втором случае размер доказательства (и,
>> соответственно, вероятность ошибок уже в нем) растет принципиально
>> быстрее, чем размер самой программы. Даже не экспоненциально, а что-то
>> типа гиперэкспоненты.
>>
OG> Это и подразумевалось. Доказательства выполняются вручную в
OG> proof assistant.
OG> Сейчас некоторые процессоры имеют доказательство корретности
OG> работы некоторых своих подчастей.
От то-то и оно, что _некоторые_ процессоры и _некоторых_ подчастей. По
сравнению с кодом хотя бы libc там доказывать-то нечего... И все равно
полного доказательства про весь процессор нету. Да и в том, что есть,
еще надо доказать отсутствие ошибок :-)
Я бы сказал так - на Си код тяжело верифицировать,
скорее всего придется отказаться от существующего кода
и писать на более формальном языке - например Лиспе.
OG> Доказательство же позволит избежать полного невозможного
OG> перебора для тестирования.
Нивапрос. Если его удастся, во-первых, построить, а во-вторых,
проверить.
Построить действительно на данный момент тяжело.
Проверка же выполняется просто -
убедаемся в правильности формализации
и коректности правил вывода.
Доказательство проверится автоматичеки.
Например бегло просмотрите tutorial:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html
Тесты ту же вероятность обычно дают дешевле.
В доказательстве нет места вероятности.
Тесты могут обнаружить ошибку,
но не могут гарантировать их отсутствие,
тогда как доказательство гарантирует.
Состояние дел можно узнать по запросам HOL, verification
на http://citeseerx.ist.psu.edu/
--
С уважением, Александр Гавенко.
--
To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
Archive: http://lists.debian.org/4bd6efc3.9030...@bifit.com.ua
