«Наука в Сибири»
№ 25 (2710)
25 июня 2009 г.
ШИРОКИЙ ВЗГЛЯД
НА ПОНИМАНИЕ ПРОГРАММ
Международная конференция «Перспективы систем информатики» («PSI’09»), посвященная памяти выдающегося отечественного ученого, математика и программиста академика Андрея Петровича Ершова (1931-1988), проводится ИСИ СО РАН с 1991 г. в седьмой раз. В этом году она была приурочена
Пресс-служба ИСИ СО РАН.
Конференция «Перспективы систем информатики» — это форум, на котором собираются ученые, разработчики и пользователи программного обеспечения, работающие как в науке, так и в промышленности. Цель конференции — наведение мостов между этими сообществами, интересы которых затрагивают такие области, как разработка и анализ программ и систем, методология и технология программирования, информационные технологии. Форум позволяет обсудить различные методы и подходы и тем самым помочь специалистам в повышении надежности и эффективности методов, алгоритмов и инструментария разработки программных и информационных систем. Проблематика конференции охватывает основания анализа разработки программ и систем, методологию и технологию программирования, информационные технологии. Предыдущие конференции, состоявшиеся в 1991, 1996, 1999, 2001, 2003 и 2006 годах, явились крупными международными событиями и прошли весьма успешно.
 |
| Участники PSI'09. |
Большая работа по подготовке конференции проделана международным Программным комитетом, который возглавляет директор ИСИ СО РАН
Огромную благодарность организаторы конференции приносят всем, кто поддержал проведение: РФФИ, STI Innsbruck (Австрия), Formal Methods Europe, Office of Naval Research (США), HP Labs, Intel, Google, Microsoft Research, Sun Microsystems, ЕМС.
 |
| В. Шюльте (Microsoft Research, США). |
На конференцию этого года были отобраны 32 доклада из 26 стран (Италия, Испания, Германия, Ирландия, США, Франция, Россия, Швейцария и др.). Кроме того, приехали пять приглашенных докладчиков из Великобритании, Дании (2), Швейцарии, США. В рамках конференции состоялись семинары «Наукоемкое программное обеспечение», «Информатика образования» и «История информатики в Сибири».
Особо хочется представить семинар «Понимание программ», который собрал около 30 участников. О предыстории организации семинара «Понимание программ» и его научной проблематике рассказывают один из сопредседателей программного комитета семинара зав. лабораторией смешанных вычислений ИСИ СО РАН
М. А. Бульонков:
 |
| В. Котляров (г. Санкт-Петербург), М. Бульонков (г. Новосибирск). |
— Семинар «Понимание программ» вошел в формат PSI в 2003 г. Идея состояла в том, чтобы организовать мероприятие сродни научному паломничеству, которое дало бы возможность тесного общения единомышленников в неформальной атмосфере. «Понимание программ» — один из любимых терминов Игоря Васильевича Поттосина. Я стал председателем этого семинара, поскольку тематика, предложенная для обсуждения, находилась в русле моих исследований по смешанным вычислениям.
Эта тематика очень хорошо подходит как стержневая для семинара: с одной стороны она задаёт явную ориентацию на анализ и преобразование программ, а с другой — допускает широкий охват проблем с уклоном на междисциплинарный контакт. Такой подход был присущ Игорю Васильевичу: широкий взгляд на понимание программ, близкий гуманитарному. Естественно, что я, будучи председателем семинара, мог влиять на тематику, которая сложилась вокруг направлений исследований нашего института. Сопредседателем ПК согласился стать мой давний знакомый Роберт Глюк (DIKU, Dept. of Computer Science, University of Copenhagen), с которым мы дружим более 20 лет.
Как известно, исследования в области смешанных вычислений восходят к академику А. П. Ершову. Смешанные вычисления можно трактовать как в узком, так и в широком, гуманитарном, мировоззренческом смысле. Что это значит? Допустим, есть некая общая, универсальная программа. Она может быть во многих обстановках использована, но мы знаем, что ее надо использовать в данном конкретном месте, и пытаемся, используя это знание, программу специализировать, т.е. сделать ее более частной, а за счет этого более эффективной, более понятной. Здесь в явном виде имеется дедукция, то есть переход от общего к частному. С такой точки зрения можно взглянуть на проблему и более широко. Например, последние работы одного из классиков смешанных вычислений В. Э. Иткина лежали в области философии, он много выступал с этой проблематикой на философских семинарах.
Еще при жизни Андрея Петровича Ершова было популярным многие программистские находки включать в тематику смешанных вычислений. Это был своего рода «лейбл», как сейчас нанотехнологии. В области смешанных вычислений работают до сих пор Ё. Футамура (InfiniteBio, Palo Alto, USA), Т. Могенсен (DIKU, University Copenhagen, Denmark), наш «ветеран», не пропустивший ни одной Ершовской конференции, С. Романенко, А. Климов (ИПМ им. М. В. Келдыша), последователи В. Ф. Турчина. В свое время у нас было соперничество, которое теперь плавно перешло в сотрудничество.
 |
