Re: сертификация
On 2010.04.27 17:54, Artem Chuprina wrote:
Oleksandr Gavenko -> debian-russian@lists.debian.org @ Tue, 27 Apr 2010 17:08:03 +0300:
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
OK!
Реализацию лиспа, на которой оно выполняется, кто доказывать будет?
-Пушкин- МакКарти?
Было бы время и возможности.
И в общем, да, ты тот лисп вообще видел? Программы на нем писал?
не CL но elisp достаточно, но это не важно
Отлаживал? А реальные программы, не учебные задачи? Я б тебя еще
понял, если б ты Хаскель назвал - тот чисто функциональный, там
действительно существенно легче верифицировать. А как только у тебя
в языке есть присваивание - все, туши свет...
в этой области профан
>> OG> Доказательство же позволит избежать полного невозможного
>> OG> перебора для тестирования.
>>
>> Нивапрос. Если его удастся, во-первых, построить, а во-вторых,
>> проверить.
OG> Построить действительно на данный момент тяжело.
OG> Проверка же выполняется просто -
OG> убедаемся в правильности формализации
OG> и коректности правил вывода.
"Ты пальцем покажи". В смысле - предъяви доказательство правильности
формализации любого _практического_ программно-аппаратного комплекса.
http://ertos.nicta.com.au/research/sel4/
Информация разбросана по инету.
OG> Доказательство проверится автоматичеки.
Автоматическую проверялку доказательства уже доказали? А автомат, на
котором оно проверяет?
Было бы время и возможности.
Но сложности все таки есть. Например
http://en.wikipedia.org/wiki/Kepler_conjecture
из осторожности не признают доказанной. Хотя машинное доказательство
http://en.wikipedia.org/wiki/Four_color_theorem#Proof_by_computer
было принято общественностью.
>> Тесты ту же вероятность обычно дают дешевле.
>>
OG> В доказательстве нет места вероятности.
Это очень наивное утверждение. Мягко говоря, не соответствующее действительности.
Из wikipedia:
In 2005 Benjamin Werner and Georges Gonthier formalized a proof of the
four color theorem inside the Coq proof assistant. This removed the need
to trust the various computer programs used to verify particular cases;
it is only necessary to *trust* the Coq kernel.
Вероятности *нет*.
Говорю как человек, который не только знает историю
великой теоремы Ферма, но и сам на практике предъявлял доказательство,
ошибку в котором нашел только третий проверяющий.
Я, знаешь ли, теорией доказательств на практике занимался...
У нас в университете один из преподавателей в 70-ых тоже ошибся,
всего лишь на 27 странице...
OG> Тесты могут обнаружить ошибку,
OG> но не могут гарантировать их отсутствие,
OG> тогда как доказательство гарантирует.
Упущено ключевое слово. _Верное_ доказательство. И вот в этом слове и
прячется вероятность.
http://en.wikipedia.org/wiki/Computer-assisted_proof
http://en.wikipedia.org/wiki/Interactive_theorem_proving
http://en.wikipedia.org/wiki/Automated_proof_checking
Ошибки в реализации конечно возможны, но замечу
что доказательства прогонялись на различных версиях
и для некоторых сложных мат. теорем имеются доказательства
в различных системах.
Было бы время и возможности для проверки правильности реализации
proof checker'а.
Я верю что спустя некоторое время общественность примет машинные
доказательства как равносильные бумажным.
И более *вероятность* правильности доказательства не будет пугать.
--
С уважением, Александр Гавенко.
Reply to: