Хотелось бы знать, как народ отнесся бы к появлению проекта по созданию Руccкой
ОС. Причём не только русской, но и всего русскоговорящего населения?
Присоеденились бы вы к такому проекту?
>>>Вспоминается TUNES. Тоже было в начале много букв. За 13 лет единственный
>>>результат - занятный сайт.
Когда-то один профессор, с которым мне довелось работать на одной кафедре, говорил мне, "зеленому" ассистенту: Работать надо, юноша. Будете работать - будет результат. А если будете сидеть и думать о результате, то его не будет. С возрастом все больше убеждаюсь, что он был прав по сути. Чтобы что-то получилось, надо работать, другого способа нет. Если у авторов проекта получится наладить совместную работу, то результат обязательно появится. Как у Линуса, который сумел перейти от мечтаний о хорошей и надежной ОС к созданию реального кода. Хотя ему тоже наверняка говорили что-то типа: "Ты совсем спятил, в 90-х годах новую ось делать. Поезд уже ушел". А насчет опасений Вы, конечно, правы. Любой проект можно "заболтать", у каждого есть свои проблемы, семью надо кормить, а для кормежки и Windows хороша :))). Я вот тоже для внешнего мира работаю с MSWindows и MSOffice. А "для души", когда никто не видит :))), работаю со своими учениками с блэкбоксами. На зарплате это не сказывается :(((, но зато есть чувство, что поддерживаю свою "форму", как специалиста, не "зашориваю" свое профессиональное образование только виндой и вижуал-бейсиком.
Некоторые мои размышления на тему формальных моделей (часть взята из публикации 2001 г.).
В начале 1970-х годов Дуглас Росс (Douglas Ross), участник знаменитого проекта Whirlwind (MIT), автор термина CAD (Computer-Aided Design, САПР), основатель компании SofTech (первые компиляторы Паскаля), автор известной методологии IDEF0, утверждал, что «80 или даже 90% информатики будет в будущем основываться на теории конечных автоматов». И хотя этого пока не наблюдается, все же можно сказать, что конечные автоматы с 60-х годов играют заметную роль в развитии компьютерных технологий.
Помимо теории формальных языков и основанных на ней методов построения компиляторов конечные автоматы активно используются в компьютерных играх, в реализации сетевых протоколов, системах сжатия информации, криптосистемах, в системах реального времени и встроенных системах. Иными словами, там, где требуется большая надежность и где логика поведения чересчур сложна, чтобы программист смог реализовать ее на одном лишь уровне здравого смысла.
С появлением структурного программирования стало очевидно, что из трех главных конструкторов управления: следования, цикла и ветвления последний является самым трудным в восприятии программиста, поскольку при множестве альтернатив превращает линеаризированную структуру алгоритма в древовидную. При этом сложность даже последовательных программ (не говоря уже о параллельных) растет стремительно и временами может превосходить дерево вариантов в столь непростой для автоматического анализа модели, как традиционные шахматы.
Разбиение программы на процессы и объекты с заменой многоступенчатого ветвления средствами обработки сообщений (событий) заменяет одну проблему на другую: вложенность уменьшается, зато количество взаимодействующих компонентов заметно возрастает. Логика «размывается» и в итоге мы получаем плохо контролируемую ситуацию, когда из-за хаотичности «ручного» синтеза и невозможности построить исчерпывающий набор тестов нет никакой уверенности в корректности построенной системы. Ключ к решению состоит в применении формальных методов, в создании удобной абстракции, способной «выжать» из алгоритма квинтэссенцию логики его работы и дать возможность проводить весь необходимый анализ.
Одной из таких удобных абстракций могут служить конечные автоматы, среди разновидностей которых стоит выделить трансдюсеры (transducer), автоматы Мили и Мура. Близость к булевой алгебре и теории графов, наглядность графического представления и детерминированность поведения являются заметными достоинствами этой абстракции. Однако при этом надо четко себе представлять, в чем их недостатки, а для этого придется обратиться к истокам программирования, к идеям «механического» вычисления. Как известно, они воплотились в таких формальных моделях, как машины Тьюринга (1936), комбинаторные процессы Поста (1936), нормальные алгорифмы Маркова (1951).
Пытаясь найти точное определение понятия эффективной вычислимости, английский математик Алан Тьюринг выделил особый класс абстрактных машин, о которых высказал предположение, что они пригодны для осуществления любой «механической» вычислительной процедуры. Несмотря на всю громоздкость описания с их помощью алгоритмов они замечательны тем, что согласуются со знаменитым тезисом Чёрча — всякая механическая процедура, манипулирующая с символами, может быть выполнена той или иной машиной Тьюринга. Иными словами, эта абстрактная машина способна реализовать любой алгоритм. В таком контексте конечный автомат эквивалентен ограниченной машине Тьюринга, у которой есть только считывающая головка, способная перемещаться лишь в одну сторону — слева направо. Достаточно ли этих возможностей, ведь далеко не все алгоритмы могут быть представлены конечными автоматами?
Чтобы ответить на этот вопрос и определить место конечных автоматов среди других абстракций, рассмотрим сети Петри, занимающие промежуточное положение между машинами Тьюринга и конечными автоматами. Сети Петри работают в терминах условий и событий, где первым сопоставлены позиции (особые узлы — емкости для хранения фишек связаны ориентированными дугами с переходами), а последним — переходы (особые узлы-действия, перемещающие фишки и связанные ориентированными дугами с позициями). Конечные автоматы являются частным случаем сетей Петри и эквивалентны автоматным сетям Петри — сетям, в которых каждый переход может иметь точно одну входную и одну выходную позицию.
Сети Петри лучше всего подходят для описания любых асинхронных систем (асинхронное программирование), тогда как конечные автоматы — преимущественно для сугубо последовательных систем (автоматное программирование). Наглядность динамики и композиционные возможности сетей Петри выше, чем у конечных автоматов, но при этом компактность представления предпочтительнее у последних. Что касается отношения к машине Тьюринга, то достаточно расширить сеть Петри сдерживающими дугами (позволяющими определять отсутствие фишек в данной позиции), как она тут же становится эквивалентной машине Тьюринга. Очевидно, что чем «мощнее» абстракция, чем больше она позволяет синтезировать возможностей, тем хуже у нее дело обстоит с анализом. Иными словами, конечные автоматы анализировать гораздо проще, чем классические сети Петри и уж тем более чем машины Тьюринга.
В работе «Научные основы доказательного программирования» А.П. Ершов выделял три вида программирования: синтезирующее (автоматическое, автоматизированное или ручное манипулирование знанием о задаче с синтезом соответствующей программы), сборочное (построение программы из уже существующих и корректных фрагментов) и конкретизирующее (построение специализированных программ из универсальных заготовок, доопределение кода).
Автоматное и асинхронное программирование в значительной степени раскрываются через синтезирующее программирование, хотя затрагивают также сборочное и конкретизирующее. В области конкретизирующего (и частично сборочного) будут использоваться нейронные стети.
Возрождение интереса к конечным автоматам связано с ростом сложности программных систем. Не последнюю роль в активизации работ в данной области играет то обстоятельство, что язык и методология UML, ставшие стандартом де-факто в области проектирования программного обеспечения, предусматривают при описании поведенческих свойств создаваемой системы использование конечных автоматов и сетей Петри. Но самой этой сфере уделяется крайне мало. Тем более -- эффективному взаимодействию разных формальных моделей.
В принципе мы вторгаемся в весьма интересную область, находящуюся сейчас на пике исследовательского интереса. Думаю, многим известен Grand Challenge (грандиозный вызов информатике), который озвучил друг и соратник Вирта проф. Тони Хоар (ныне ведущий специалист в Microsoft Research). Речь идет о верифицирующем компиляторе. Детальнее введение в задачу можно посм. здесь :
http://www.osp.ru/os/2003/09/183409/
Применение формальных моделей не апостериори, а априори, до "человеческого кодирования", существенно упрощает задачу верификации и позволяет получить куда более лучшее качество. Но это требует иного подхода к программированию, переноса наукоемкости на уровень мышления аналитика, а не путем встраивания в инструментарий, который призван вычищать чьи-то ошибки.
Что касается общего введения в область формальных методов, рекомендую хорошую статью признанных авторитетов в этой области -- англичан Джонатана Боуэна (соратника Хоара) и Майкла Хинчи. В 1997 г. я активно переписывался с Боуэном (Oxford University Computing Lab), и одним из публичных результатов стала публикация его просветительской работы в журнале "Мир ПК". Она называется "Десять заповедей формальных методов". Часть 1:
http://www.osp.ru/pcworld/1997/09/157957/
Часть 2:
http://www.osp.ru/pcworld/1997/10/158102/
