OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Суббота, 22 Сентябрь, 2018 20:21

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 26 ]  На страницу Пред.  1, 2
Автор Сообщение
СообщениеДобавлено: Суббота, 10 Март, 2018 02:33 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 693
Откуда: Киев
Владимир Ситников писал(а):
1) В репозитории "доказательств" seL4 код вообще на Haskell. Круто. Чего ж.

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

Цитата:
Те же seL4 говорят, что они предполагают идеальную работу железа. Ну, да, конечно
Вы хотели, чтобы они сотворили чудо и исправили кривое железо, а иначе не годится?

Цитата:
FDIV всегда работало верно. Иными словами, если возникает глюк железа, то всё их хвалёное доказательство трещит по швам
3) В seL4 английским по белому написано, что их "доказательство" не доказывает отсутствие timing атак. Иными словами, Spectre, Meltdown их доказательство никак не обнаруживает.
С какой стати? У них есть участок, за который они отвечают. Они его проработали. Что Вы ещё хотите, чтобы они ещё и пролёт высокоэнергетических частиц просчитали и брак на заводе учли и от сбоящей память защитили? Каким боком это относится к доказательству программ, или любым другим методам отладки? Может быть, Вы пошаговой отладкой собрались Meltdown обнаруживать?

Цитата:
4) Нужно понимать, что seL4 используют свой "доказанный" (ну или как там) компилятор.
Нет, они используют другой подход, но доказанный оптимизирующий компилятор C существует - CompCert. Впрочем, у него за рамками доказательства оказался парсер, генерируемый компилятором грамматик Menhir.

Цитата:
Понятно дело, что когда формальной верификацией покрыто 100% кода (в том числе микрокод процессоров), то это хорошо. И? Хотя бы 5% проектов находятся в таком состоянии? Море проектов, которые просто берут GCC и/или LLVM/Clang и радуются.
И что, если нам приходится использовать другое ПО, то всё - конец? Это аргумент той же силы, что "я буду курить, потому что и так дышу городским загазованным автомобилями воздухом".

Цитата:
Поймите меня правильно. Разумеется, где-то спецификация может и помочь. Но моё исходное мнение было в том, что есть много случаев, когда пошаговая отладка очень полезна.
Внимательно следите за руками. Сначала Вы утверждаете, что согласно теореме Прайса, доказывать код невозможно. Когда я указываю, что из теоремы Прайса нет такого следствия, Вы просите объяснить подробней. Сначала я показываю на простейшем примере, что код, всё-таки, в каких-то случаях можно доказывать и даю ссылки на гораздо более серьёзные учебные примеры. Затем даю ссылку на промышленное применение, так как понимаю, что это следующий этап разговора, благо раньше у людей уже возникали такие запросы. После этого Вы меняете показания и, снабжая свою речь утончённым сарказмом, начинаете писать, что, мол, доказательство корректности не умеет превращать воду в вино, не исцеляет прокажённых от болезни и, вообще, "Круто. Чего ж. Ну, да, конечно", так, как будто утверждалось обратное. Я ответил на конкретный вопрос, а не на некие домыслы, которые в итоге посыпались.

Цитата:
В той же теме я услышал "пошаговая отладка это разврат мозга на уровне импринтинга". Так там было? Ну, пусть так и будет.
У этого обсуждения есть конкретный контекст - школьная версия, образовательная система, базовые знания.
У Вас другое мнение? Я считаю это нормальным.

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

Цитата:
Я понял, что вы показали как спецификация связана с реальным C кодом.
Да, это, конечно, забавнее, чем писать программу отдельно, а Coq доказательство отдельно.
Но означает ли это, что код в farma-c стиле не требует пошаговой отладки?
По-моему, не означает.
1) Например, в самой спецификации может быть ошибка. Как её обнаружить? Вдумчиво глядеть на все спецификации?
Ну, подаём в программу массив, а она один из элементов "не туда" сортирует. Ответ "работает согласно спецификации",

Как Вы себе представляете такую спецификацию?

