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

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #165 : Август 21, 2012, 01:26:40 pm »
Поэтому неплохо бы показать каким образом это может работать. На реальном примере.

Так не проблема же -- бери в руки книшку "Дисциплина программирования" -- и вперёд! )))
Лучше так:  "бери в руки книшку "Дисциплина программирования" , засунь под подушку и спать(шоб расстояние между гениальными идеями, содержащимися в ней ,и мозгом было минимальным),  а с утра в перед!  :D

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #166 : Август 21, 2012, 01:31:51 pm »
...а если не прокатило то "вы попытаетесь использовать их для распутывания хаоса, созданного группой некомпетентных, неорганизованных программистов" - короче, сам дурак....

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #167 : Август 22, 2012, 02:34:31 am »
Формальная верификация Си кода
http://habrahabr.ru/post/148709/
to iterate is human, to recurse, divine

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

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #168 : Август 22, 2012, 03:12:12 am »

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

"How big is seL4?

8,700 lines of C code plus 600 lines of ARM assembly code.
How much of it is verified?

7,500 lines of C code. We currently do not verify the assembly code and the boot code (1,200 lines).
How big is the proof?

 All together 200,000 lines of Isabelle proof script. Manually written, machine checked. Roughly 3,500 A4 pages if printed out (a stack about half a meter high).

 This is one of the largest formal proofs ever done. For comparison, the famous machine-checked proof of the four colour theorem is about 60,000 lines in the theorem prover. The only other proof that we know of that is larger, is from the Verisoft project (they report about 245,000 proof steps). Of course, in mathematics, the smaller the proof, the better it is considered to be :-)"
« Последнее редактирование: Август 22, 2012, 03:13:45 am от DIzer »

vlad

  • Hero Member
  • *****
  • Сообщений: 1391
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #169 : Август 22, 2012, 03:12:19 am »
Формальная верификация Си кода
http://habrahabr.ru/post/148709/

Мда. Впечатляет. Как иллюстрация того, что оно даже "не дойдет до попыток применения на реальном коде" :)

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #170 : Август 22, 2012, 03:19:15 am »
т.е. коэффициент 1 к 30, не, пожалуй выну я Дейкстру из под подушки.... ;D А если учесть что эти 200000 строк писались ручками и по сути дела являются отдельной программой для прувера.... чур чура.....
« Последнее редактирование: Август 22, 2012, 03:21:16 am от DIzer »

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #171 : Август 22, 2012, 03:52:57 am »
How much work was it?

 In total, design, documentation, implementation and verification of the seL4 kernel come to about 25-30 person years. This includes a lot of new research, new tools, and new libraries. If we were to do it again, we think it would be less than 10 person years.

 As a comparison, an industry rule of thumb for software certification in the Common Criteria process at Evaluation Level 6 (which is not even the highest) is $1,000 per line of code. That means a traditional process would be around $8.7 Million for seL4 and would give less assurance.

How many bugs have you found?

We found 160 bugs in the C code in total. 16 of these were found during testing and internal student projects running the kernel before the C verification had started in earnest. 144 bugs were found during the C verification phase.
to iterate is human, to recurse, divine

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

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #172 : Август 22, 2012, 04:03:49 am »
А с чем? Управление памятью?..
Не понял вопроса.
...
Я имел в виду - с чем связано по-Вашему?.. м.б. как раз с ошибками в требованиях к программе?..

Geniepro

  • Hero Member
  • *****
  • Сообщений: 1955
  • Знайте- истина в том, что повторено трижды подряд!
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #173 : Август 22, 2012, 05:28:31 am »
А с чем? Управление памятью?..
Не понял вопроса.
...
Я имел в виду - с чем связано по-Вашему?.. м.б. как раз с ошибками в требованиях к программе?..
Самая большая проблема в отладке микроконтроллерного софта -- это воспроизведение внешних воздействий, сигналов с датчиков и тд. и тп...
to iterate is human, to recurse, divine

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

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #174 : Август 22, 2012, 09:14:39 am »
А, это то, что решается типа как здесь или здесь говорилось...

Кстати, исходные данные для прувера как раз и можно понимать как "формализацию ТЗ"...

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #175 : Август 22, 2012, 09:41:18 am »
А с чем? Управление памятью?..
Не понял вопроса.
...
Я имел в виду - с чем связано по-Вашему?.. м.б. как раз с ошибками в требованиях к программе?..
А, про это то. С памятью в мк  проблем вообще нет - какие могут быть проблемы когда ты знаешь в лицо каждый из 256 доступных байт? :-)