| Т. Моргенсен и Д. Бьорнер, Дания. |
С течением времени меняются не только сами теоретические воззрения, но и подходы к роли теоретических исследований. У нас давние споры с одним из классиков программирования А. Н. Тереховым по поводу подходов к теории компиляции. Я в свое время настаивал на необходимости решения сложных задач глобальной оптимизации, а он говорил, что надо искать практические методы для применения их в реальной обстановке. Через 15 лет наши точки зрения в определённом смысле поменялись местами. Те вопросы, которые раньше казались академическими, с развитием техники трансляции во многих трансляторах нашли свое практическое применение. Встречаются даже гораздо более сложные техники, чем те, которые казались ранее слабо воплотимыми. Приходят порой студенты, исследования которых можно выразить в терминах смешанных вычислений. Они сами до этого доходят практически, еще не подозревая о существовании соответствующей теории, в терминах которой можно изложить их находки. На методологическом уровне это и есть соотношение между общим и частным.
В. А. Захаров:
 |
| В. Захаров (г. Москва). |
— Компьютер — одно из самых сложных устройств, созданных человечеством. И самая сложная часть компьютера, которая порой не видна тем, кто им пользуется — это программы. Весь компьютер пронизан программами, и даже то, что называют «железной» частью компьютера, аппаратурой — это тоже программа, которая реализована в виде полупроводников, проводов и прочих физических частей.
До тех пор, пока компьютеры были простыми, и программы были сравнительно простыми. Достаточно было аккуратного квалифицированного человеческого труда, чтобы обеспечить правильную и производительную работу этих программ. Но по мере широкого распространения программ и удешевления компьютеров объем и сложность программ неизмеримо возросли, в то время как количество программистов увеличилось незначительно. Это означало, что для поддержания темпов развития программирования программисты должны быть снабжены хорошим инструментальным аппаратом. Подобно тому, как сложное механическое устройство невозможно сделать, если не будет хороших обрабатывающих станков, материалов, подходящей технологии, точно так же хорошие производительные точные программы нельзя будет создавать, если не будет подходящей инструментальной базы для создания этих программ.
Одним из важных компонентов этой инструментальной базы являются средства, позволяющие оценивать, доказывать, проверять то, что программы выполняют именно те функции, которые от них требуются, т.е. являются правильными, корректными. Для доказательства обоснования корректности программ, для построения надежных и производительных программ необходимо, прежде всего, точное понимание связи между устройством программы и той функцией, которую программа выполняет.
Проблемы обнаружения этой взаимосвязи, распознавания того, как зависят между собой устройство программы, ее синтаксис, ее структура, и та функция, которую выполняет программа, тем поведением, которую она обеспечивает, и составляют тематику семинара «Понимание программ», который проводится в третий раз в Новосибирске. Этот семинар охватывает как теоретические вопросы, связанные с выявлением этой взаимосвязи между устройством и функционированием программы, так и практическое создание инструментальных средств, используемых на основании этих теоретических положений.
Программа, будучи очень сложной системой, оказывается и одним из наиболее сложных объектов математики. Дело в том, что вопросы понимания программ находятся на самой границе того, что могут совершать алгоритмы. Точный анализ программ, выяснение точной связи между устройством программы и ее функциональностью относится к числу алгоритмически неразрешимых задач, т.е. таких задач, для которых нет ни одного алгоритма, который бы наверняка мог их решить.
Это означает, что для того, чтобы иметь средства, позволяющие анализировать программы, доказывать их правильность, необходимо строить очень большое число моделей. Эти модели на разных уровнях абстракции и точности должны позволять оценивать поведение программы с тем, чтобы для практических программ, с которыми мы имеем дело в реальности, уметь решать ту задачу, для которой нет общего решения. Этот кажущийся парадокс составляет самую главную трудность и одновременно самую главную прелесть этого направления исследований.
К основным задачам, которые рассматриваются в этой области, относится задача доказательства правильности программ, разработки математических методов, которые бы позволяли обнаружить отсутствие или наличие ошибок в программе. Каким образом изменения, которые мы совершаем с программами, влияют на изменения в их поведении? Каким образом можно улучшать работу программ и их внешний облик (эта задача называется задачей реорганизации программ)? Каким образом можно показывать, что программы являются одинаковыми по поведению, эквивалентными? Каким образом можно, имея программу, написанную на одном языке программирования, преобразовать ее, не теряя эффективности, ее качеств, в программу, написанную на другом языке программирования? На все эти вопросы ищут ответы специалисты, работающие в этой области.
К этой же сфере деятельности относятся и многие вопросы компьютерной безопасности. Всем известны программы, с которыми почти всем приходилось сталкиваться — компьютерные вирусы. Как можно обнаружить, что программа, которую мы запускаем, таит в себе опасность повреждения нашего компьютера? Для того чтобы распознать злонамеренное поведение некой программы, необходимо уметь заранее по некоторым признакам в ее поведении, в ее устройстве обнаружить, что она может нанести вред нашей информационной системе.
В самом широком смысле тематика понимания программ охватывает практически всякую сторону деятельности программирования. Программист, который разрабатывает текст программы, тем самым вольно или невольно, подчас бессознательно, решает для себя задачу понимания программ: каким образом тот текст программы, который он пишет, обеспечивает поведение программы? С другой стороны, в чисто техническом отношении это всё-таки достаточно узкое направление, поскольку оно занимается изучением довольно специальных математических методов, при помощи которых удается установить связь между поведением и текстом программы.
Это направление имеет непосредственную связь с технологией программирования. Один из этапов технологии создания всякой программы — это доказательство в самом высшем математическом смысле того, что написанная программа является правильной. Каким образом можно убедить пользователя в том, что предъявленный ему программный продукт выполняет в точности то, что пользователь желает? Можно ему предъявить систему тестовых примеров, демонстрирующих, что в частных случаях, на специально подобранных значениях входных параметров программа показывает желаемое поведение. Но на самом деле, если программа имеет сложное, изощренное поведение, такая система примеров не является достаточно убедительной демонстрацией правильности ее работы.
Самый надежный способ проверки правильности программы и убеждения в этом пользователя состоит в том, что пользователю предъявляется вместе с программой доказательство ее правильности. Оно должно быть таким же строгим, как доказательство математической теоремы. Пользователь, либо имея определенный опыт изучения таких доказательств, либо располагая инструментальным средством проверки правильности доказательства, может взять сертификат, проверить его, и он будет надежной гарантией правильности программы. Разработка методов проверки правильности программ путем построения доказательств их правильности — это важный, перспективный и, как считают многие специалисты у нас и за рубежом, единственно возможный способ дальнейшего совершенствования технологии программирования.
стр. 4