Цитата:
3) Что, если будет ошибка в компиляторе? Ну, подаём данные на вход, а выход неверный. Спецификация на месте. Как искать ошибку?
А, Вы, наверно, думаете, что наличие доказательства отменяет тесты? Нет, спецификация - это половина информации для тестов. На "трудные" вопросы про компиляторы уже давно даны и даже стандартизированы ответы. Дмитрий Дагаев делился этими ответами касательно стандарта создания критичного ПО для АЭС. Ответы верны даже в случае аллергии на доказательства ПО.

Цитата:
4) Что, если ошибка в памяти? Ну, записывается одно значение, а читается другое. Так вам спецификация на farma-c поможет
Всё ждём воскрешения мёртвых? Ответ всё там же, у Дмитрия.

Цитата:
5) Что, если ошибка в сторонней системе? Пишете, например, клиентское приложение к PostgreSQL. Обложились спецификациями. А в реальности -- в PostgreSQL море ошибок. Как искать?
Как я уже писал, спецификации под доказательство не отменяют тесты, а наоборот - им способствуют.

Цитата:
Кстати, пользуясь случаем, предложу. У вас есть желание рассказать что-нибудь на тему тестирования, формальной верификации и т.п.
на конференции Гейзенбаг (Москва, 6-7 декабря) для рядовых тестировщиков/разработчиков? Конференция по вопросам тестирования, и доклад на подобную тему наверняка был бы интересен.
Понимаю, что подготовка доклада это время, но вдруг интересно?
Доклад я уже делал для нужд компании, в которой работаю. Материалы для внешней конференции, наверно, нужно делать заново, но проблема не в этом. Я живу в Киеве и не люблю путешествовать. Планировать за год тоже не в моих привычках. Но спасибо за предложение.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 10 Март, 2018 13:41 

Зарегистрирован: Вторник, 27 Февраль, 2018 09:18
Сообщения: 53
Comdiv писал(а):
Внимательно следите за руками. Сначала Вы утверждаете, что согласно теореме Прайса, доказывать код невозможно. Когда я указываю, что из теоремы Прайса нет такого следствия, Вы просите объяснить подробней. Сначала я показываю на простейшем примере, что код, всё-таки, в каких-то случаях можно доказывать и даю ссылки на гораздо более серьёзные учебные примеры. Затем даю ссылку на промышленное применение, так как понимаю, что это следующий этап разговора, благо раньше у людей уже возникали такие запросы. После этого Вы меняете показания и, снабжая свою речь утончённым сарказмом, начинаете писать, что, мол, доказательство корректности не умеет превращать воду в вино, не исцеляет прокажённых от болезни и, вообще, "Круто. Чего ж. Ну, да, конечно", так, как будто утверждалось обратное. Я ответил на конкретный вопрос, а не на некие домыслы, которые в итоге посыпались.

Да, был неправ. Спасибо.
Да, теорема Райса не запрещает программе работать согласно её собственной спецификации.
Проблемы возникают тогда, когда спецификация (алгоритм) находится отдельно от программы.

Тут, конечно, можно много обсуждать "до какого уровня доказательств" нужно спускаться.
Иначе говоря, при программировании на языке со статической типизацией, можно считать, что "программируем под доказательство" (где спецификациями являются типы возвращаемых значений).

