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> тогда как доказательство гарантирует. Упущено ключевое слово. _Верное_ доказательство. И вот в этом слове и прячется вероятность. -- Правки Белявского, сделанные им в рабочей копии головы -- Из коммитлога. -- 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/54010...@tigger.lan.cryptocom.ru