Основные проблемы, собственно как и везде, со взаимодействием с другими компонентами (не важно железные они или програмные). Общение с другой железкой (скажем сенсором) по I2C например бывает ну очень увлекательным. Не работает и все. Хоть ты пополам разорвись. Потом оказывается что документация лжет (и вообще все лгут) и клок в мегагерц оно не держит, и нужно сильно ниже например. Полно багов в самих кристалах (на уровне железа), впрочем это я описывал уже: http://oberspace.dyndns.org/index.php/topic,261.msg6259.html#msg6259

Ну и сторонние либы (например для реализации bluetooth стека). Там тоже бывает весело. И, замечу, это все и одновременно. В отличае от толстых десктопов и мобильников, в мк корректность работы это не только правильные алгоритмы, но и еще нужно уложиться по времени. Жесткий (настоящий) реалтайм. Ах, да, по энергопотреблению тоже уложиться нужно, ибо если твой мк жрет 4 mA, то он никому не нужен. И то что работает как часы без энергосбережения начинает глючть в одном из энергосберегающих режимов (на уровне железа с не софта).

Собственно от логики в мк (которую можно верифицировать) ну очень мало. В этом плане программы там очень простые - не запутаешься. Поэтому там вполне применим Дракон :-)
"но сейчас, чтобы компенсировать растущую мощность компьютеров, программисты используют фреймворки"

DIzer

  • Гость
Re: ещё про цикл дейкстры
« Ответ #176 : Август 22, 2012, 12:41:51 pm »
How much work was it?
.....
Geniepro - я пошутил, не принимайте так близко...,  лет через пятьдесят возможно будет использоваться автоматизированная верификация программ  - пока это мало кто себе может позволить, но развиваться в этом направлении стоит.. вот кто из живущих 60 лет назад мог бы по думать о сегодняшнем развитии вычь техники - я лишь смеюсь над кучкой людей сотворивших фетиш и толпой поклоняющихся ему.

Влад Жаринов

  • Full Member
  • ***
  • Сообщений: 189
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #177 : Август 23, 2012, 04:37:56 am »
Ну, формальная верификация проверкой моделей уже применяется всё шире...
Вот с формальной верификацией доказательством всё сложнее... не совсем ясно, что именно она даёт. Скорее в этом случае оправданно "сразу правильно строить программы"... по не сразу правильному формальному ТЗ... ;) т.е. нужна будет методика итеративного проектирования...

...
Собственно от логики в мк (которую можно верифицировать) ну очень мало. В этом плане программы там очень простые - не запутаешься. Поэтому там вполне применим Дракон :-)
А, так значит моё мнение, что техноязык немного продвинулся в практику (даже в такой с-ложной среде, как Ты-реализация) не случайно в первую очередь именно на этом направлении, было не случайным... ;) именно простота проектов и неудобство копания в асм-кодах в текстовой записи по сравнению с графикой икон и силуэтными джампами...

valexey

  • Administrator
  • Hero Member
  • *****
  • Сообщений: 1990
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #178 : Август 23, 2012, 09:43:47 am »
...
Собственно от логики в мк (которую можно верифицировать) ну очень мало. В этом плане программы там очень простые - не запутаешься. Поэтому там вполне применим Дракон :-)
А, так значит моё мнение, что техноязык немного продвинулся в практику (даже в такой с-ложной среде, как Ты-реализация) не случайно в первую очередь именно на этом направлении, было не случайным... ;) именно простота проектов и неудобство копания в асм-кодах в текстовой записи по сравнению с графикой икон и силуэтными джампами...

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

На асме под мк пишут относительно редко. Обычно сейчас все же пишут на Си. Кроме того, соблюдать согласованность придуманной схемы на Драконе с рукописным кодом на асме будет тяжко. Так что основных причин две:
1) простота алгоритмов + малый размер кодовой базы (поэтому Дракон в принципе применим)
2) широкое применение графических схем в не програмных частях проекта (схемотехника) => банальная привычка к ним + будет экономия времени из за отсутствия необходимости переключения мозга с графического на текстовый "режим" восприятия и обработки.

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

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

Kemet

  • Hero Member
  • *****
  • Сообщений: 587
    • Просмотр профиля
Re: ещё про цикл дейкстры
« Ответ #179 : Август 23, 2012, 10:16:55 am »
Скорее потенциальная популярность Дракона у микроконтроллерщиков связана с их привычкой к графическим двумерным схемам
Под микроконтроллеры не пишут тонны кода, поэтому вполне реально и кому-то даже удобно, рисовать блок-схемы. Как только размер программы начинает увеличиваться, и рисовать становится абсолютно непродуктивно, блок-схемы уходят даже не на второй, а на третий план, ибо писать программы и рисовать блок-схемы несколько разные вещи.

valexey: поправил оформление цитаты
« Последнее редактирование: Август 23, 2012, 10:47:07 am от valexey »