Получается, программа на статически-типизированном языке уже считается "программой под доказательство".
Конечно, возникнет голос из зала: "Простите, но нам программа нужна не про то, что <<результат будет иметь тип int>>, а про то, <<деньги со счёта не пропадут бесследно>>". И последует (доглая) беседа на тему того, является ли подобный код следствием бизнес-требований заказчика (==действительно ли заказчик разговаривает на таком языке и ставит требования таким образом. Ведь, если он ставит требования другим образом, то нужно ещё как-то доказывать переход, иначе от того, что программа работает по "нашей" спецификации заказчику не легче)
Код:
value_type* a, size_type n
{
  /*@
    loop invariant bound:   0 <= i <= n;
    loop invariant sorted:  Sorted(a, i);
    loop invariant sorted:  0 < i  ==> LowerBound(a, i, n, a[i-1]);
    loop invariant reorder: MultisetUnchanged{Pre,Here}(a, n);
    loop assigns   i, a[0..n-1];
    loop variant   n - i;
  */
  for (size_type i = 0; i < n; ++i) {
    const size_type sel = i + min_element(a + i, n - i);
    //@ assert reorder: i <= sel < n;
    /*@
       assigns a[sel], a[i];
       ensures reorder: a[i]   == \old(a[sel]);
       ensures reorder: a[sel] == \old(a[i]);
       ensures reorder: Unchanged{Old,Here}(a, 0,     i);
       ensures reorder: Unchanged{Old,Here}(a, i+1,   sel);
       ensures reorder: Unchanged{Old,Here}(a, sel+1, n);
    */
    swap(a + sel, a + i);
    //@ assert reorder: MultisetUnchanged{Pre,Here}(a, n);
  }


Comdiv писал(а):
Владимир Ситников писал(а):
FDIV всегда работало верно. Иными словами, если возникает глюк железа
Каким боком это относится к доказательству программ, или любым другим методам отладки?

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

Comdiv писал(а):
Владимир Ситников писал(а):
В той же теме я услышал "пошаговая отладка это разврат мозга на уровне импринтинга". Так там было? Ну, пусть так и будет.
У этого обсуждения есть конкретный контекст - школьная версия, образовательная система, базовые знания.
У Вас другое мнение? Я считаю это нормальным.

Разумеется, зависит от объёма курса, но у меня мнение другое. На мой взгляд, даже просто возможность пошагового выполнения это наглядный способ показать, что внутри магии нет.
Большая (146%) часть сарказма относилась именно к пункту "пошаговый отладчик".

Comdiv писал(а):
Цитата:
Я вижу, что вы пишете интересные штуки, но у меня совершенно нет желания, чтобы вы меня убеждали в том, что "пошаговая отладка мне не нужна".
Ещё раз, я ответил на конкретный вопрос. Я сам указывал, что пошаговая отладка может быть полезна. Вам не понравилось, что речь шла об обфусцированном коде?

Тут, скорее, в части "пошаговой отладки" я перепутал адресата.

Comdiv писал(а):
Владимир Ситников писал(а):
Ну, подаём в программу массив, а она один из элементов "не туда" сортирует. Ответ "работает согласно спецификации",

Как Вы себе представляете такую спецификацию?

Например, забыли условие на "устойчивость" сортировки (вместо stable получили простую).
Мало ли ещё ошибок в спецификации может быть? Я говорю не про логические, а про алгоритмические ошибки.

Comdiv писал(а):
Цитата:
3) Что, если будет ошибка в компиляторе? Ну, подаём данные на вход, а выход неверный. Спецификация на месте. Как искать ошибку?
А, Вы, наверно, думаете, что наличие доказательства отменяет тесты?

Я намекал на то, что есть случаи, когда пошаговая отладка полезна в том числе и при использовании спецификаций.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Суббота, 10 Март, 2018 16:57 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 693
Откуда: Киев
Владимир Ситников писал(а):
Тут, конечно, можно много обсуждать "до какого уровня доказательств" нужно спускаться.
Иначе говоря, при программировании на языке со статической типизацией, можно считать, что "программируем под доказательство" (где спецификациями являются типы возвращаемых значений).

Получается, программа на статически-типизированном языке уже считается "программой под доказательство".
Кем считается? Доказательства бывают полными и неполными. Неполные доказательства люди любят из-за того, что их, зачастую, проще достичь. В частности, статическая типизация позволяет соблюсти ряд важных свойств на уровне, близком к автоматическому, чем и ценна в деле достижения корректности. Полное доказательство подразумевает доказательство всех заявленных свойств, а не только той же статической типизации. Это, как правило, очень трудоёмко, тем не менее, это не означает, что нужно ограничиваться статической типизацией или чем-то ещё подобным. То, что некие необъявленные свойства не могут будут доказаны, то это очевидно. Мы говорим не о чудесах с кнопками "сделай мне хорошо", а о науке в рамках физических законов. В контексте нашего разговора также остаётся неясным, каким образом необъявленные свойства должны обнаруживаться в пошаговой отладке. Программист с пошаговым отладчиком становится телепатом?

