Автор Тема: ещё про цикл дейкстры  (Прочитано 28146 раз)

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #150 : Август 21, 2012, 07:47:06 am »
Ну, "годен для доказательного программирования (сиречь, дедуктивной верификации)" - это по теории получается прежде всего, "удовлетворяет структурной теореме"... :) так что печать вроде как ставит кодер, воздерживающийся от иного... ;)
А вот для верификации проверкой моделей вроде как и goto не помеха... там, правда, надо не забыть представить все существенные техтребования в виде *TL-формул... :)

Я скорее к тому, что вот язык, применимый для программной реализации систем в смысле Усова - он должен такие различия учитывать?.. и вообще это м.б. один из существующих языков (Хаскель или иной)?.. можно что-то с позиции CS-профессионала сказать?..

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 481
    • Просмотр профиля
Re: Ещё про циклы
« Ответ #151 : Август 21, 2012, 07:54:23 am »
Вот тут предложена некая классификация циклов вообще...
...
Дело в том, что на практике есть не два, а 5 видов циклов.
 1. Подлинно бесконечный цикл, с остановкой по исключению.
 2. Цикл опроса (предмет цикла меняется извне; покуда он не изменился, мы молотим почти бесконечный цикл).
 3. Цикл неограниченных итераций, с остановкой по условию (предмет цикла меняется в его теле, но последовательность значений нетривиальна, а то и непредсказуема — например, проблема 3X+1)
 4. Цикл линейного пробега по всему диапазону.
 5. Цикл линейного поиска.

 К сожалению, в Си есть только три языковые конструкции: for, while/do-while и проклятая if-goto
 Вот и приходится выделываться с while(true), for(;;) и break/continue.
...
Типа от жизни обосновывается.
Как я понимаю, в доказательном подходе предлагается выводить первые три обычно через 4 и/или 5. Для того же и ЦД. Или я чего-то не понимаю?.. :)
Замечу, что 5 не является подмножеством 4. Кроме того, в Обероне пункт 4 отсутствует.
Классификация достойна пера великого художника http://oberspace.dyndns.org/index.php/topic,172.msg2841.html#msg2841

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #152 : Август 21, 2012, 08:05:25 am »
Мысль (вроде от Питера Брейгеля?) понятна... :)
Кстати, автор поста вроде как не любитель ДРАКОНа... :D

А как Вы бы подразделили?.. для языка?..

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #153 : Август 21, 2012, 08:06:19 am »
Ну, "годен для доказательного программирования (сиречь, дедуктивной верификации)" - это по теории получается прежде всего, "удовлетворяет структурной теореме"... :) так что печать вроде как ставит кодер, воздерживающийся от иного... ;)
Это теорема которая:
Цитировать
Любую схему алгоритма можно представить в виде композиции вложенных блоков begin и end, условных операторов if, then, else, циклов с предусловием (while) и может быть дополнительных логических переменных (флагов).
?

Замечу, что тут if/then/else лишние (избыточные). Хватило бы блоков с while.

Почитал про это самое доказательное программирование (вот тут: http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf), собственно ясно что оно не пригодно для применения в обычном производстве софта, ибо слишком трудоемко и плохо масштабируется. Годится для простых систем (той же встроенки), там это себе можно позволить. С другой стороны уж там то баги часто с логикой программы (которую можно верифицировать) ну никак не связаны.
"но сейчас, чтобы компенсировать растущую мощность компьютеров, программисты используют фреймворки"

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #154 : Август 21, 2012, 08:18:50 am »
А с чем? Управление памятью?..

Кстати, возможно, поэтому проверка моделей больше востребована - тот же Спин сделала Белл для себя... потом и МС стала применять аналогичную систему для верификации драйверов и их взаимодействия с другими частями ОС... как поддержка чего вроде появилась "модель драйверов"...

Насчёт избыточности ветвления - это первыми заметили сами авторы теоремы... вот тут всплыло: http://forum.oberoncore.ru/viewtopic.php?p=73992#p73992 ... ;) Я так понимаю, что путаница с тем, что при доказательстве используются и обе структуры циклов, и ветвление...

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #155 : Август 21, 2012, 08:25:44 am »
А с чем? Управление памятью?..
Не понял вопроса.

Насчёт избыточности ветвления - это первыми заметили сами авторы теоремы... вот тут всплыло: http://forum.oberoncore.ru/viewtopic.php?p=73992#p73992 ... ;) Я так понимаю, что путаница с тем, что при доказательстве используются и обе структуры циклов, и ветвление...
Ну, собственно это написано в любой книжке где описывается структурное программирование. Я это тоже где-то вычитал.
"но сейчас, чтобы компенсировать растущую мощность компьютеров, программисты используют фреймворки"

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #156 : Август 21, 2012, 08:35:44 am »
Да, вспомнил - для встроенки ведь актуально проверять системы процессов. При дедукции для этого м.б. использованы модифицированные исчисления программ - вроде
этого
. Можно и описать логику поведения и величины состоояния - а дальше автоматизированный анализ/синтез софта для целевой платформы.

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 481
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #157 : Август 21, 2012, 10:22:53 am »
Почитал про это самое доказательное программирование (вот тут: http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf), собственно ясно что оно не пригодно для применения в обычном производстве софта, ибо слишком трудоемко и плохо масштабируется. Годится для простых систем (той же встроенки), там это себе можно позволить. С другой стороны уж там то баги часто с логикой программы (которую можно верифицировать) ну никак не связаны.
Тоже пролистал по диагонали.
Нежизнеспособно.
Даже нельзя сказать, что оно отомрет при реальной работе.
Оно до нее просто не доживет.

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1953
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #158 : Август 21, 2012, 11:01:23 am »
Почитал про это самое доказательное программирование (вот тут: http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf), собственно ясно что оно не пригодно для применения в обычном производстве софта, ибо слишком трудоемко и плохо масштабируется. Годится для простых систем (той же встроенки), там это себе можно позволить. С другой стороны уж там то баги часто с логикой программы (которую можно верифицировать) ну никак не связаны.
Почитай, что Дейкстра об этом писал:
Цитата: Edsger W. Dijkstra
•Кое-кто из вас сомневается, что упомянутые ранее "приемы эффективного доказательства", столь изящные для маленьких программ, способны масштабироваться, я цитирую, "применимо к устрашающим размерам и явной сложности большинства программ". Что ж, они окажутся бессильны, если вы попытаетесь использовать их для распутывания хаоса, созданного группой некомпетентных, неорганизованных программистов. Их сила проявляется в фазе конструирования, когда (i) они приводят к значительно более коротким исходным текстам, чем созданные без их помощи, и (ii) длина вывода программы растет не быстрее, чем линейно, с ростом самой программы. Наконец, программы, произведенные таким способом, получаются бесконечно лучшими, чем обычный программный хлам.
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

