First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 09:45
Оценка: 8 (2)
Анонс.

Обсуждение на слешдоте со ссылками.

Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.

Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re: First fully verified operating system kernel.
От: Alu Россия  
Дата: 14.08.09 11:15
Оценка:
Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ. Можно лишь показать что ПО 100% работоспособно на ограниченном мн-ве тестов. Кто-то из них неправ
Настоящему индейцу завсегда везде ништяк!
Re[2]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 11:33
Оценка: :)
Здравствуйте, Alu, Вы писали:

Alu>Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ. Можно лишь показать что ПО 100% работоспособно на ограниченном мн-ве тестов. Кто-то из них неправ


Ничего не могу сказать, поскольку информации недостаточно.

Хотя нет, могу.

Конечно же, неправ твой препод.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[3]: First fully verified operating system kernel.
От: Alu Россия  
Дата: 14.08.09 11:54
Оценка:
Здравствуйте, thesz, Вы писали:
T>Конечно же, неправ твой препод.

Тогда нас ждут интересные времена. Через некоторое время появится Specification Definition Language, на котором будут писать спеки и скармливать их верификатору ПО вместе с разработанным ПО. Тестеры станут не нужны. Потом сделают большую нейронную сеть, которую с помошью верификатора научат создовать ПО по спекам. И разработчики тоже станут не нужны. Люди вообще станут не нужны.
Смотрите в кинотеатрах города: Матрица:Верификация.
Настоящему индейцу завсегда везде ништяк!
Re[4]: First fully verified operating system kernel.
От: borisman3 Канада http://paskoboris.blogspot.com/
Дата: 14.08.09 12:02
Оценка:
Здравствуйте, Alu, Вы писали:

Alu>Здравствуйте, thesz, Вы писали:

T>>Конечно же, неправ твой препод.

Alu>Тогда нас ждут интересные времена. Через некоторое время появится Specification Definition Language, на котором будут писать спеки и скармливать их верификатору ПО вместе с разработанным ПО. Тестеры станут не нужны. Потом сделают большую нейронную сеть, которую с помошью верификатора научат создовать ПО по спекам. И разработчики тоже станут не нужны. Люди вообще станут не нужны.

Alu>Смотрите в кинотеатрах города: Матрица:Верификация.

Ошибки в спеке никто не отменял
Re[2]: First fully verified operating system kernel.
От: borisman3 Канада http://paskoboris.blogspot.com/
Дата: 14.08.09 12:09
Оценка:
Здравствуйте, Alu, Вы писали:

Alu>Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ. Можно лишь показать что ПО 100% работоспособно на ограниченном мн-ве тестов. Кто-то из них неправ


Преподаватель скорее всего доказывал неразрешимость похожей, но другой задачи.

А здесь читайте: The researchers used an executable specification written in Haskell

то бишь ресерчеры лишь доказали полное соответствие С кода спецификации на Хаскель-коде. Скорее всего С-код был получен некоей трансформацией из Хаскель-кода.

Об ошибках в Хаскель-коде даже речи не идет.
Re: First fully verified operating system kernel.
От: borisman3 Канада http://paskoboris.blogspot.com/
Дата: 14.08.09 12:11
Оценка:
Здравствуйте, thesz, Вы писали:

T>Анонс.


T>Обсуждение на слешдоте со ссылками.


T>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


Осталость всего-ничего:
1) Доказать верность спецификации
2) Доказать что железо, на котором это все исполняется, не имеет дефектов.
Re[2]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 12:51
Оценка:
T>>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.

B>Осталость всего-ничего:
B>1) Доказать верность спецификации

Можно показать верность спецификации. Небольшим набором функциональных тестов.

B>2) Доказать что железо, на котором это все исполняется, не имеет дефектов.


Это выходит за рамки обсуждения, тем не менее: Про применение ACL2 при разработке железа
Автор: thesz
Дата: 05.02.09
.

Вообще, практически все большие железки от больших производителей проверяются формальными методами.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[3]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 12:54
Оценка:
B>то бишь ресерчеры лишь доказали полное соответствие С кода спецификации на Хаскель-коде. Скорее всего С-код был получен некоей трансформацией из Хаскель-кода.

B>Об ошибках в Хаскель-коде даже речи не идет.


Код на Хаскеле проверяли Isabelle.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[5]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 13:02
Оценка:
Здравствуйте, borisman3, Вы писали:

B>Здравствуйте, Alu, Вы писали:


Alu>>Здравствуйте, thesz, Вы писали:

T>>>Конечно же, неправ твой препод.

Alu>>Тогда нас ждут интересные времена. Через некоторое время появится Specification Definition Language, на котором будут писать спеки и скармливать их верификатору ПО вместе с разработанным ПО. Тестеры станут не нужны. Потом сделают большую нейронную сеть, которую с помошью верификатора научат создовать ПО по спекам. И разработчики тоже станут не нужны. Люди вообще станут не нужны.