Цитата:
Конечно, возникнет голос из зала: "Простите, но нам программа нужна не про то, что <<результат будет иметь тип int>>, а про то, <<деньги со счёта не пропадут бесследно>>". И последует (доглая) беседа на тему того, является ли подобный код следствием бизнес-требований заказчика (==действительно ли заказчик разговаривает на таком языке и ставит требования таким образом. Ведь, если он ставит требования другим образом, то нужно ещё как-то доказывать переход, иначе от того, что программа работает по "нашей" спецификации заказчику не легче)
Заказчик не обязан писать формальные спецификации, как и не обязан писать тесты или заниматься пошаговой отладкой. Программирование под доказательство и формальные спецификации нужны в первую очередь инженерам.

Цитата:
Comdiv писал(а):
Владимир Ситников писал(а):
FDIV всегда работало верно. Иными словами, если возникает глюк железа
Каким боком это относится к доказательству программ, или любым другим методам отладки?
Это самым прямым образом относится к пользе пошагового отладчика для изучения ошибок железа, компилятора и т.п.
Вот тут - точно нет. Если у Вас есть полноценные спецификации, то ошибку Вы обнаружите не неведомо где, а максимально близко к месту возникновения. Вам не надо никуда шагать.

Цитата:
На мой взгляд, даже просто возможность пошагового выполнения это наглядный способ показать, что внутри магии нет.
Нас учили теории алгоритмов, которая под силу школьнику. Она и была способом показать, что внутри магии нет. В качестве разминки-шутки учитель использовал учеников для иллюстрации выполнения алгоритма. Такая наглядность была необязательной, но против неё я ничего не имею. Также, на мой взгляд, выполнение алгоритмов самостоятельно на бумажке даёт гораздо больше понимания, как оно работает без магии, чем созерцание магических мультиков.

Цитата:
Comdiv писал(а):
Как Вы себе представляете такую спецификацию?
Например, забыли условие на "устойчивость" сортировки (вместо stable получили простую).
Мало ли ещё ошибок в спецификации может быть? Я говорю не про логические, а про алгоритмические ошибки.
То есть, Вы имеете ввиду ситуацию, когда в голове у Вас есть спецификация, а в тексте программы её нет? Иначе ведь не поймёшь, что "неустойчивая" сортировка неверна. Так в том и состоит задача программирования под доказательство, чтобы вместо интерпретации программы как процессор, интерпретировать её как система доказательства. И тогда Ваша внутренняя спецификация будет отображаться не на пошаговое исполнение, а на символьное.

Цитата:
Comdiv писал(а):
А, Вы, наверно, думаете, что наличие доказательства отменяет тесты?
Я намекал на то, что есть случаи, когда пошаговая отладка полезна в том числе и при использовании спецификаций.
Я уже писал, что наличие формальных спецификаций, позволяет находить ошибку максимально близко месту возникновения, никуда шагать не нужно. Как это делается? Посмотрите на упомянутый Frama-C, у него есть pluging E-ACSL, который позволяет формальные проверки превратить в фактические во время исполнения. Если компилятор и чудит что-то, то это самый эффективный способ получить информацию по существу, где именно, а никак не пошаговая отладка.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 14 Март, 2018 14:28 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 8989
Откуда: Россия, Орёл
Владимир Ситников писал(а):
И, кстати, когда я учил брата программированию, у него наблюдалась обратная ситуация: он мог подолгу "тупить в код", хотя достаточно было выполнить пошаговую отладку и понять почему ожидаемое поведение не соответствует желаемому.


Вот это и хорошо, что "тупить в код".
Иначе получается риск каждый раз решения частного случая выполнения, ликвидации частной ошибки.
Цикл завис - погоняли, поставили дополнительный if-break. И т.п.
Нужно формировать постепенными упражнениями видение именно всего класса вычислений.
Что возможно только пристальным вниманием к самому алгоритму как формальной конструкции, а не к конкретному экземпляру его исполнения.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Среда, 14 Март, 2018 14:32 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 8989
Откуда: Россия, Орёл
Comdiv, коллега, большое спасибо за содержательную ветку.

Надо внимательно посмотреть на это микроядро и методы.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Четверг, 15 Март, 2018 00:25 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 693
Откуда: Киев
seL4 примечательно тем, что это используемая в промышленности система с доказанной корректностью, но путь, который они выбрали достаточно экстравагантен, что обусловлено возрастом проекта. Сейчас, на мой взгляд, более привлекательны решения предоставляемые Frama-C +CompCert либо SPARK Ada.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 26 ]  На страницу Пред.  1, 2

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2018, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB