https://www.opennet.ru/openforum/vsluhforumID3/57847.html Ученые из австралийского исследовательского центра NICTA нашли (http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally-Proven-OS-Kernel?from=rss) способ математически доказать, что определенное ПО не содержит ошибок и, соответственно, не станет причиной отказа управляемого им оборудования. Проведение такого рода тестирования жизненно необходимо во многих отраслях промышленности, таких как, например, авиа и автомобилестроение, где сбои в бортовой компьютерной сети возникают чаще, чем поломки механических агрегатов.<br><br>Для проведения теста (http://ertos.nicta.com.au/research/l4.verified/) было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание...<br><br>URL: http://tech.sl https://www.opennet.ru/openforum/vsluhforumID3/57847.html#43 Thu, 11 Jun 2020 00:26:50 GMT &gt; only that it will always do what it is supposed to <br><br>Скорее, что она работает не выходя за рамки спецификации... Это не совсем "supposed to".<br><br>Скажем, практически все спецификации на сортировку будут удовлетворены командами sort &#124; uniq. А значительная часть спецификаций из всяких самоучителей вообще пропустит такую функцию сортировки:<br><br>sort :: Ord a =&gt; [a] -&gt; [a]<br>sort _ = []<br><br>Нельзя ведь сказать, что результат выполнения этой функции неотсортирован!<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#42 Thu, 11 Jun 2020 00:20:42 GMT +1<br><br>Новость в стиле "учёный изнасиловал журналиста". Проверка спецификации, кстати, отдельная задача. ;-)<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#41 Fri, 28 Jan 2011 13:12:03 GMT Очередное ламерство от вас :(<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#40 Fri, 28 Jan 2011 12:31:50 GMT Достаточно богата еще не значит полна. С Геделем все ОК )<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#38 Tue, 18 Aug 2009 11:00:13 GMT &gt;Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, <br>&gt;с помощью которого доказывается непротиворечивость этой теории. <br><br>Это напрямую запрещено теоремой Гёделя.<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#37 Mon, 17 Aug 2009 12:17:48 GMT А если наша Гостехкомиссия (или кто там щас вместо неё) будет юзать эту штуку - время выдачи сертификата уменьшится или увеличится?<br><br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#36 Sun, 16 Aug 2009 04:16:32 GMT Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, с помощью которого доказывается непротиворечивость этой теории.<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#35 Sat, 15 Aug 2009 15:37:18 GMT Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы для её проверки на соответствие с КОДОМ.<br> https://www.opennet.ru/openforum/vsluhforumID3/57847.html#33 Fri, 14 Aug 2009 19:36:10 GMT Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая проблема в общем случае<br>