Alu>>Смотрите в кинотеатрах города: Матрица:Верификация.

B>Ошибки в спеке никто не отменял


Их проверить много проще.

Но самое важное то, что формальная проверка покажет все места, где исходники расходятся со спецификацией. Изменить исходники под изменившуюся спецификацию будет много проще, а главное — безопасней.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re: First fully verified operating system kernel.
От: SleepyDrago Украина  
Дата: 14.08.09 13:24
Оценка:
Здравствуйте, thesz, Вы писали:

T>Анонс.


T>Обсуждение на слешдоте со ссылками.


T>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


Не знаю что там насчет Хаскеля, но с пруфами там забавно.
Команда австралийцев :
*) не смогла доказать что их кернел работает с виртуальной памятью корректно (sic).
*) полностью проигнорировала multi-threading (omg).

так что имхо под гром фанфар они могут проследовать прямо ... в музей истории.
Re[2]: First fully verified operating system kernel.
От: D. Mon Великобритания http://thedeemon.livejournal.com
Дата: 14.08.09 14:44
Оценка: 1 (1) +1
Здравствуйте, Alu, Вы писали:

Alu>Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ. Можно лишь показать что ПО 100% работоспособно на ограниченном мн-ве тестов. Кто-то из них неправ


У нас на аналогичном предмете была чудесная формулировка "переход от неформального к формальному существенно неформален".
Re[2]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 14.08.09 14:53
Оценка:
Здравствуйте, SleepyDrago, Вы писали:

SD>Здравствуйте, thesz, Вы писали:


T>>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


SD>Не знаю что там насчет Хаскеля, но с пруфами там забавно.

SD>Команда австралийцев :
SD>*) не смогла доказать что их кернел работает с виртуальной памятью корректно (sic).
SD>*) полностью проигнорировала multi-threading (omg).

SD>так что имхо под гром фанфар они могут проследовать прямо ... в музей истории.


Я подожду.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re: First fully verified operating system kernel.
От: nikov США http://www.linkedin.com/in/nikov
Дата: 14.08.09 16:28
Оценка:
Здравствуйте, thesz, Вы писали:

T>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


Достижение, безусловно, очень важное. Тем не менее, будем ждать багов в доказанном софте из-за ошибок в процессорах, возможных ошибок в theorem prover'e, и возможной противоречивости используемой формальной системы.
Re[2]: First fully verified operating system kernel.
От: nikov США http://www.linkedin.com/in/nikov
Дата: 14.08.09 16:34
Оценка: +2
Здравствуйте, Alu, Вы писали:

Alu>Был у сокурсников предмет "Технологии разработки ПО". Преподаватель математически доказывал неразрешимость этой задачи. Доказательство я не знаю, помню только вывод о том, что нельзя говорить о 100% соответствии ПО и ТЗ.


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

Однако, это не означает, что нет алгоритма, который мог бы решить эту задачу для некоторых частных случаев.
Re: First fully verified operating system kernel.
От: Шахтер Интернет  
Дата: 14.08.09 16:59
Оценка: +4 :)))
Здравствуйте, thesz, Вы писали:

Я так понял, речь идет о доказательстве формального соответсвия 7500 строк на С коду на Haskell.
Я бы назвал это освоением средств инвесторов.
В XXI век с CCore.
Копай Нео, копай -- летать научишься. © Matrix. Парадоксы
Re: First fully verified operating system kernel.
От: Pzz Россия https://github.com/alexpevzner
Дата: 15.08.09 00:04
Оценка: +1
Здравствуйте, thesz, Вы писали:

T>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


Я не очень понимаю, в чем value. Доказана эквиавалентность кода на Haskell'е и формальной спецификации системы. Но кто сказал, что в самой формальной спецификации нет ошибок? И кстати, непонятно, почему бы вместо доказательства эквиавалентности кода просто не странслировать формальную спецификацию в исполняемый код.
Re[2]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 15.08.09 11:07
Оценка:
Здравствуйте, Pzz, Вы писали:

Pzz>Здравствуйте, thesz, Вы писали:


T>>Цитата:

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.


Pzz>Я не очень понимаю, в чем value. Доказана эквиавалентность кода на Haskell'е и формальной спецификации системы. Но кто сказал, что в самой формальной спецификации нет ошибок?


Вот все об этом говорят.

Будь так бобр (pun intented), покажи мне, чем это плохо, наличие в спецификации ошибок.

После чего я ещё раз повторю, что "теперь исправление спецификации менее трудоёмкий процесс, поскольку нам покажут, где что не так в остальном коде" и добавлю, что допустить ошибки в спецификации можно только весьма высокоуровневые, которые ловятся гораздо меньшим количеством тестов.

Если раньше (и сейчас) спецификация находилась в начале программы и исправление ошибок в ней были самые дорогие, то в будущем это всё будет не сложней исправлений ошибок типизации в языках типа C++.

