forum.opennet.ru - "Найден способ формального подтверждения соответствия ПО техн..." (32)

"Найден способ формального подтверждения соответствия ПО техн..."

Форум Разговоры, обсуждение новостей
Вариант для распечатки		Пред. тема \| След. тема
Изначальное сообщение		[ Отслеживать ]

"Найден способ формального подтверждения соответствия ПО техн..."	+/–
Сообщение от opennews (??), 14-Авг-09, 12:51
Ученые из австралийского исследовательского центра 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.me/opennews/art.shtml?num=23011
Ответить \| Правка \| Cообщить модератору

Оглавление

что-то они там упустили, Аноним (-), 12:51 , 14-Авг-09, (1) –2
Ну ты им расскажи об этом , AlexanderYT (?), 12:56 , 14-Авг-09, (2) –4
У нас сегодня определенно день надуманных новостей В тексте новости явно расска, Aleksey (??), 13:03 , 14-Авг-09, (3) +2

И как правильно заметили в комментарии к исходной новости It only means it meets, Aleksey (??), 13:04 , 14-Авг-09, (4) +3

Ну и нормально И хорошо, что пока еще не изобрели методику, которая за меня опр, dq0s4y71 (?), 13:20 , 14-Авг-09, (6) +1
Скорее, что она работает не выходя за рамки спецификации Это не совсем suppo, Vkni (ok), 03:26 , 11-Июн-20, (43)

Вот-вот Поправьте новость уже, без слез смотреть нельзя , anonymous (??), 15:42 , 14-Авг-09, (26) +1

Риторический вопрос как верифицировать верификатор , anonimous (?), 13:17 , 14-Авг-09, (5) +2

Первый вопрос, который пришёл в голову Лем очень неплохо в Ананке над верификат, zazik (ok), 13:48 , 14-Авг-09, (10)
примерно так же, как компилируют компиляторы первым делом - , nathoo (?), 15:21 , 14-Авг-09, (23) +2
Так ведь как обычно Выбрать аксиоматику ту же ZFC и пожалуйста, в бой , anonymous (??), 15:24 , 14-Авг-09, (24)
Никак Проблема обнаружения закладки в компиляторе неразрешима , Andrew Kolchoogin (?), 20:53 , 14-Авг-09, (29)

Очередное ламерство от вас , Аноним (-), 16:12 , 28-Янв-11, (41)

И все равно непонятно, что именно доказано Слишком общая формулировка Никакой к, FractalizeR (ok), 13:21 , 14-Авг-09, (7) +2

Доказано соответствие спецификации , Аноним (8), 13:28 , 14-Авг-09, (8) –1

А кто будет отлавливать баги в Isabelle , white_raven (?), 13:50 , 14-Авг-09, (11)
ого просто нет других слов , psyhomo (?), 13:50 , 14-Авг-09, (12)
Пускай программу проверки проверят ею же не исключено что программа не пройдет , fooser (?), 13:52 , 14-Авг-09, (13)
1 Если они действительно смогут математически доказывать корректность программ, uZver (??), 14:09 , 14-Авг-09, (14) –1

Это смотря кем ещё программа написана Есть такие программные гении которые даж, Имя (?), 14:26 , 14-Авг-09, (15)

Угу Вечный вопрос - можно ли математически описать хаос Как-то тоже пришлос, psyhomo (?), 15:01 , 14-Авг-09, (20)
дык в этом случае пофигу - прописать в ТЗ что код должен проходить анализ Потом, uZver (??), 21:53 , 14-Авг-09, (31)

Выдержка из с их страницы statistic Сколько строк было проверено Наскол, Aleksey (??), 15:15 , 14-Авг-09, (22) +2

прорыв будет если мат правила для доказательства будут примерно 1-1 к коду , uZver (??), 21:55 , 14-Авг-09, (32) +1

А кто проверит Isabelle Вдруг там ошибка , Slava_K (?), 21:32 , 14-Авг-09, (30) –1
Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая про, аноним (?), 23:36 , 14-Авг-09, (33)

