Не для Cybera, а истины для и остальных, кто сюда заглянет.
T>>Нет. Обычный (нетаймированный) автомат неспособен адекватно описать систему реального времени.
C>Вообще-то, конечный автомат не может представить много чего. Поэтому я и пишу "state-машина" (aka "автомат").
У меня слова "конечный" не было. Впрочем, бесконечный нетаймированный автомат тоже представить адекватно систему реального времени не может, конечно.
T>>У нас и программисты хорошие. О школе академика Ершова что-нибудь слышали, например?
C>То было давно...
Было, есть в настоящее время, и будет.
http://ru.wikipedia.org/wiki/%D0%9A%D0%B0%D1%81%D1%8C%D1%8F%D0%BD%D0%BE%D0%B2,_%D0%92%D0%B8%D0%BA%D1%82%D0%BE%D1%80_%D0%9D%D0%B8%D0%BA%D0%BE%D0%BB%D0%B0%D0%B5%D0%B2%D0%B8%D1%87
C>Не чушь. Товарищи из буржуйских стран сейчас занимаются интересными вещами, у нас же практически ничего не происходит.
Если кое-кому о чем-то неизвестно, вынужден повториться, это не значит, что это отсутствует в природе.
http://www.iis.nsk.su/preprints/abstracts_ru.shtml
http://www.iis.nsk.su/projects/index.shtml
http://www.iis.nsk.su/preprints/books/index_ru.shtml
http://www.spiiras.nw.ru/modules.php?name=Content&pa=showpage&pid=16
http://www.ccas.ru/
http://space.iias.spb.su/
http://www.keldysh.ru/projects/projects-fr.html
http://library.keldysh.ru/prep_ls.asp
C>Смотрим: http://arxiv.org/list/cs/pastweek?skip=0&show=25 — сюда сейчас попадают практически все нормальные статьи по информатике.
Вот прямо все.
C>А вся "Russian Academy of Science" ( http://search.arxiv.org:8081/?query=Russian+Academy+of+Science&in=grp_cs ) проигрывает одному MIT: http://search.arxiv.org:8081/?query=MIT&in=grp_cs со счётом 110 против 3552 (точнее, немного меньше из-за случайных совпадений со словом MIT)!
Конечно, следует приветстовать, если человек интересуется, что происходит в его проблемной области в мире. В то же время низкопоклонство перед Западом приветствовать вряд ли стоит.
C>Ещё можно сравнить знаменитый курс MIT'а по программированию и наши курсы в университетах.
Можно сравнить. Не так плохи курсы во многих наших университетах, и не только в Москве и Санкт-Петербурге.
T>>при создании вами же упомянутой системы управления парижским метро 14 ветки используется
T>>так называемая "B-технология", именно позволяющая генерировать гарантированно соответствующие спецификации программы. И они в этом не одиноки 
C>Проблема тогда в том, что спека будет аналогом алгоритма. Там всё сложнее — их система позволяет проверять соблюдение инвариантов при создании кода.
C>>>>>Если у нас есть спецификация алгоритма, достаточно подробная, чтобы доказать её корректность, то это УЖЕ будет почти что готовая его реализация.
T>>Точно, именно так ПО для парижского метро и делали.
C>Его делали немного по-другому, однако. Сначала сформировали спеку с набором инвариантов и гарантий, а потом следили за их соблюдением.
Все именно так, как я написал. Да, "спецификация" на B-языке по объему приблизительно соответствует записи программы на "обычном" языке программирования. Да, при этом она снабжается описанием инвариантов.
C>Что далеко ходить — система SAP R3 содержит около 250 миллионов строк кода. Т.е. гигабайты исходного кода.
C>бухгалтерия — это часто как раз те же десятки взаимодействующих друг с другом процессов
Он не взаимодействуют в реальном времени, конечно же. И "бухгалтерские" программы по сути своей безнадежно последовательны. Вычислительной сложности в них тоже нет. Сложность там возникает в связи с объемами, это да.
Но говорить, что бухгалтерские программы сложнее программ управления космическими аппаратами некорректно.