Pzz>И кстати, непонятно, почему бы вместо доказательства эквиавалентности кода просто не странслировать формальную спецификацию в исполняемый код.


Отлично. Займёшься?
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
Re[3]: First fully verified operating system kernel.
От: geniepro http://geniepro.livejournal.com/
Дата: 17.08.09 04:18
Оценка:
Здравствуйте, borisman3, Вы писали:

B>то бишь ресерчеры лишь доказали полное соответствие С кода спецификации на Хаскель-коде. Скорее всего С-код был получен некоей трансформацией из Хаскель-кода.


Там вручную с Хаскелла на Си переводили (для повышения эффективности).
Re[3]: First fully verified operating system kernel.
От: fmiracle  
Дата: 17.08.09 11:23
Оценка: 4 (1)
Здравствуйте, thesz, Вы писали:

T>После чего я ещё раз повторю, что "теперь исправление спецификации менее трудоёмкий процесс, поскольку нам покажут, где что не так в остальном коде" и добавлю, что допустить ошибки в спецификации можно только весьма высокоуровневые, которые ловятся гораздо меньшим количеством тестов.


T>Если раньше (и сейчас) спецификация находилась в начале программы и исправление ошибок в ней были самые дорогие, то в будущем это всё будет не сложней исправлений ошибок типизации в языках типа C++.


Потому что для этого нужно формальное описание спецификации.
А создается спецификация на человеческом (т.е. неформальном) языке, понятном экспертам предметной области, которые формулируют задачу.

Перевод спецификации с человеческого языка в строгий формальный синтаксис лежит где-то очень близко к написанию собственно кода.

По сути дела код программы — это и есть формальное описание спецификации на языке C++, C# и т.д. И проблемы возникают из-за
1. неверной формулировки задачи экспертом при составлении человеческой спецификации.
2. ошибки при переводе с неформального человеческого языка в формальное описание того же самого на C++, Хаскель, и прочих языках.

В данном случае п.1 никак не отменяется, а п.2 заменяется возможными ошибками при переводе на "язык формального описания спецификаций".


Я не говорю что пользы тут нет никакой — плюс тут может быть, если данный язык описания формальных спецификаций будет проще и понятнее, чем соответственно текущие языки разработки. Но это радикальное решение проблемы, а частное улучшение текущей ситуации.
... << RSDN@Home 1.2.0 alpha 4 rev. 1237>>
Re[4]: First fully verified operating system kernel.
От: thesz Россия http://thesz.livejournal.com
Дата: 17.08.09 14:10
Оценка:
Здравствуйте, fmiracle, Вы писали:

F>Здравствуйте, thesz, Вы писали:


T>>После чего я ещё раз повторю, что "теперь исправление спецификации менее трудоёмкий процесс, поскольку нам покажут, где что не так в остальном коде" и добавлю, что допустить ошибки в спецификации можно только весьма высокоуровневые, которые ловятся гораздо меньшим количеством тестов.

T>>Если раньше (и сейчас) спецификация находилась в начале программы и исправление ошибок в ней были самые дорогие, то в будущем это всё будет не сложней исправлений ошибок типизации в языках типа C++.
F>Потому что для этого нужно формальное описание спецификации.

"Потому, что" открывает ответ на вопрос "почему".

Я не обнаружил вопроса в своих двух параграфах выше.

Какой же вопрос я задавал?

F>А создается спецификация на человеческом (т.е. неформальном) языке, понятном экспертам предметной области, которые формулируют задачу.

F>Перевод спецификации с человеческого языка в строгий формальный синтаксис лежит где-то очень близко к написанию собственно кода.

Ты, прошу прощения, комбинаторными библиотеками пользовался?

F>По сути дела код программы — это и есть формальное описание спецификации на языке C++, C# и т.д.


Nope. Close, but nope.

Код программы — это доказательство существования решения проблемы в ограничениях языка (C++, C#, Java, Haskell).

Спецификация — описание проблемы.

F>И проблемы возникают из-за

F>1. неверной формулировки задачи экспертом при составлении человеческой спецификации.
F>2. ошибки при переводе с неформального человеческого языка в формальное описание того же самого на C++, Хаскель, и прочих языках.

Вот здесь не надо всех равнять. Языки разные.

F>В данном случае п.1 никак не отменяется, а п.2 заменяется возможными ошибками при переводе на "язык формального описания спецификаций".


Построение доказательства существования решения подчиняется строгим правилам.

Чем лучше организованы эти правила (лучше система типов), тем быстрее мы получим ответ "ошибка в спецификации".

F>Я не говорю что пользы тут нет никакой — плюс тут может быть, если данный язык описания формальных спецификаций будет проще и понятнее, чем соответственно текущие языки разработки. Но это радикальное решение проблемы, а частное улучшение текущей ситуации.


Ну, да.

Иерархия вселенных.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.