1Новость в стиле учёный изнасиловал журналиста Проверка спецификации, кстати, Vkni (ok), 03:20 , 11-Июн-20, (42)

Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы д, Качатель (?), 19:37 , 15-Авг-09, (35)
Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей, FrBrGeorge (ok), 08:16 , 16-Авг-09, (36)

Это напрямую запрещено теоремой Гёделя , nuclight (??), 15:00 , 18-Авг-09, (38)

Достаточно богата еще не значит полна С Геделем все ОК , Аноним (-), 15:31 , 28-Янв-11, (40)

А если наша Гостехкомиссия или кто там щас вместо неё будет юзать эту штуку - , Онаним (?), 16:17 , 17-Авг-09, (37)

Сообщения [Сортировка по времени | RSS]

1. "Найден способ формального подтверждения соответствия ПО техн..." –2 +/–

Сообщение от Аноним (-), 14-Авг-09, 12:51

что-то они там упустили

Ответить | Правка | Наверх | Cообщить модератору

2. "Найден способ формального подтверждения соответствия ПО техн..." –4 +/–

Сообщение от AlexanderYT (?), 14-Авг-09, 12:56

Ну ты им расскажи об этом.

Ответить | Правка | Наверх | Cообщить модератору

3. "Найден способ формального подтверждения соответствия ПО техн..." +2 +/–

Сообщение от Aleksey (??), 14-Авг-09, 13:03

У нас сегодня определенно день надуманных новостей. В тексте новости явно рассказано, что исследователям удалось создать первое ядро системы для которого для которого было проведено доказательство 100% соответствия тех.заданию. (First Formally-Proven OS Kernel).
А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.

Ответить | Правка | Наверх | Cообщить модератору

4. "Найден способ формального подтверждения соответствия ПО техн..." +3 +/–

Сообщение от Aleksey (??), 14-Авг-09, 13:04

И как правильно заметили в комментарии к исходной новости:
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 ...

Ответить | Правка | Наверх | Cообщить модератору

6. "Найден способ формального подтверждения соответствия ПО техн..." +1 +/–

Сообщение от dq0s4y71 (?), 14-Авг-09, 13:20

Ну и нормально. И хорошо, что пока еще не изобрели методику, которая за меня определяет _что_ я хочу. :)

Ответить | Правка | Наверх | Cообщить модератору

43. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от Vkni (ok), 11-Июн-20, 03:26

> only that it will always do what it is supposed to
Скорее, что она работает не выходя за рамки спецификации... Это не совсем "supposed to".
Скажем, практически все спецификации на сортировку будут удовлетворены командами sort | uniq. А значительная часть спецификаций из всяких самоучителей вообще пропустит такую функцию сортировки:
sort :: Ord a => [a] -> [a]
sort _ = []
Нельзя ведь сказать, что результат выполнения этой функции неотсортирован!

Ответить | Правка | К родителю #4 | Наверх | Cообщить модератору

26. "Найден способ формального подтверждения соответствия ПО техн..." +1 +/–

Сообщение от anonymous (??), 14-Авг-09, 15:42

> А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.
Вот-вот. Поправьте новость уже, без слез смотреть нельзя.

Ответить | Правка | К родителю #3 | Наверх | Cообщить модератору

5. "Найден способ формального подтверждения соответствия ПО техн..." +2 +/–

Сообщение от anonimous (?), 14-Авг-09, 13:17

Риторический вопрос: как верифицировать верификатор?

Ответить | Правка | Наверх | Cообщить модератору

10. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от zazik (ok), 14-Авг-09, 13:48

Первый вопрос, который пришёл в голову. Лем очень неплохо в Ананке над верификаторами постебался.

Ответить | Правка | Наверх | Cообщить модератору

23. "Найден способ формального подтверждения соответствия ПО техн..." +2 +/–

Сообщение от nathoo (?), 14-Авг-09, 15:21

примерно так же, как компилируют компиляторы: первым делом ;-)

Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

24. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от anonymous (??), 14-Авг-09, 15:24

> Риторический вопрос: как верифицировать верификатор?
Так ведь как обычно. Выбрать аксиоматику (ту же ZFC) и пожалуйста, в бой.

Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

29. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от Andrew Kolchoogin (?), 14-Авг-09, 20:53

Никак. "Проблема обнаружения закладки в компиляторе" неразрешима.

Ответить | Правка | К родителю #5 | Наверх | Cообщить модератору

41. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от Аноним (-), 28-Янв-11, 16:12

Очередное ламерство от вас :(

Ответить | Правка | Наверх | Cообщить модератору

7. "Найден способ формального подтверждения соответствия ПО техн..." +2 +/–

Сообщение от FractalizeR (ok), 14-Авг-09, 13:21

И все равно непонятно, что именно доказано?
>математически доказать, что определенное ПО не содержит ошибок
Слишком общая формулировка. Никакой конкретики.

Ответить | Правка | Наверх | Cообщить модератору

8. "Найден способ формального подтверждения соответствия ПО техн..." –1 +/–

Сообщение от Аноним (8), 14-Авг-09, 13:28

>И все равно непонятно, что именно доказано?
Доказано соответствие спецификации.

Ответить | Правка | Наверх | Cообщить модератору

11. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от white_raven (?), 14-Авг-09, 13:50

А кто будет отлавливать баги в Isabelle???

Ответить | Правка | Наверх | Cообщить модератору

12. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от psyhomo (?), 14-Авг-09, 13:50

ого! (просто нет других слов)

Ответить | Правка | Наверх | Cообщить модератору

13. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от fooser (?), 14-Авг-09, 13:52

Пускай программу проверки проверят ею же. не исключено что программа не пройдет проверки корректности ;)

Ответить | Правка | Наверх | Cообщить модератору

14. "Найден способ формального подтверждения соответствия ПО техн..." –1 +/–

Сообщение от uZver (??), 14-Авг-09, 14:09

+1. Если они действительно смогут математически доказывать корректность программы, то это уменьшит количество проблем и багов на порядок.

Ответить | Правка | Наверх | Cообщить модератору

15. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от Имя (?), 14-Авг-09, 14:26

Это смотря кем ещё программа написана. Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.

Ответить | Правка | Наверх | Cообщить модератору

20. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от psyhomo (?), 14-Авг-09, 15:01

Угу. Вечный вопрос - "можно ли математически описать хаос?". Как-то тоже пришлось поглядеть на творчество и фантазию "программных гениев" изнутри.

Ответить | Правка | Наверх | Cообщить модератору

31. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от uZver (??), 14-Авг-09, 21:53

> Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.
дык в этом случае пофигу - прописать в ТЗ что код должен проходить анализ. Потому сдыхание анализатора это несоответствие ТЗ, а сам програмер идет переучиваться.

Ответить | Правка | К родителю #15 | Наверх | Cообщить модератору

22. "Найден способ формального подтверждения соответствия ПО техн..." +2 +/–

Сообщение от Aleksey (??), 14-Авг-09, 15:15

Выдержка из с их страницы (statistic):
=======
Сколько строк было проверено?
> 7500 строк на C. Пока не проверен эсемблерный код и код, ответственный за загрузку (1200 строк)
Насколько большое получилось доказательство?
Около 200000 строк кода на языке доказательств Isabelle. Весь код доказательства был написан вручную с последующей машинной проверкой. В сумме это приблизительно 3500 страниц формата A4, если его распечатать (высота распечатки будет около полуметра высотой).
Это одно из самых больших формальных доказательств из когда-либо сделаных. Для примера, известная теорема о четырех красках (которая тоже была доказана машиной) состояла из 60000 строк в доказательстве теоремы. Единственное известное доказательство, которое больше этого принадлежит проекту Verisoft (они сообщают о 245000 строк доказательства). И конечно, в математике, чем меньше доказательство, тем оно понятнее :)
=======
Так что ни о каком прорыве в программировании речи не идет.

Ответить | Правка | К родителю #14 | Наверх | Cообщить модератору

32. "Найден способ формального подтверждения соответствия ПО техн..." +1 +/–

Сообщение от uZver (??), 14-Авг-09, 21:55

> Так что ни о каком прорыве в программировании речи не идет.
прорыв будет если мат.правила для доказательства будут примерно 1-1 к коду.

Ответить | Правка | Наверх | Cообщить модератору

30. "Найден способ формального подтверждения 100% отсутствия ошиб..." –1 +/–

Сообщение от Slava_K (?), 14-Авг-09, 21:32

>> Итоговый анализ выполняется с помощью интерактивной программы Isabelle
А кто проверит Isabelle? Вдруг там ошибка?

Ответить | Правка | Наверх | Cообщить модератору

33. "Найден способ формального подтверждения 100% отсутствия ошиб..." +/–

Сообщение от аноним (?), 14-Авг-09, 23:36

Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая проблема в общем случае

Ответить | Правка | Наверх | Cообщить модератору

42. "Найден способ формального подтверждения 100% отсутствия ошиб..." +/–

Сообщение от Vkni (ok), 11-Июн-20, 03:20

+1
Новость в стиле "учёный изнасиловал журналиста". Проверка спецификации, кстати, отдельная задача. ;-)

Ответить | Правка | Наверх | Cообщить модератору

35. "Найден способ формального подтверждения 100% отсутствия ошиб..." +/–

Сообщение от Качатель (?), 15-Авг-09, 19:37

Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы для её проверки на соответствие с КОДОМ.

Ответить | Правка | Наверх | Cообщить модератору

36. "Решена задача самоприменимости!" +/–

Сообщение от FrBrGeorge (ok), 16-Авг-09, 08:16

Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, с помощью которого доказывается непротиворечивость этой теории.

Ответить | Правка | Наверх | Cообщить модератору

38. "Решена задача самоприменимости!" +/–

Сообщение от nuclight (??), 18-Авг-09, 15:00

>Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий,
>с помощью которого доказывается непротиворечивость этой теории.
Это напрямую запрещено теоремой Гёделя.

Ответить | Правка | Наверх | Cообщить модератору

40. "Решена задача самоприменимости!" +/–

Сообщение от Аноним (-), 28-Янв-11, 15:31

Достаточно богата еще не значит полна. С Геделем все ОК )

Ответить | Правка | Наверх | Cообщить модератору

37. "Найден способ формального подтверждения соответствия ПО техн..." +/–

Сообщение от Онаним (?), 17-Авг-09, 16:17

А если наша Гостехкомиссия (или кто там щас вместо неё) будет юзать эту штуку - время выдачи сертификата уменьшится или увеличится?

Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру

1. "Найден способ формального подтверждения соответствия ПО техн..."	–2 +/–
Сообщение от Аноним (-), 14-Авг-09, 12:51
что-то они там упустили
Ответить \| Правка \| Наверх \| Cообщить модератору

2. "Найден способ формального подтверждения соответствия ПО техн..."	–4 +/–
Сообщение от AlexanderYT (?), 14-Авг-09, 12:56
Ну ты им расскажи об этом.
Ответить \| Правка \| Наверх \| Cообщить модератору

3. "Найден способ формального подтверждения соответствия ПО техн..."	+2 +/–
Сообщение от Aleksey (??), 14-Авг-09, 13:03
У нас сегодня определенно день надуманных новостей. В тексте новости явно рассказано, что исследователям удалось создать первое ядро системы для которого для которого было проведено доказательство 100% соответствия тех.заданию. (First Formally-Proven OS Kernel). А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо.
Ответить \| Правка \| Наверх \| Cообщить модератору


	4. "Найден способ формального подтверждения соответствия ПО техн..."	+3 +/–
	Сообщение от Aleksey (??), 14-Авг-09, 13:04
	И как правильно заметили в комментарии к исходной новости: 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 ...
	Ответить \| Правка \| Наверх \| Cообщить модератору


	6. "Найден способ формального подтверждения соответствия ПО техн..."	+1 +/–
	Сообщение от dq0s4y71 (?), 14-Авг-09, 13:20
	Ну и нормально. И хорошо, что пока еще не изобрели методику, которая за меня определяет _что_ я хочу. :)
	Ответить \| Правка \| Наверх \| Cообщить модератору


	43. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от Vkni (ok), 11-Июн-20, 03:26
	> only that it will always do what it is supposed to Скорее, что она работает не выходя за рамки спецификации... Это не совсем "supposed to". Скажем, практически все спецификации на сортировку будут удовлетворены командами sort \| uniq. А значительная часть спецификаций из всяких самоучителей вообще пропустит такую функцию сортировки: sort :: Ord a => [a] -> [a] sort _ = [] Нельзя ведь сказать, что результат выполнения этой функции неотсортирован!
	Ответить \| Правка \| К родителю #4 \| Наверх \| Cообщить модератору


	26. "Найден способ формального подтверждения соответствия ПО техн..."	+1 +/–
	Сообщение от anonymous (??), 14-Авг-09, 15:42
	> А механизмы доказательства корректности алгоритмов известны не одно десятилетие и вовсю применяются в областях, где это необходимо. Вот-вот. Поправьте новость уже, без слез смотреть нельзя.
	Ответить \| Правка \| К родителю #3 \| Наверх \| Cообщить модератору

