Ученые из австралийского исследовательского центра NICTA нашли (http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First...) способ математически доказать, что определенное ПО не содержит ошибок и, соответственно, не станет причиной отказа управляемого им оборудования. Проведение такого рода тестирования жизненно необходимо во многих отраслях промышленности, таких как, например, авиа и автомобилестроение, где сбои в бортовой компьютерной сети возникают чаще, чем поломки механических агрегатов.Для проведения теста (http://ertos.nicta.com.au/research/l4.verified/) было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание...
URL: http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First...
Новость: http://www.opennet.dev/opennews/art.shtml?num=23011
что-то они там упустили
Ну ты им расскажи об этом.
У нас сегодня определенно день надуманных новостей. В тексте новости явно рассказано, что исследователям удалось создать первое ядро системы для которого для которого было проведено доказательство 100% соответствия тех.заданию. (First Formally-Proven OS Kernel).А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.
И как правильно заметили в комментарии к исходной новости:It only means it meets the spec, not that the spec is correct ...
It does not mean that the faulty or erratic hardware cannot crash the system
It does not mean that other programs cannot crash and lose your data ...
It does not mean that buggy device drivers can make your system unusable
It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...
Ну и нормально. И хорошо, что пока еще не изобрели методику, которая за меня определяет _что_ я хочу. :)
> only that it will always do what it is supposed toСкорее, что она работает не выходя за рамки спецификации... Это не совсем "supposed to".
Скажем, практически все спецификации на сортировку будут удовлетворены командами sort | uniq. А значительная часть спецификаций из всяких самоучителей вообще пропустит такую функцию сортировки:
sort :: Ord a => [a] -> [a]
sort _ = []Нельзя ведь сказать, что результат выполнения этой функции неотсортирован!
> А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.Вот-вот. Поправьте новость уже, без слез смотреть нельзя.
Риторический вопрос: как верифицировать верификатор?
Первый вопрос, который пришёл в голову. Лем очень неплохо в Ананке над верификаторами постебался.
примерно так же, как компилируют компиляторы: первым делом ;-)
> Риторический вопрос: как верифицировать верификатор?Так ведь как обычно. Выбрать аксиоматику (ту же ZFC) и пожалуйста, в бой.
Никак. "Проблема обнаружения закладки в компиляторе" неразрешима.
Очередное ламерство от вас :(
И все равно непонятно, что именно доказано?
>математически доказать, что определенное ПО не содержит ошибокСлишком общая формулировка. Никакой конкретики.
>И все равно непонятно, что именно доказано?Доказано соответствие спецификации.
А кто будет отлавливать баги в Isabelle???
ого! (просто нет других слов)
Пускай программу проверки проверят ею же. не исключено что программа не пройдет проверки корректности ;)
+1. Если они действительно смогут математически доказывать корректность программы, то это уменьшит количество проблем и багов на порядок.
Это смотря кем ещё программа написана. Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.
Угу. Вечный вопрос - "можно ли математически описать хаос?". Как-то тоже пришлось поглядеть на творчество и фантазию "программных гениев" изнутри.
> Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.дык в этом случае пофигу - прописать в ТЗ что код должен проходить анализ. Потому сдыхание анализатора это несоответствие ТЗ, а сам програмер идет переучиваться.
Выдержка из с их страницы (statistic):
=======
Сколько строк было проверено?
> 7500 строк на C. Пока не проверен эсемблерный код и код, ответственный за загрузку (1200 строк)Насколько большое получилось доказательство?
Около 200000 строк кода на языке доказательств Isabelle. Весь код доказательства был написан вручную с последующей машинной проверкой. В сумме это приблизительно 3500 страниц формата A4, если его распечатать (высота распечатки будет около полуметра высотой).
Это одно из самых больших формальных доказательств из когда-либо сделаных. Для примера, известная теорема о четырех красках (которая тоже была доказана машиной) состояла из 60000 строк в доказательстве теоремы. Единственное известное доказательство, которое больше этого принадлежит проекту Verisoft (они сообщают о 245000 строк доказательства). И конечно, в математике, чем меньше доказательство, тем оно понятнее :)
=======Так что ни о каком прорыве в программировании речи не идет.
> Так что ни о каком прорыве в программировании речи не идет.прорыв будет если мат.правила для доказательства будут примерно 1-1 к коду.
>> Итоговый анализ выполняется с помощью интерактивной программы IsabelleА кто проверит Isabelle? Вдруг там ошибка?
Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая проблема в общем случае
+1Новость в стиле "учёный изнасиловал журналиста". Проверка спецификации, кстати, отдельная задача. ;-)
Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы для её проверки на соответствие с КОДОМ.
Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, с помощью которого доказывается непротиворечивость этой теории.
>Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий,
>с помощью которого доказывается непротиворечивость этой теории.Это напрямую запрещено теоремой Гёделя.
Достаточно богата еще не значит полна. С Геделем все ОК )
А если наша Гостехкомиссия (или кто там щас вместо неё) будет юзать эту штуку - время выдачи сертификата уменьшится или увеличится?