Peter Almazov

  • Sr. Member
  • ****
  • Сообщений: 481
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #159 : Август 21, 2012, 11:20:39 am »
Почитал про это самое доказательное программирование (вот тут: http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf), собственно ясно что оно не пригодно для применения в обычном производстве софта, ибо слишком трудоемко и плохо масштабируется. Годится для простых систем (той же встроенки), там это себе можно позволить. С другой стороны уж там то баги часто с логикой программы (которую можно верифицировать) ну никак не связаны.
Почитай, что Дейкстра об этом писал:
Как минимум, он не мог писать об этом http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf
:)

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #160 : Август 21, 2012, 12:08:31 pm »
Почитал про это самое доказательное программирование (вот тут: http://aivt.ftk.spbstu.ru/media/files/2012/course/quality/deductive_verification.pdf), собственно ясно что оно не пригодно для применения в обычном производстве софта, ибо слишком трудоемко и плохо масштабируется. Годится для простых систем (той же встроенки), там это себе можно позволить. С другой стороны уж там то баги часто с логикой программы (которую можно верифицировать) ну никак не связаны.
Почитай, что Дейкстра об этом писал:
Цитата: Edsger W. Dijkstra
•Кое-кто из вас сомневается, что упомянутые ранее "приемы эффективного доказательства", столь изящные для маленьких программ, способны масштабироваться, я цитирую, "применимо к устрашающим размерам и явной сложности большинства программ". Что ж, они окажутся бессильны, если вы попытаетесь использовать их для распутывания хаоса, созданного группой некомпетентных, неорганизованных программистов. Их сила проявляется в фазе конструирования, когда (i) они приводят к значительно более коротким исходным текстам, чем созданные без их помощи, и (ii) длина вывода программы растет не быстрее, чем линейно, с ростом самой программы. Наконец, программы, произведенные таким способом, получаются бесконечно лучшими, чем обычный программный хлам.

Нужно четко понимать контекст слов Дейкстры, какое тогда было время и какие техники программирования. Тогда была распространено писать на asm'e и в высокоуровневых языках плодить лапшу из goto. Естественно те програмки которые тогда писались (а они относительно сегодняшнего дня маленькие или средние) быстро становились не поддерживаемыми.

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

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1953
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #161 : Август 21, 2012, 12:28:15 pm »
Нужно четко понимать контекст слов Дейкстры, какое тогда было время и какие техники программирования. Тогда была распространено писать на asm'e и в высокоуровневых языках плодить лапшу из goto. Естественно те програмки которые тогда писались (а они относительно сегодняшнего дня маленькие или средние) быстро становились не поддерживаемыми.

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

Это была выдержка из EWD1305 от 2000 г. -- не так уж и давно это было...
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #162 : Август 21, 2012, 12:43:55 pm »
Нужно четко понимать контекст слов Дейкстры, какое тогда было время и какие техники программирования. Тогда была распространено писать на asm'e и в высокоуровневых языках плодить лапшу из goto. Естественно те програмки которые тогда писались (а они относительно сегодняшнего дня маленькие или средние) быстро становились не поддерживаемыми.

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

Это была выдержка из EWD1305 от 2000 г. -- не так уж и давно это было...

ok. Но это всего лишь заявление и не факт что оно было сделано с учетом современных реалий а не его богатого опыта 70-х и 80-х. Поэтому неплохо бы показать каким образом это может работать. На реальном примере.
"но сейчас, чтобы компенсировать растущую мощность компьютеров, программисты используют фреймворки"

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #163 : Август 21, 2012, 01:13:50 pm »

Применительно же к сегодняшнему дню я не видел ни одного примера когда доказательное написание приводило бы к уменьшению числа строк кода/объема кода.
:D тут вы забыли еще о длине  самого доказательства  ;D которая не меньше чем длина "оптимизированного" кода, весьма крутые требования к команде кодеров
( а где таких на практике взять? = разве что в коровнике  :D ). Во общем, время рассудит - или уже рассудило?  ;)

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1953
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #164 : Август 21, 2012, 01:19:32 pm »
Поэтому неплохо бы показать каким образом это может работать. На реальном примере.

Так не проблема же -- бери в руки книшку "Дисциплина программирования" -- и вперёд! )))
to iterate is human, to recurse, divine

Салат «рекурсия»: помидоры, огурцы, салат…