5. "Найден способ формального подтверждения соответствия ПО техн..."	+2 +/–
Сообщение от anonimous (?), 14-Авг-09, 13:17
Риторический вопрос: как верифицировать верификатор?
Ответить \| Правка \| Наверх \| Cообщить модератору


	10. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от zazik (ok), 14-Авг-09, 13:48
	Первый вопрос, который пришёл в голову. Лем очень неплохо в Ананке над верификаторами постебался.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	23. "Найден способ формального подтверждения соответствия ПО техн..."	+2 +/–
	Сообщение от nathoo (?), 14-Авг-09, 15:21
	примерно так же, как компилируют компиляторы: первым делом ;-)
	Ответить \| Правка \| К родителю #5 \| Наверх \| Cообщить модератору


	24. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от anonymous (??), 14-Авг-09, 15:24
	> Риторический вопрос: как верифицировать верификатор? Так ведь как обычно. Выбрать аксиоматику (ту же ZFC) и пожалуйста, в бой.
	Ответить \| Правка \| К родителю #5 \| Наверх \| Cообщить модератору


	29. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от Andrew Kolchoogin (?), 14-Авг-09, 20:53
	Никак. "Проблема обнаружения закладки в компиляторе" неразрешима.
	Ответить \| Правка \| К родителю #5 \| Наверх \| Cообщить модератору


	41. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от Аноним (-), 28-Янв-11, 16:12
	Очередное ламерство от вас :(
	Ответить \| Правка \| Наверх \| Cообщить модератору

7. "Найден способ формального подтверждения соответствия ПО техн..."	+2 +/–
Сообщение от FractalizeR (ok), 14-Авг-09, 13:21
И все равно непонятно, что именно доказано? >математически доказать, что определенное ПО не содержит ошибок Слишком общая формулировка. Никакой конкретики.
Ответить \| Правка \| Наверх \| Cообщить модератору


	8. "Найден способ формального подтверждения соответствия ПО техн..."	–1 +/–
	Сообщение от Аноним (8), 14-Авг-09, 13:28
	>И все равно непонятно, что именно доказано? Доказано соответствие спецификации.
	Ответить \| Правка \| Наверх \| Cообщить модератору

11. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
Сообщение от white_raven (?), 14-Авг-09, 13:50
А кто будет отлавливать баги в Isabelle???
Ответить \| Правка \| Наверх \| Cообщить модератору

12. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
Сообщение от psyhomo (?), 14-Авг-09, 13:50
ого! (просто нет других слов)
Ответить \| Правка \| Наверх \| Cообщить модератору

13. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
Сообщение от fooser (?), 14-Авг-09, 13:52
Пускай программу проверки проверят ею же. не исключено что программа не пройдет проверки корректности ;)
Ответить \| Правка \| Наверх \| Cообщить модератору

14. "Найден способ формального подтверждения соответствия ПО техн..."	–1 +/–
Сообщение от uZver (??), 14-Авг-09, 14:09
+1. Если они действительно смогут математически доказывать корректность программы, то это уменьшит количество проблем и багов на порядок.
Ответить \| Правка \| Наверх \| Cообщить модератору


	15. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от Имя (?), 14-Авг-09, 14:26
	Это смотря кем ещё программа написана. Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	20. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от psyhomo (?), 14-Авг-09, 15:01
	Угу. Вечный вопрос - "можно ли математически описать хаос?". Как-то тоже пришлось поглядеть на творчество и фантазию "программных гениев" изнутри.
	Ответить \| Правка \| Наверх \| Cообщить модератору


	31. "Найден способ формального подтверждения соответствия ПО техн..."	+/–
	Сообщение от uZver (??), 14-Авг-09, 21:53
	> Есть такие программные гении (которые даже не знают что такое указатель), что анализируя их программы быстро исдохнет любая математическая логика. дык в этом случае пофигу - прописать в ТЗ что код должен проходить анализ. Потому сдыхание анализатора это несоответствие ТЗ, а сам програмер идет переучиваться.
	Ответить \| Правка \| К родителю #15 \| Наверх \| Cообщить модератору


	22. "Найден способ формального подтверждения соответствия ПО техн..."	+2 +/–
	Сообщение от Aleksey (??), 14-Авг-09, 15:15
	Выдержка из с их страницы (statistic): ======= Сколько строк было проверено? > 7500 строк на C. Пока не проверен эсемблерный код и код, ответственный за загрузку (1200 строк) Насколько большое получилось доказательство? Около 200000 строк кода на языке доказательств Isabelle. Весь код доказательства был написан вручную с последующей машинной проверкой. В сумме это приблизительно 3500 страниц формата A4, если его распечатать (высота распечатки будет около полуметра высотой). Это одно из самых больших формальных доказательств из когда-либо сделаных. Для примера, известная теорема о четырех красках (которая тоже была доказана машиной) состояла из 60000 строк в доказательстве теоремы. Единственное известное доказательство, которое больше этого принадлежит проекту Verisoft (они сообщают о 245000 строк доказательства). И конечно, в математике, чем меньше доказательство, тем оно понятнее :) ======= Так что ни о каком прорыве в программировании речи не идет.
	Ответить \| Правка \| К родителю #14 \| Наверх \| Cообщить модератору


	32. "Найден способ формального подтверждения соответствия ПО техн..."	+1 +/–
	Сообщение от uZver (??), 14-Авг-09, 21:55
	> Так что ни о каком прорыве в программировании речи не идет. прорыв будет если мат.правила для доказательства будут примерно 1-1 к коду.
	Ответить \| Правка \| Наверх \| Cообщить модератору

30. "Найден способ формального подтверждения 100% отсутствия ошиб..."	–1 +/–
Сообщение от Slava_K (?), 14-Авг-09, 21:32
>> Итоговый анализ выполняется с помощью интерактивной программы Isabelle А кто проверит Isabelle? Вдруг там ошибка?
Ответить \| Правка \| Наверх \| Cообщить модератору

33. "Найден способ формального подтверждения 100% отсутствия ошиб..."	+/–
Сообщение от аноним (?), 14-Авг-09, 23:36
Не отсутствия ошибок, а соответствия спецификации, а вообще это неразрешимая проблема в общем случае
Ответить \| Правка \| Наверх \| Cообщить модератору


	42. "Найден способ формального подтверждения 100% отсутствия ошиб..."	+/–
	Сообщение от Vkni (ok), 11-Июн-20, 03:20
	+1 Новость в стиле "учёный изнасиловал журналиста". Проверка спецификации, кстати, отдельная задача. ;-)
	Ответить \| Правка \| Наверх \| Cообщить модератору

35. "Найден способ формального подтверждения 100% отсутствия ошиб..."	+/–
Сообщение от Качатель (?), 15-Авг-09, 19:37
Каким образом они собираются ТЕКСТОВУЮ спецификацию подавать на вход программы для её проверки на соответствие с КОДОМ.
Ответить \| Правка \| Наверх \| Cообщить модератору

36. "Решена задача самоприменимости!"	+/–
Сообщение от FrBrGeorge (ok), 16-Авг-09, 08:16
Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, с помощью которого доказывается непротиворечивость этой теории.
Ответить \| Правка \| Наверх \| Cообщить модератору


	38. "Решена задача самоприменимости!"	+/–
	Сообщение от nuclight (??), 18-Авг-09, 15:00
	>Следующий шаг -- создание достаточно богатой непротиворечивой теории, включающей в себя инструментарий, >с помощью которого доказывается непротиворечивость этой теории. Это напрямую запрещено теоремой Гёделя.
	Ответить \| Правка \| Наверх \| Cообщить модератору